exact Set.subset_insert _ _
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.B
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ {cfg.A, cfg.C, cfg.B} ⊆ {cfg.A₁, cfg.A, cfg.C, cfg.B}
no goals