awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0

Tactic:
have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
⊢ Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w''' : V) (0 : V)

Tactic:
simp [w''', ← hs'', hi, hj]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
⊢ Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w''' : V) (0 : V)

Tactic:
have hs''' : fs'.weightedVSub p w''' = 0 := by
    simp [w''', ← hs'', hi, hj]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
hs''' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w''' : V) (0 : V)
⊢ w''' i = 0

Tactic:
have h0 := ha fs' w''' hw''' hs''' i hi
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
hs''' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w''' : V) (0 : V)
h0 : w''' i = 0
⊢ False

Tactic:
simp [w''', w'', Pi.sub_apply, hne.symm, his₂] at h0

Premises used: Ne.symm, Pi.sub_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
mp :
  Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)) →
    s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
mpr :
  s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton →
    Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)) ↔
    s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
pos : ∀ (he : s₁ = s₂), s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
neg : ∀ (he : ¬s₁ = s₂), s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
by_cases he : s₁ = s₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : s₁ = s₂
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
simp [he]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
neg : s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
simp only [he, false_or]

Premises used: false_or
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
pos : ∀ (h₁ : s₁.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
neg : ∀ (h₁ : ¬s₁.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
by_cases h₁ : s₁.Subsingleton

Premises used: Set.Subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ (p '' s₂).Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, eq_comm, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
h₂ : (p '' s₂).Subsingleton
⊢ ¬s₁ = s₂

Tactic:
rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, eq_comm, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
h₂ : (p '' s₂).Subsingleton
he₁ : ¬s₁ = s₂
⊢ s₁.Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, eq_comm, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : (p '' s₂).Subsingleton
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
⟨h₁, Set.subsingleton_of_image ha.injective s₂ h⟩

Premises used: Set.subsingleton_of_image, AffineIndependent.injective, And.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : (p '' s₂).Subsingleton
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
exact ⟨h₁, Set.subsingleton_of_image ha.injective s₂ h⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
pos : ∀ (h₂ : s₂.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
neg : ∀ (h₂ : ¬s₂.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
by_cases h₂ : s₂.Subsingleton

Premises used: Set.Subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ (p '' s₁).Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
h₃ : (p '' s₁).Subsingleton
⊢ ¬s₁ = s₂

Tactic:
rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
h₃ : (p '' s₁).Subsingleton
he₁ : ¬s₁ = s₂
⊢ ¬s₁.Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
h₃ : (p '' s₁).Subsingleton
he₁ : ¬s₁ = s₂
h₄ : ¬s₁.Subsingleton
⊢ s₂.Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h

Premises used: vectorSpan_eq_bot_iff_subsingleton, Set.Subsingleton.image, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : (p '' s₁).Subsingleton
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
⟨Set.subsingleton_of_image ha.injective s₁ h, h₂⟩

Premises used: Set.subsingleton_of_image, AffineIndependent.injective, And.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : (p '' s₁).Subsingleton
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
exact ⟨Set.subsingleton_of_image ha.injective s₁ h, h₂⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
neg : False
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
simp only [h₁, h₂, false_and]

Premises used: false_and
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
⊢ (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
⊢ (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁

Tactic:
have hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁ := by grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁
neg : ∀ (i : ι) (his₁ : i ∈ s₁) (his₂ : i ∉ s₂), False
neg₁ : ∀ (i : ι) (his₂ : i ∈ s₂) (his₁ : i ∉ s₁), False
⊢ False

Tactic:
rcases hi with ⟨i, his₁, his₂⟩ | ⟨i, his₂, his₁⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
⊢ False

Tactic:
ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₁ his₂ h₁ h

Premises used: _private.0.AffineIndependent.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
⊢ False

Tactic:
exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₁ his₂ h₁ h

Premises used: _private.0.AffineIndependent.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₂ : i ∈ s₂
his₁ : i ∉ s₁
⊢ False

Tactic:
ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₂ his₁ h₂ h.symm

Premises used: _private.0.AffineIndependent.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₂ : i ∈ s₂
his₁ : i ∉ s₁
⊢ False

Tactic:
exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₂ his₁ h₂ h.symm

Premises used: _private.0.AffineIndependent.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
mpr : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₁))
mpr₁ :
  ∀ (h₁ : s₁.Subsingleton) (h₂ : s₂.Subsingleton),
    Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))

Tactic:
rcases h with rfl | ⟨h₁, h₂⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ : Set ι
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₁))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h₁ : s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))

Tactic:
simp [h₁.image p, h₂.image p, vectorSpan_of_subsingleton]

Premises used: Set.Subsingleton.image, vectorSpan_of_subsingleton