exact (sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair (by decide) hA hB hA' hB').symm.not_rotate
  cfg.sbtw_A_A₁_A₂.wbtw
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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
hB' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
⊢ False
no goals