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 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.

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

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_ABC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : AffineIndependent ℝ ![self.A, self.B, self.C]

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_A₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : Wbtw ℝ self.B self.A₁ self.C

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_A_B₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : Wbtw ℝ self.A self.B₁ self.C

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_A_P_A₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : Wbtw ℝ self.A self.P self.A₁

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : Wbtw ℝ self.B self.Q self.B₁

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

theorem Imo2019Q2.Imo2019q2Cfg.P_ne_Q {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : self.P ≠ self.Q

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_P_B₁_P₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : Sbtw ℝ self.P self.B₁ self.P₁

theorem Imo2019Q2.Imo2019q2Cfg.angle_PP₁C_eq_angle_BAC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : EuclideanGeometry.angle self.P self.P₁ self.C = EuclideanGeometry.angle self.B self.A self.C

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

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : Sbtw ℝ self.Q self.A₁ self.Q₁

theorem Imo2019Q2.Imo2019q2Cfg.angle_CQ₁Q_eq_angle_CBA {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) : EuclideanGeometry.angle self.C self.Q₁ self.Q = EuclideanGeometry.angle self.C self.B self.A

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

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.

Equations

• Imo2019Q2.someOrientation V = { positiveOrientation := (FiniteDimensional.finBasisOfFinrankEq ℝ V ⋯).orientation }

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").

Equations

• One or more equations did not get rendered due to their size.

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_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [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.

Equations

• cfg.triangleABC = { points := ![cfg.A, cfg.B, cfg.C], independent := ⋯ }

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

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

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

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

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

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.

Equations

• cfg.A₂ = (Affine.Simplex.circumsphere cfg.triangleABC).secondInter cfg.A (cfg.A₁ -ᵥ cfg.A)

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.

Equations

• cfg.B₂ = (Affine.Simplex.circumsphere cfg.triangleABC).secondInter cfg.B (cfg.B₁ -ᵥ cfg.B)

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

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

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

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

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_A₁ {V : Type u_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : Collinear ℝ {cfg.P, cfg.A, cfg.A₁, cfg.A₂}

theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_C {V : Type u_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [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_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) : (affineSpan ℝ {cfg.C, cfg.B}).SOppSide 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_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) [Module.Oriented ℝ V (Fin 2)] : (EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.Q).sign = (EuclideanGeometry.oangle cfg.C cfg.B cfg.A).sign

theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA {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) [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_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) : cfg.A₁ ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_A₁_C {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) : Sbtw ℝ cfg.B cfg.A₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_B₁_C {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) : Sbtw ℝ cfg.A cfg.B₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_A₁_A₂ {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) : Sbtw ℝ cfg.A cfg.A₁ cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_B₁_B₂ {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) : Sbtw ℝ cfg.B cfg.B₁ cfg.B₂

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_A {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) : cfg.A₂ ≠ cfg.A

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_P {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) : cfg.A₂ ≠ cfg.P

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_B {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) : cfg.A₂ ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_C {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) : cfg.A₂ ≠ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_B {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) : cfg.B₂ ≠ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_Q {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) : cfg.B₂ ≠ cfg.Q

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_A₂ {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) : cfg.B₂ ≠ cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₂ {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) : Wbtw ℝ cfg.B cfg.Q cfg.B₂

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_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) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.Q cfg.P cfg.A₂ = 2 • EuclideanGeometry.oangle cfg.B cfg.A cfg.A₂

More obvious configuration properties

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂ {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) : ¬Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_ne_A₂ {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) : cfg.Q₁ ≠ cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_QPA₂ {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) : AffineIndependent ℝ ![cfg.Q, cfg.P, cfg.A₂]

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_PQB₂ {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) : AffineIndependent ℝ ![cfg.P, cfg.Q, cfg.B₂]

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.

Equations

• cfg.triangleQPA₂ = { points := ![cfg.Q, cfg.P, cfg.A₂], independent := ⋯ }

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.

Equations

• cfg.trianglePQB₂ = { points := ![cfg.P, cfg.Q, cfg.B₂], independent := ⋯ }

theorem Imo2019Q2.Imo2019q2Cfg.symm_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) : cfg.symm.triangleQPA₂ = cfg.trianglePQB₂

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₁.

Equations

• cfg.ω = Affine.Simplex.circumsphere cfg.triangleQPA₂

theorem Imo2019Q2.Imo2019q2Cfg.P_mem_ω {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) : cfg.P ∈ cfg.ω

theorem Imo2019Q2.Imo2019q2Cfg.Q_mem_ω {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) : cfg.Q ∈ 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_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) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.Q cfg.P cfg.A₂ = 2 • EuclideanGeometry.oangle cfg.Q cfg.B₂ cfg.A₂

Conclusions from that first angle chase

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_QPB₂A₂ {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.Cospherical {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}

theorem Imo2019Q2.Imo2019q2Cfg.symm_ω_eq_trianglePQB₂_circumsphere {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) : cfg.symm.ω = Affine.Simplex.circumsphere cfg.trianglePQB₂

theorem Imo2019Q2.Imo2019q2Cfg.symm_ω {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) : cfg.symm.ω = cfg.ω

The second angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA {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) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.C cfg.A₂ 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_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) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.C cfg.A₂ 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_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) : ¬Collinear ℝ {cfg.C, cfg.A₂, cfg.A₁}

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂ {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.Cospherical {cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂}

The third angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂ {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) [Module.Oriented ℝ V (Fin 2)] : 2 • EuclideanGeometry.oangle cfg.Q cfg.Q₁ cfg.A₂ = 2 • EuclideanGeometry.oangle cfg.Q cfg.P cfg.A₂

Conclusions from that third angle chase

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_mem_ω {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) : cfg.Q₁ ∈ cfg.ω

theorem Imo2019Q2.Imo2019q2Cfg.P₁_mem_ω {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) : cfg.P₁ ∈ cfg.ω

theorem Imo2019Q2.Imo2019q2Cfg.result {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.Concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}

theorem imo2019_q2 (V : Type u_1) (Pt : Type u_2) [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 : (affineSpan ℝ {P, Q}).Parallel (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₁}