awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₃}) p₁
hne : p₁ ≠ p₃
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₁, p₃}) (affineSpan k {p₂, p₃})

Tactic:
affineSpan_pair_eq_of_mem_of_mem_of_ne h (right_mem_affineSpan_pair _ _ _) hne

Premises used: affineSpan_pair_eq_of_mem_of_mem_of_ne, right_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₃}) p₁
hne : p₁ ≠ p₂
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₂, p₁}) (affineSpan k {p₂, p₃})

Tactic:
affineSpan_pair_eq_of_mem_of_mem_of_ne (left_mem_affineSpan_pair _ _ _) h hne.symm

Premises used: affineSpan_pair_eq_of_mem_of_mem_of_ne, Ne.symm, left_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁}))
⊢ ∃ (z : kˣ), z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄

Tactic:
rw [affineSpan_pair_parallel_iff_exists_unit_smul'] at h₁₂₄₅

Premises used: AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁}))
h₁₂₄₆ : ∃ (z : kˣ), z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₅, p₆})) (direction (P := P) (affineSpan k {p₂, p₃}))

Tactic:
rw [affineSpan_pair_parallel_iff_exists_unit_smul'] at h₁₂₄₅

Premises used: AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁}))
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₃}))
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₆, p₄})) (direction (P := P) (affineSpan k {p₃, p₁}))

Tactic:
rw [affineSpan_pair_parallel_iff_exists_unit_smul'] at h₁₂₄₅

Premises used: AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁}))
⊢ ∃ (z : k), z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅

Tactic:
rw [direction_affineSpan_pair_le_iff_exists_smul] at h₂₃₅₆ h₃₁₆₄

Premises used: AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₅
⊢ ∃ (z : k), z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆

Tactic:
rw [direction_affineSpan_pair_le_iff_exists_smul] at h₂₃₅₆ h₃₁₆₄

Premises used: AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₆
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₃)
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
obtain ⟨r₁, hr₁⟩ := h₁₂₄₅
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₄
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₃)
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
obtain ⟨r₂, hr₂⟩ := h₂₃₅₆
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₅
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₃)
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
obtain ⟨r₃, hr₃⟩ := h₃₁₆₄
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₆
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₃)
⊢ ∃ (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₁

Premises used: Units.smul_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃)
neg :
  ∀ (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₃)

Tactic:
by_cases h : (r₁ : k) = r₂

Premises used: Units.val
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃)

Tactic:
⟨r₁, r₁.ne_zero, hr₁.symm, h ▸ hr₂.symm, ?_⟩

Premises used: Units.val, Eq.rec, Units.ne_zero, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃)
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
refine ⟨r₁, r₁.ne_zero, hr₁.symm, h ▸ hr₂.symm, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₄)
pos₉ pos₁₀ : p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = p₆ -ᵥ p₅ + (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₂]

Premises used: vsub_add_vsub_cancel, smul_neg, neg_inj, neg_vsub_eq_vsub_rev, smul_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
neg : False
⊢ ∃ (r : k), r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
rw : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) (r₃ • (p₁ -ᵥ p₃))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))

Tactic:
rw [hr₁, hr₂, add_comm, vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, neg_mem_iff, ← hr₃]

Premises used: neg_mem_iff, vsub_add_vsub_cancel, add_comm, neg_vsub_eq_vsub_rev
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃ • (p₁ -ᵥ p₃))

Tactic:
smul_vsub_mem_vectorSpan_pair _ _ _

Premises used: smul_vsub_mem_vectorSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃ • (p₁ -ᵥ p₃))

Tactic:
exact smul_vsub_mem_vectorSpan_pair _ _ _

Premises used: smul_vsub_mem_vectorSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂))

Tactic:
have h₁₂ : (r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [hr₁, hr₂, add_comm, vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, neg_mem_iff, ← hr₃]
      exact smul_vsub_mem_vectorSpan_pair _ _ _
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
rw : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₃ -ᵥ p₁))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))

Tactic:
rw [add_comm, ← smul_add, vsub_add_vsub_cancel]

Premises used: vsub_add_vsub_cancel, add_comm, smul_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₃ -ᵥ p₁))

Tactic:
smul_vsub_rev_mem_vectorSpan_pair _ _ _

Premises used: Set.Mem, smul_vsub_rev_mem_vectorSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₃ -ᵥ p₁))

Tactic:
exact smul_vsub_rev_mem_vectorSpan_pair _ _ _

Premises used: smul_vsub_rev_mem_vectorSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))

Tactic:
have h₁₁ : (r₁ : k) • (p₂ -ᵥ p₁) + (r₁ : k) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [add_comm, ← smul_add, vsub_add_vsub_cancel]
      exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))

Tactic:
simpa [sub_smul] using sub_mem h₁₂ h₁₁

Premises used: sub_smul, sub_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))

Tactic:
have h₂₁ : (r₂ - r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      simpa [sub_smul] using sub_mem h₁₂ h₁₁
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))
rwa : r₂ ≠ (↑r₁ : k)
rwa₁ rwa₂ rwa₃ rwa₄ : (↑r₁ : k) ≠ r₂
⊢ r₂ - (↑r₁ : k) ≠ 0

Tactic:
rwa [sub_ne_zero, ne_comm]

Premises used: sub_ne_zero, ne_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₃}) p₂

Tactic:
rw [Submodule.smul_mem_iff _ (by rwa [sub_ne_zero, ne_comm]), ← direction_affineSpan,
      vsub_left_mem_direction_iff_mem (right_mem_affineSpan_pair _ _ _)] at h₂₁

Premises used: direction_affineSpan, right_mem_affineSpan_pair, Submodule.smul_mem_iff, AffineSubspace.vsub_left_mem_direction_iff_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₃}) p₂
⊢ False

Tactic:
h₂ h₂₁
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₃}) p₂
⊢ False

Tactic:
exact h₂ h₂₁
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ Eq (α := Submodule k V) (vectorSpan k s) (Submodule.span k (s -ᵥ s))

Tactic:
rfl

Premises used: vectorSpan, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : Set P
h : s₁ ⊆ s₂
⊢ LE.le (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂)

Tactic:
Submodule.span_mono (vsub_self_mono h)

Premises used: Set.Mem, Set.vsub_self_mono, Submodule.span_mono