have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
  refine cfg.triangleABC.circumsphere.cospherical.subset ?_
  simp only [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
    cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff, and_true]
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
this : Module.Oriented ℝ V (Fin 2)
⊢ AffineIndependent ℝ ![cfg.B, cfg.A, cfg.A₂]
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
this : Module.Oriented ℝ V (Fin 2)
h : Cospherical {cfg.B, cfg.A, cfg.A₂}
⊢ AffineIndependent ℝ ![cfg.B, cfg.A, cfg.A₂]