Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA (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.A₂ cfg.A₁ = 2 • ∡ cfg.C cfg.A₂ cfg.A
Tactic:
rw [cfg.sbtw_A_A₁_A₂.symm.oangle_eq_right]
State after:
no goals