Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂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.B cfg.B₂ cfg.A₂ = 2 • ∡ cfg.Q cfg.B₂ cfg.A₂
Tactic:
rw [cfg.wbtw_B_Q_B₂.symm.oangle_eq_left cfg.B₂_ne_Q.symm]
State after:
no goals