Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB (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
⊢ cfg.Q ∉ affineSpan ℝ {cfg.C, cfg.B}
Tactic:
intro hQ
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
have hQA₁ : line[ℝ, cfg.Q, cfg.A₁] ≤ line[ℝ, cfg.C, cfg.B] :=
  affineSpan_pair_le_of_mem_of_mem hQ cfg.wbtw_B_A₁_C.symm.mem_affineSpan
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
⊢ False

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
have hQ₁ : cfg.Q₁ ∈ line[ℝ, cfg.C, cfg.B] := by
  rw [AffineSubspace.le_def'] at hQA₁
  exact hQA₁ _ cfg.sbtw_Q_A₁_Q₁.right_mem_affineSpan
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
have hc : Collinear ℝ ({cfg.C, cfg.Q₁, cfg.Q} : Set Pt) :=
  haveI hc' : Collinear ℝ ({cfg.B, cfg.C, cfg.Q₁, cfg.Q} : Set Pt) := by
    rw [Set.insert_comm cfg.B, Set.insert_comm cfg.B, Set.pair_comm, Set.insert_comm cfg.C,
      Set.insert_comm cfg.C]
    exact collinear_insert_insert_of_mem_affineSpan_pair hQ₁ hQ
  hc'.subset (Set.subset_insert _ _)
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : Collinear ℝ {cfg.C, cfg.Q₁, cfg.Q}
⊢ False

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : Collinear ℝ {cfg.C, cfg.Q₁, cfg.Q}
⊢ False
Tactic:
rw [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, cfg.angle_CQ₁Q_eq_angle_CBA,
  or_iff_right cfg.C_ne_Q₁, or_iff_right cfg.sbtw_Q_A₁_Q₁.left_ne_right, angle_comm] at hc
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : ∠ cfg.A cfg.B cfg.C = 0 ∨ ∠ cfg.A cfg.B cfg.C = π
⊢ False

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : ∠ cfg.A cfg.B cfg.C = 0 ∨ ∠ cfg.A cfg.B cfg.C = π
⊢ False
Tactic:
exact cfg.not_collinear_ABC (hc.elim collinear_of_angle_eq_zero collinear_of_angle_eq_pi)
State after:
no goals

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
⊢ cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
Tactic:
rw [AffineSubspace.le_def'] at hQA₁
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : ∀ p ∈ affineSpan ℝ {cfg.Q, cfg.A₁}, p ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ cfg.Q₁ ∈ affineSpan ℝ {cfg.C, 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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : ∀ p ∈ affineSpan ℝ {cfg.Q, cfg.A₁}, p ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
Tactic:
exact hQA₁ _ cfg.sbtw_Q_A₁_Q₁.right_mem_affineSpan
State after:
no goals

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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.B, cfg.C, cfg.Q₁, cfg.Q}
Tactic:
rw [Set.insert_comm cfg.B, Set.insert_comm cfg.B, Set.pair_comm, Set.insert_comm cfg.C,
  Set.insert_comm cfg.C]
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.Q₁, cfg.Q, cfg.C, 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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.Q₁, cfg.Q, cfg.C, cfg.B}
Tactic:
exact collinear_insert_insert_of_mem_affineSpan_pair hQ₁ hQ
State after:
no goals