Theorem: Imo2019P2.Imo2019q2Cfg.QP_parallel_BA (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
⊢ affineSpan ℝ {cfg.Q, cfg.P} ∥ affineSpan ℝ {cfg.B, cfg.A}
Tactic:
rw [Set.pair_comm cfg.Q, Set.pair_comm cfg.B]
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
⊢ affineSpan ℝ {cfg.P, cfg.Q} ∥ affineSpan ℝ {cfg.A, cfg.B}

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
⊢ affineSpan ℝ {cfg.P, cfg.Q} ∥ affineSpan ℝ {cfg.A, cfg.B}
Tactic:
exact cfg.PQ_parallel_AB
State after:
no goals