Theorem: Imo2019P2.Imo2019q2Cfg.symm_A₂ (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.A₂ = cfg.B₂
Tactic:
simp_rw [A₂, B₂, symm_triangleABC_circumsphere]
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
⊢ (circumsphere cfg.triangleABC).secondInter cfg.symm.A (cfg.symm.A₁ -ᵥ cfg.symm.A) =
    (circumsphere cfg.triangleABC).secondInter cfg.B (cfg.B₁ -ᵥ cfg.B)

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
⊢ (circumsphere cfg.triangleABC).secondInter cfg.symm.A (cfg.symm.A₁ -ᵥ cfg.symm.A) =
    (circumsphere cfg.triangleABC).secondInter cfg.B (cfg.B₁ -ᵥ cfg.B)
Tactic:
rfl
State after:
no goals