mathlib3 documentation

mathlib-archive / imo.imo2019_q2

IMO 2019 Q2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ℤ) • _ _ _.

We apply the following conventions for formalizing IMO geometry problems. A problem is assumed to take place in the plane unless that is clearly not intended, so it is not required to prove that the points are coplanar (whether or not that in fact follows from the other conditions). Angles in problem statements are taken to be unoriented. A reference to an angle ∠XYZ is taken to imply that X and Z are not equal to Y, since choices of junk values play no role in informal mathematics, and those implications are included as hypotheses for the problem whether or not they follow from the other hypotheses. Similar, a reference to XY as a line is taken to imply that X does not equal Y and that is included as a hypothesis, and a reference to XY being parallel to something is considered a reference to it as a line. However, such an implicit hypothesis about two points being different is included only once for any given two points (even if it follows from more than one reference to a line or an angle), if X ≠ Y is included then Y ≠ X is not included separately, and such hypotheses are not included in the case where there is also a reference in the problem to a triangle including those two points, or to strict betweenness of three points including those two. If betweenness is stated, it is taken to be strict betweenness. However, segments and sides are taken to include their endpoints (unless this makes a problem false), although those degenerate cases might not necessarily have been considered when the problem was formulated and contestants might not have been expected to deal with them. A reference to a point being on a side or a segment is expressed directly with wbtw rather than more literally with affine_segment.

@[nolint]
structure imo2019_q2.imo2019q2_cfg (V : Type u_1) (Pt : Type u_2) [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 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 imo2019_q2.imo2019q2_cfg
  • imo2019_q2.imo2019q2_cfg.has_sizeof_inst
noncomputable def imo2019_q2.some_orientation (V : Type u_1) [normed_add_comm_group V] [inner_product_space V] [hd2 : fact (fdim V = 2)] :

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

Equations

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

Equations

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

points A₂ and B₂

theorem imo2019_q2.imo2019q2_cfg.A_ne_B {V : Type u_1} {Pt : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.A cfg.B
theorem imo2019_q2.imo2019q2_cfg.A_ne_C {V : Type u_1} {Pt : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.A cfg.C
theorem imo2019_q2.imo2019q2_cfg.B_ne_C {V : Type u_1} {Pt : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.B cfg.C

ABC as a triangle.

Equations
noncomputable def imo2019_q2.imo2019q2_cfg.A₂ {V : Type u_1} {Pt : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (cfg : imo2019_q2.imo2019q2_cfg V Pt) :
Pt

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

Equations
noncomputable def imo2019_q2.imo2019q2_cfg.B₂ {V : Type u_1} {Pt : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (cfg : imo2019_q2.imo2019q2_cfg V Pt) :
Pt

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

Equations
theorem imo2019_q2.imo2019q2_cfg.Q_ne_B {V : Type u_1} {Pt : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.Q cfg.B

Relate the orientations of different angles in the configuration #

More obvious configuration properties #

The first equality in the first angle chase in the solution #

More obvious configuration properties #

QPA₂ as a triangle.

Equations

PQB₂ as a triangle.

Equations

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

Equations

The rest of the first angle chase in the solution #

Conclusions from that first angle chase #

The second angle chase in the solution #

Conclusions from that second angle chase #

The third angle chase in the solution #

Conclusions from that third angle chase #

theorem imo2019_q2 (V : Type u_1) (Pt : Type u_2) [normed_add_comm_group V] [inner_product_space V] [metric_space Pt] [normed_add_torsor V Pt] [hd2 : fact (fdim V = 2)] (A B C A₁ B₁ P Q P₁ Q₁ : Pt) (affine_independent_ABC : affine_independent ![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 : (affine_span {P, Q}).parallel (affine_span {A, B})) (P_ne_Q : P Q) (sbtw_P_B₁_P₁ : sbtw P B₁ P₁) (angle_PP₁C_eq_angle_BAC : euclidean_geometry.angle P P₁ C = euclidean_geometry.angle B A C) (C_ne_P₁ : C P₁) (sbtw_Q_A₁_Q₁ : sbtw Q A₁ Q₁) (angle_CQ₁Q_eq_angle_CBA : euclidean_geometry.angle C Q₁ Q = euclidean_geometry.angle C B A) (C_ne_Q₁ : C Q₁) :
euclidean_geometry.concyclic {P, Q, P₁, Q₁}