Compfiles/Imo2023P6.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2023, Problem 6

Let ABC be an equilateral triangle. Let A₁,B₁,C₁ be interior points of ABC such that BA₁=A₁C, CB₁ = B₁A, AC₁=C₁B, and

∠BA₁C + ∠CB₁A + ∠C₁B = 480°.

Let BC₁ and CB₁ meet at A₂, let CA₁ and AC₁ meet at B₂, and let AB₁ and BA₁ meet at $C₂.

Prove that if triangle A₁B₁C₁ is scalene, then the three circumcircles of triangles AA₁A₂, BB₁B₂ and CC₁C₂ all pass through two common points.

Imports (2)
Imported by 1 file
  1. problem Imo2023P6.imo2023_p6 sorry line 42 source

    depends on sorry what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, AffineIndependent, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Affine.Simplex.Equilateral, Affine.Simplex.mk, Membership.mem, Set, Affine.Simplex.interior and 21 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.