fin_cases i <;> rfl
case h
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
i : Fin (2 + 1)
⊢ cfg.symm.triangleABC.points i = (reindex cfg.triangleABC (Equiv.swap 0 1)).points i
no goals