awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have rw : ∀ (hp₂ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃) (hp₁₂ : p₁ ≠ p₂) (r₁ : k) (hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃),
  LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
Tactic: rw [← vsub_vadd p₂ p₃, vadd_left_mem_affineSpan_pair] at hp₂
Cleared hypotheses: hp₂, hp₁₂, r₁, hp₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₂ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have rcases : ∀ (r₂ : k) (hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃),
  LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
Tactic: rcases hp₂ with ⟨r₂, hp₂⟩
Cleared hypotheses: hp₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
⊢ r₂ - r₁ ≠ 0
have rw : r₂ ≠ r₁
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have hr₀ : r₂ - r₁ ≠ 0
Tactic: have hr₀ : r₂ - r₁ ≠ 0 := by
    rw [sub_ne_zero]
    rintro rfl
    simp_all
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁
Tactic: have hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁ := by
    simp [sub_smul, hp₁, hp₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have hr₁ : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
Tactic: rw [← eq_inv_smul_iff₀ hr₀] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have refine_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
Tactic: refine affineSpan_pair_le_of_mem_of_mem ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
refine_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have refine_2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₄
Tactic: refine affineSpan_pair_le_of_mem_of_mem ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
have h : p₃ = (-r₁ * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: convert! smul_vsub_vadd_mem_affineSpan_pair (-r₁ * (r₂ - r₁)⁻¹) p₁ p₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₄
have h : p₄ = ((1 - r₁) * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: convert! smul_vsub_vadd_mem_affineSpan_pair ((1 - r₁) * (r₂ - r₁)⁻¹) p₁ p₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
h₁₂₄₅ : Parallel (P := P) (affineSpan k {p₁, p₂}) (affineSpan k {p₄, p₅})
h₂₃₅₆ :
  LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₅, p₆})) (direction (P := P) (affineSpan k {p₂, p₃}))
h₃₁₆₄ :
  LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₆, p₄})) (direction (P := P) (affineSpan k {p₃, p₁}))
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have h₁₂₄₆ : ∃ (z : kˣ), z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
Tactic: rw [affineSpan_pair_parallel_iff_exists_unit_smul'] at h₁₂₄₅
Cleared hypotheses: h₁₂₄₅, h₂₃₅₆, h₃₁₆₄
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
h₁₂₄₅ : ∃ (z : kˣ), z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
h₂₃₅₆ :
  LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₅, p₆})) (direction (P := P) (affineSpan k {p₂, p₃}))
h₃₁₆₄ :
  LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₆, p₄})) (direction (P := P) (affineSpan k {p₃, p₁}))
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have h₂₃₅₇ : ∃ (z : k), z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
Tactic: rw [direction_affineSpan_pair_le_iff_exists_smul] at h₂₃₅₆ h₃₁₆₄
Cleared hypotheses: h₂₃₅₆, h₃₁₆₄
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
h₁₂₄₅ : ∃ (z : kˣ), z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
h₂₃₅₆ :
  LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₅, p₆})) (direction (P := P) (affineSpan k {p₂, p₃}))
h₃₁₆₄ :
  LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₆, p₄})) (direction (P := P) (affineSpan k {p₃, p₁}))
h₂₃₅₇ : ∃ (z : k), z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have h₃₁₆₅ : ∃ (z : k), z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
Tactic: rw [direction_affineSpan_pair_le_iff_exists_smul] at h₂₃₅₆ h₃₁₆₄
Cleared hypotheses: h₂₃₅₆, h₃₁₆₄
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
h₁₂₄₅ : ∃ (z : kˣ), z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
h₂₃₅₆ : ∃ (z : k), z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
h₃₁₆₄ : ∃ (z : k), z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have obtain : ∀ (r₁ : kˣ) (hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄),
  ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Tactic: obtain ⟨r₁, hr₁⟩ := h₁₂₄₅
Cleared hypotheses: h₁₂₄₅
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
h₂₃₅₆ : ∃ (z : k), z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
h₃₁₆₄ : ∃ (z : k), z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
r₁ : kˣ
hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have obtain : ∀ (r₂ : k) (hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅),
  ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Tactic: obtain ⟨r₂, hr₂⟩ := h₂₃₅₆
Cleared hypotheses: h₂₃₅₆
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
h₃₁₆₄ : ∃ (z : k), z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
r₁ : kˣ
hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have obtain : ∀ (r₃ : k) (hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆),
  ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Tactic: obtain ⟨r₃, hr₃⟩ := h₃₁₆₄
Cleared hypotheses: h₃₁₆₄
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have rw : ∀ (hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄) (r₂ : k) (hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅) (r₃ : k)
  (hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆),
  ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Tactic: rw [Units.smul_def] at hr₁
Cleared hypotheses: hr₁, r₂, hr₂, r₃, hr₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have pos : ∀ (h : (↑r₁ : k) = r₂),
  ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Tactic: by_cases h : (r₁ : k) = r₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
pos :
  ∀ (h : (↑r₁ : k) = r₂),
    ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have neg : ∀ (h : ¬(↑r₁ : k) = r₂),
  ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Tactic: by_cases h : (r₁ : k) = r₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have pos : p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
Tactic: refine ⟨r₁, r₁.ne_zero, hr₁.symm, h ▸ hr₂.symm, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₄ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₁)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₄ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₁)
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₅ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂ + (p₂ -ᵥ p₁))
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₄ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₅ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂ + (p₂ -ᵥ p₁))
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₆ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (↑r₁ : k) • (p₂ -ᵥ p₁)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₄ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₅ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂ + (p₂ -ᵥ p₁))
pos₆ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (↑r₁ : k) • (p₂ -ᵥ p₁)
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₇ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (p₅ -ᵥ p₄)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₄ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₅ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂ + (p₂ -ᵥ p₁))
pos₆ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (↑r₁ : k) • (p₂ -ᵥ p₁)
pos₇ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (p₅ -ᵥ p₄)
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₈ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = r₂ • (p₃ -ᵥ p₂) + (p₅ -ᵥ p₄)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : (↑r₁ : k) = r₂
pos : -(p₄ -ᵥ p₆) = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₁ : p₆ -ᵥ p₄ = -((↑r₁ : k) • (p₁ -ᵥ p₃))
pos₂ : p₆ -ᵥ p₄ = (↑r₁ : k) • -(p₁ -ᵥ p₃)
pos₃ : p₆ -ᵥ p₄ = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₄ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₁)
pos₅ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂ + (p₂ -ᵥ p₁))
pos₆ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (↑r₁ : k) • (p₂ -ᵥ p₁)
pos₇ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = (↑r₁ : k) • (p₃ -ᵥ p₂) + (p₅ -ᵥ p₄)
pos₈ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = r₂ • (p₃ -ᵥ p₂) + (p₅ -ᵥ p₄)
⊢ p₄ -ᵥ p₆ = (↑r₁ : k) • (p₁ -ᵥ p₃)
have pos₉ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = p₆ -ᵥ p₅ + (p₅ -ᵥ p₄)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
have rw : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) (r₃ • (p₁ -ᵥ p₃))
Tactic: rw [hr₁, hr₂, add_comm, vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, neg_mem_iff, ← hr₃]