Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleQPA₂ (Compfiles/Imo2019P2.lean)

State before:
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
⊢ cfg.symm.triangleQPA₂ = cfg.trianglePQB₂
Tactic:
simp_rw [trianglePQB₂, ← symm_A₂]
State after:
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
⊢ cfg.symm.triangleQPA₂ = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }

State before:
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
⊢ cfg.symm.triangleQPA₂ = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }
Tactic:
ext i
State after:
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.triangleQPA₂.points i = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }.points i

State before:
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.triangleQPA₂.points i = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }.points i
Tactic:
fin_cases i <;> rfl
State after:
no goals