IMO 2019 Q2

In triangle ABC, point A₁ lies on side BC and point B₁ lies on side AC. Let P and Q be points on segments AA₁ and BB₁, respectively, such that PQ is parallel to AB. Let P₁ be a point on line PB₁, such that B₁ lies strictly between P and P₁, and ∠PP₁C = ∠BAC. Similarly, let Q₁ be a point on line QA₁, such that A₁ lies strictly between Q and Q₁, and ∠CQ₁Q = ∠CBA.

Prove that points P, Q, P₁, and Q₁ are concyclic.

We follow Solution 1 from the official solutions. Letting the rays AA₁ and BB₁ intersect the circumcircle of ABC at A₂ and B₂ respectively, we show with an angle chase that P, Q, A₂, B₂ are concyclic and let ω be the circle through those points. We then show that C, Q₁, A₂, A₁ are concyclic, and then that Q₁ lies on ω, and similarly that P₁ lies on ω, so the required four points are concyclic.

Note that most of the formal proof is actually proving nondegeneracy conditions needed for that angle chase / concyclicity argument, where an informal solution doesn't discuss those conditions at all. Also note that (as described in Geometry.Euclidean.Angle.Oriented.Basic) the oriented angles used are modulo 2 * π, so parts of the angle chase that are only valid for angles modulo π (as used in the informal solution) are represented as equalities of twice angles, which we write as (2 : ℤ) • ∡ _ _ _ = (2 : ℤ) • _ _ _.

structure Imo2019Q2.Imo2019q2Cfg (V : Type u_1) (Pt : Type u_2) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] : Type u_2

• A : Pt
• B : Pt
• C : Pt
• A₁ : Pt
• B₁ : Pt
• P : Pt
• Q : Pt
• P₁ : Pt
• Q₁ : Pt
• affineIndependent_ABC : AffineIndependent ℝ ![s.A, s.B, s.C]
• wbtw_B_A₁_C : Wbtw ℝ s.B s.A₁ s.C
• wbtw_A_B₁_C : Wbtw ℝ s.A s.B₁ s.C
• wbtw_A_P_A₁ : Wbtw ℝ s.A s.P s.A₁
• wbtw_B_Q_B₁ : Wbtw ℝ s.B s.Q s.B₁
• PQ_parallel_AB : AffineSubspace.Parallel (affineSpan ℝ {s.P, s.Q}) (affineSpan ℝ {s.A, s.B})
• P_ne_Q : s.P ≠ s.Q
• sbtw_P_B₁_P₁ : Sbtw ℝ s.P s.B₁ s.P₁
• angle_PP₁C_eq_angle_BAC : EuclideanGeometry.angle s.P s.P₁ s.C = EuclideanGeometry.angle s.B s.A s.C
• C_ne_P₁ : s.C ≠ s.P₁
• sbtw_Q_A₁_Q₁ : Sbtw ℝ s.Q s.A₁ s.Q₁
• angle_CQ₁Q_eq_angle_CBA : EuclideanGeometry.angle s.C s.Q₁ s.Q = EuclideanGeometry.angle s.C s.B s.A
• C_ne_Q₁ : s.C ≠ s.Q₁

A configuration satisfying the conditions of the problem. We define this structure to avoid passing many hypotheses around as we build up information about the configuration; the final result for a statement of the problem not using this structure is then deduced from one in terms of this structure.

def Imo2019Q2.someOrientation (V : Type u_1) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2)

A default choice of orientation, for lemmas that need to pick one.

def Imo2019Q2.Imo2019q2Cfg.symm {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg V Pt

The configuration has symmetry, allowing results proved for one point to be applied for another (where the informal solution says "similarly").

Configuration properties that are obvious from the diagram, and construction of the

points A₂ and B₂

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_B {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.A ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.A ≠ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B_ne_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.B ≠ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_ABC {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : ¬Collinear ℝ {cfg.A, cfg.B, cfg.C}

def Imo2019Q2.Imo2019q2Cfg.triangleABC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Affine.Triangle ℝ Pt

ABC as a Triangle.

theorem Imo2019Q2.Imo2019q2Cfg.A_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.A ∈ Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg)

theorem Imo2019Q2.Imo2019q2Cfg.B_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.B ∈ Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg)

theorem Imo2019Q2.Imo2019q2Cfg.C_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.C ∈ Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg)

theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.triangleABC (Imo2019Q2.Imo2019q2Cfg.symm cfg) = Affine.Simplex.reindex (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg) (Equiv.swap 0 1)

theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC (Imo2019Q2.Imo2019q2Cfg.symm cfg)) = Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg)

def Imo2019Q2.Imo2019q2Cfg.A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Pt

A₂ is the second point of intersection of the ray AA₁ with the circumcircle of ABC.

def Imo2019Q2.Imo2019q2Cfg.B₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Pt

B₂ is the second point of intersection of the ray BB₁ with the circumcircle of ABC.

theorem Imo2019Q2.Imo2019q2Cfg.A₂_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.A₂ cfg ∈ Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg)

theorem Imo2019Q2.Imo2019q2Cfg.B₂_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.B₂ cfg ∈ Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.triangleABC cfg)

theorem Imo2019Q2.Imo2019q2Cfg.symm_A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.A₂ (Imo2019Q2.Imo2019q2Cfg.symm cfg) = Imo2019Q2.Imo2019q2Cfg.B₂ cfg

theorem Imo2019Q2.Imo2019q2Cfg.QP_parallel_BA {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : AffineSubspace.Parallel (affineSpan ℝ {cfg.Q, cfg.P}) (affineSpan ℝ {cfg.B, cfg.A})

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_A₁ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.A ≠ cfg.A₁

theorem Imo2019Q2.Imo2019q2Cfg.collinear_PAA₁A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Collinear ℝ {cfg.P, cfg.A, cfg.A₁, Imo2019Q2.Imo2019q2Cfg.A₂ cfg}

theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.A₁ ≠ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B₁_ne_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.B₁ ≠ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.Q_not_mem_CB {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : ¬cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}

theorem Imo2019Q2.Imo2019q2Cfg.Q_ne_B {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.Q ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : AffineSubspace.SOppSide (affineSpan ℝ {cfg.C, cfg.B}) cfg.Q cfg.Q₁

Relate the orientations of different angles in the configuration

theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : Real.Angle.sign (EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.Q) = Real.Angle.sign (EuclideanGeometry.oangle cfg.C cfg.B cfg.A)

theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.Q = EuclideanGeometry.oangle cfg.C cfg.B cfg.A

More obvious configuration properties

theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_B {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.A₁ ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_A₁_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Sbtw ℝ cfg.B cfg.A₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_B₁_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Sbtw ℝ cfg.A cfg.B₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_A₁_A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Sbtw ℝ cfg.A cfg.A₁ (Imo2019Q2.Imo2019q2Cfg.A₂ cfg)

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_B₁_B₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Sbtw ℝ cfg.B cfg.B₁ (Imo2019Q2.Imo2019q2Cfg.B₂ cfg)

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_A {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.A₂ cfg ≠ cfg.A

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_P {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.A₂ cfg ≠ cfg.P

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_B {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.A₂ cfg ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_C {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.A₂ cfg ≠ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_B {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.B₂ cfg ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_Q {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.B₂ cfg ≠ cfg.Q

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.B₂ cfg ≠ Imo2019Q2.Imo2019q2Cfg.A₂ cfg

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Wbtw ℝ cfg.B cfg.Q (Imo2019Q2.Imo2019q2Cfg.B₂ cfg)

The first equality in the first angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.Q cfg.P (Imo2019Q2.Imo2019q2Cfg.A₂ cfg) = 2 • EuclideanGeometry.oangle cfg.B cfg.A (Imo2019Q2.Imo2019q2Cfg.A₂ cfg)

More obvious configuration properties

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : ¬Collinear ℝ {cfg.Q, cfg.P, Imo2019Q2.Imo2019q2Cfg.A₂ cfg}

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_ne_A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.Q₁ ≠ Imo2019Q2.Imo2019q2Cfg.A₂ cfg

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_QPA₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : AffineIndependent ℝ ![cfg.Q, cfg.P, Imo2019Q2.Imo2019q2Cfg.A₂ cfg]

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_PQB₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : AffineIndependent ℝ ![cfg.P, cfg.Q, Imo2019Q2.Imo2019q2Cfg.B₂ cfg]

def Imo2019Q2.Imo2019q2Cfg.triangleQPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Affine.Triangle ℝ Pt

QPA₂ as a Triangle.

def Imo2019Q2.Imo2019q2Cfg.trianglePQB₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Affine.Triangle ℝ Pt

PQB₂ as a Triangle.

theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleQPA₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.triangleQPA₂ (Imo2019Q2.Imo2019q2Cfg.symm cfg) = Imo2019Q2.Imo2019q2Cfg.trianglePQB₂ cfg

def Imo2019Q2.Imo2019q2Cfg.ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : EuclideanGeometry.Sphere Pt

ω is the circle containing Q, P and A₂, which will be shown also to contain B₂, P₁ and Q₁.

theorem Imo2019Q2.Imo2019q2Cfg.P_mem_ω {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.P ∈ Imo2019Q2.Imo2019q2Cfg.ω cfg

theorem Imo2019Q2.Imo2019q2Cfg.Q_mem_ω {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.Q ∈ Imo2019Q2.Imo2019q2Cfg.ω cfg

The rest of the first angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.Q cfg.P (Imo2019Q2.Imo2019q2Cfg.A₂ cfg) = 2 • EuclideanGeometry.oangle cfg.Q (Imo2019Q2.Imo2019q2Cfg.B₂ cfg) (Imo2019Q2.Imo2019q2Cfg.A₂ cfg)

Conclusions from that first angle chase

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_QPB₂A₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : EuclideanGeometry.Cospherical {cfg.Q, cfg.P, Imo2019Q2.Imo2019q2Cfg.B₂ cfg, Imo2019Q2.Imo2019q2Cfg.A₂ cfg}

theorem Imo2019Q2.Imo2019q2Cfg.symm_ω_eq_trianglePQB₂_circumsphere {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.ω (Imo2019Q2.Imo2019q2Cfg.symm cfg) = Affine.Simplex.circumsphere (Imo2019Q2.Imo2019q2Cfg.trianglePQB₂ cfg)

theorem Imo2019Q2.Imo2019q2Cfg.symm_ω {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Imo2019Q2.Imo2019q2Cfg.ω (Imo2019Q2.Imo2019q2Cfg.symm cfg) = Imo2019Q2.Imo2019q2Cfg.ω cfg

The second angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.C (Imo2019Q2.Imo2019q2Cfg.A₂ cfg) cfg.A₁ = 2 • EuclideanGeometry.oangle cfg.C cfg.B cfg.A

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.C (Imo2019Q2.Imo2019q2Cfg.A₂ cfg) cfg.A₁ = 2 • EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.A₁

Conclusions from that second angle chase

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_CA₂A₁ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : ¬Collinear ℝ {cfg.C, Imo2019Q2.Imo2019q2Cfg.A₂ cfg, cfg.A₁}

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : EuclideanGeometry.Cospherical {cfg.A₁, cfg.Q₁, cfg.C, Imo2019Q2.Imo2019q2Cfg.A₂ cfg}

The third angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂ {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.Q cfg.Q₁ (Imo2019Q2.Imo2019q2Cfg.A₂ cfg) = 2 • EuclideanGeometry.oangle cfg.Q cfg.P (Imo2019Q2.Imo2019q2Cfg.A₂ cfg)

Conclusions from that third angle chase

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_mem_ω {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.Q₁ ∈ Imo2019Q2.Imo2019q2Cfg.ω cfg

theorem Imo2019Q2.Imo2019q2Cfg.P₁_mem_ω {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : cfg.P₁ ∈ Imo2019Q2.Imo2019q2Cfg.ω cfg

theorem Imo2019Q2.Imo2019q2Cfg.result {V : Type u_2} {Pt : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : EuclideanGeometry.Concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}

theorem imo2019_q2 (V : Type u_2) (Pt : Type u_1) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (A : Pt) (B : Pt) (C : Pt) (A₁ : Pt) (B₁ : Pt) (P : Pt) (Q : Pt) (P₁ : Pt) (Q₁ : Pt) (affine_independent_ABC : AffineIndependent ℝ ![A, B, C]) (wbtw_B_A₁_C : Wbtw ℝ B A₁ C) (wbtw_A_B₁_C : Wbtw ℝ A B₁ C) (wbtw_A_P_A₁ : Wbtw ℝ A P A₁) (wbtw_B_Q_B₁ : Wbtw ℝ B Q B₁) (PQ_parallel_AB : AffineSubspace.Parallel (affineSpan ℝ {P, Q}) (affineSpan ℝ {A, B})) (P_ne_Q : P ≠ Q) (sbtw_P_B₁_P₁ : Sbtw ℝ P B₁ P₁) (angle_PP₁C_eq_angle_BAC : EuclideanGeometry.angle P P₁ C = EuclideanGeometry.angle B A C) (C_ne_P₁ : C ≠ P₁) (sbtw_Q_A₁_Q₁ : Sbtw ℝ Q A₁ Q₁) (angle_CQ₁Q_eq_angle_CBA : EuclideanGeometry.angle C Q₁ Q = EuclideanGeometry.angle C B A) (C_ne_Q₁ : C ≠ Q₁) : EuclideanGeometry.Concyclic {P, Q, P₁, Q₁}