have hc : Collinear ℝ ({cfg.A, cfg.B, cfg.C, cfg.A₁} : Set Pt) :=
  collinear_insert_insert_of_mem_affineSpan_pair h₁.left_mem_affineSpan
    cfg.sbtw_B_A₁_C.left_mem_affineSpan
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}