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