Theorem: Imo2019P2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign (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)
⊢ (∡ cfg.C cfg.Q₁ cfg.Q).sign = (∡ cfg.C cfg.B cfg.A).sign
Tactic:
rw [← cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_right,
  cfg.sOppSide_CB_Q_Q₁.oangle_sign_eq_neg (left_mem_affineSpan_pair ℝ cfg.C cfg.B)
    cfg.wbtw_B_A₁_C.symm.mem_affineSpan,
  ← Real.Angle.sign_neg, ← oangle_rev,
  cfg.wbtw_B_A₁_C.oangle_sign_eq_of_ne_right cfg.Q cfg.A₁_ne_C, oangle_rotate_sign,
  cfg.wbtw_B_Q_B₁.oangle_eq_right cfg.Q_ne_B,
  cfg.wbtw_A_B₁_C.symm.oangle_sign_eq_of_ne_left cfg.B cfg.B₁_ne_C.symm]
State after:
no goals