exact (angle_ne_zero_of_not_collinear cfg.not_collinear_ABC) ha
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
h : cfg.A₁ = cfg.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
ha : ∠ cfg.A cfg.B cfg.C = 0
⊢ False
no goals