Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂ (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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.Q cfg.Q₁ cfg.A₂ = 2 • ∡ cfg.A₁ cfg.Q₁ cfg.A₂
Tactic:
rw [cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_left]
State after:
no goals

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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.A₁ cfg.C cfg.A₂ = 2 • ∡ cfg.B cfg.C cfg.A₂
Tactic:
rw [cfg.sbtw_B_A₁_C.symm.oangle_eq_left]
State after:
no goals