Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_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
⊢ cfg.Q₁ ≠ cfg.A₂
Tactic:
intro h
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
h : cfg.Q₁ = cfg.A₂
⊢ 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
h : cfg.Q₁ = cfg.A₂
⊢ False
Tactic:
have h₁ := cfg.sbtw_Q_A₁_Q₁
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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.Q₁
⊢ False
Tactic:
rw [h] at h₁
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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ False
Tactic:
refine cfg.not_collinear_QPA₂ ?_
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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ Collinear ℝ {cfg.Q, cfg.P, 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
have hA₂ := cfg.sbtw_A_A₁_A₂.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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
have hA₂A₁ : line[ℝ, cfg.A₂, cfg.A₁] ≤ line[ℝ, cfg.A, cfg.A₁] :=
  affineSpan_pair_le_of_left_mem hA₂
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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
have hQ : cfg.Q ∈ line[ℝ, cfg.A, cfg.A₁] := by
  rw [AffineSubspace.le_def'] at hA₂A₁
  exact hA₂A₁ _ h₁.left_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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
hQ : cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
hQ : cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
exact collinear_triple_of_mem_affineSpan_pair hQ cfg.wbtw_A_P_A₁.mem_affineSpan hA₂
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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
Tactic:
rw [AffineSubspace.le_def'] at hA₂A₁
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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : ∀ p ∈ affineSpan ℝ {cfg.A₂, cfg.A₁}, p ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ cfg.Q ∈ 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : ∀ p ∈ affineSpan ℝ {cfg.A₂, cfg.A₁}, p ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
Tactic:
exact hA₂A₁ _ h₁.left_mem_affineSpan
State after:
no goals