Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂ (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.P cfg.A₂ = 2 • ∡ cfg.B cfg.A cfg.A₂
Tactic:
refine two_zsmul_oangle_of_parallel cfg.QP_parallel_BA ?_
State after:
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)
⊢ affineSpan ℝ {cfg.A₂, cfg.P} ∥ affineSpan ℝ {cfg.A₂, cfg.A}

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)
⊢ affineSpan ℝ {cfg.A₂, cfg.P} ∥ affineSpan ℝ {cfg.A₂, cfg.A}
Tactic:
convert AffineSubspace.Parallel.refl (k := ℝ) (P := Pt) _ using 1
State after:
case h.e'_9
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)
⊢ affineSpan ℝ {cfg.A₂, cfg.A} = affineSpan ℝ {cfg.A₂, cfg.P}

State before:
case h.e'_9
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)
⊢ affineSpan ℝ {cfg.A₂, cfg.A} = affineSpan ℝ {cfg.A₂, cfg.P}
Tactic:
rw [cfg.collinear_PAA₁A₂.affineSpan_eq_of_ne (Set.mem_insert_of_mem _
  (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
  (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) cfg.A₂_ne_A,
    cfg.collinear_PAA₁A₂.affineSpan_eq_of_ne (Set.mem_insert_of_mem _
  (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
  (Set.mem_insert _ _) cfg.A₂_ne_P]
State after:
no goals