exact cfg.not_collinear_ABC (hc.elim collinear_of_angle_eq_zero collinear_of_angle_eq_pi)
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : ∠ cfg.A cfg.B cfg.C = 0 ∨ ∠ cfg.A cfg.B cfg.C = π
⊢ False
no goals