# Documentation

Archive.Imo.Imo2019Q2

# 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) [] [] [] :
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.

Instances For
def Imo2019Q2.someOrientation (V : Type u_1) [] [hd2 : Fact ()] :

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

Instances For
def Imo2019Q2.Imo2019q2Cfg.symm {V : Type u_1} {Pt : Type u_2} [] [] [] (cfg : ) :

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

Instances For

### 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} [] [] [] (cfg : ) :
cfg.A cfg.B
theorem Imo2019Q2.Imo2019q2Cfg.A_ne_C {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
cfg.A cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.B_ne_C {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
cfg.B cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_ABC {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
¬Collinear {cfg.A, cfg.B, cfg.C}
def Imo2019Q2.Imo2019q2Cfg.triangleABC {V : Type u_1} {Pt : Type u_2} [] [] [] (cfg : ) :

ABC as a Triangle.

Instances For
theorem Imo2019Q2.Imo2019q2Cfg.A_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.B_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.C_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
def Imo2019Q2.Imo2019q2Cfg.A₂ {V : Type u_1} {Pt : Type u_2} [] [] [] (cfg : ) :
Pt

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

Instances For
def Imo2019Q2.Imo2019q2Cfg.B₂ {V : Type u_1} {Pt : Type u_2} [] [] [] (cfg : ) :
Pt

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

Instances For
theorem Imo2019Q2.Imo2019q2Cfg.A₂_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.B₂_mem_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.symm_A₂ {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.QP_parallel_BA {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
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} [] [] [] (cfg : ) :
cfg.A cfg.A₁
theorem Imo2019Q2.Imo2019q2Cfg.collinear_PAA₁A₂ {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
Collinear {cfg.P, cfg.A, cfg.A₁, }
theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_C {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
cfg.A₁ cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.B₁_ne_C {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
cfg.B₁ cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.Q_not_mem_CB {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
¬cfg.Q affineSpan {cfg.C, cfg.B}
theorem Imo2019Q2.Imo2019q2Cfg.Q_ne_B {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
cfg.Q cfg.B
theorem Imo2019Q2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁ {V : Type u_2} {Pt : Type u_1} [] [] [] (cfg : ) :
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} [] [] [] [hd2 : Fact ()] (cfg : ) [Module.Oriented V (Fin 2)] :
theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) [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} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.A₁ cfg.B
theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_A₁_C {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
Sbtw cfg.B cfg.A₁ cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_B₁_C {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
Sbtw cfg.A cfg.B₁ cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_A₁_A₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
Sbtw cfg.A cfg.A₁ ()
theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_B₁_B₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
Sbtw cfg.B cfg.B₁ ()
theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_A {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.A
theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_P {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.P
theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_B {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.B
theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_C {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.C
theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_B {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.B
theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_Q {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.Q
theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_A₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
Wbtw cfg.B cfg.Q ()

### 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} [] [] [] [hd2 : Fact ()] (cfg : ) [Module.Oriented V (Fin 2)] :
2 EuclideanGeometry.oangle cfg.Q cfg.P () = 2 EuclideanGeometry.oangle cfg.B cfg.A ()

### More obvious configuration properties #

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
¬Collinear {cfg.Q, cfg.P, }
theorem Imo2019Q2.Imo2019q2Cfg.Q₁_ne_A₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.Q₁
theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_QPA₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
AffineIndependent ![cfg.Q, cfg.P, ]
theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_PQB₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
AffineIndependent ![cfg.P, cfg.Q, ]
def Imo2019Q2.Imo2019q2Cfg.triangleQPA₂ {V : Type u_1} {Pt : Type u_2} [] [] [] [hd2 : Fact ()] (cfg : ) :

QPA₂ as a Triangle.

Instances For
def Imo2019Q2.Imo2019q2Cfg.trianglePQB₂ {V : Type u_1} {Pt : Type u_2} [] [] [] [hd2 : Fact ()] (cfg : ) :

PQB₂ as a Triangle.

Instances For
theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleQPA₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
def Imo2019Q2.Imo2019q2Cfg.ω {V : Type u_1} {Pt : Type u_2} [] [] [] [hd2 : Fact ()] (cfg : ) :

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

Instances For
theorem Imo2019Q2.Imo2019q2Cfg.P_mem_ω {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.P
theorem Imo2019Q2.Imo2019q2Cfg.Q_mem_ω {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.Q

### Conclusions from that first angle chase #

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_QPB₂A₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.symm_ω_eq_trianglePQB₂_circumsphere {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
theorem Imo2019Q2.Imo2019q2Cfg.symm_ω {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (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} [] [] [] [hd2 : Fact ()] (cfg : ) [Module.Oriented V (Fin 2)] :
2 EuclideanGeometry.oangle cfg.C () 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} [] [] [] [hd2 : Fact ()] (cfg : ) [Module.Oriented V (Fin 2)] :
2 EuclideanGeometry.oangle cfg.C () 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} [] [] [] [hd2 : Fact ()] (cfg : ) :
¬Collinear {cfg.C, , cfg.A₁}
theorem Imo2019Q2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂ {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
EuclideanGeometry.Cospherical {cfg.A₁, cfg.Q₁, cfg.C, }

### 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} [] [] [] [hd2 : Fact ()] (cfg : ) [Module.Oriented V (Fin 2)] :
2 EuclideanGeometry.oangle cfg.Q cfg.Q₁ () = 2 EuclideanGeometry.oangle cfg.Q cfg.P ()

### Conclusions from that third angle chase #

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_mem_ω {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.Q₁
theorem Imo2019Q2.Imo2019q2Cfg.P₁_mem_ω {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
cfg.P₁
theorem Imo2019Q2.Imo2019q2Cfg.result {V : Type u_2} {Pt : Type u_1} [] [] [] [hd2 : Fact ()] (cfg : ) :
EuclideanGeometry.Concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
theorem imo2019_q2 (V : Type u_2) (Pt : Type u_1) [] [] [] [hd2 : Fact ()] (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 : = ) (C_ne_P₁ : C P₁) (sbtw_Q_A₁_Q₁ : Sbtw Q A₁ Q₁) (angle_CQ₁Q_eq_angle_CBA : = ) (C_ne_Q₁ : C Q₁) :
EuclideanGeometry.Concyclic {P, Q, P₁, Q₁}