convert AffineSubspace.Parallel.refl (k := ℝ) (P := Pt) _ using 1
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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ affineSpan ℝ {cfg.A₂, cfg.P} ∥ affineSpan ℝ {cfg.A₂, cfg.A}
case h.e'_9
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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ affineSpan ℝ {cfg.A₂, cfg.A} = affineSpan ℝ {cfg.A₂, cfg.P}