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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁
hi₂ : i ∉ fs₂
⊢ i ∈ (↑fs₁ : Set ι)

Tactic:
simpa using 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁
hi₂ : i ∉ fs₂
h : (↑fs₂ : Set ι).indicator w₂ i = 0
⊢ w₁ i = 0

Tactic:
rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]

Premises used: Set.indicator_of_mem
-- 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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
ha : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
i : ι
hi : i ∈ fs₁
hi₂ : i ∉ fs₂
⊢ (↑fs₂ : Set ι).indicator w₂ i = 0

Tactic:
simp [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 ι
p' : P
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) →
    (∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
      ∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₂ ∧
          ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w

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
s1 s2 : Set ι
p0 : P
hp0s1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1)) p0
hp0s2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s2)) p0
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1) ⊓ affineSpan k (p '' s2)) p0

Tactic:
have hp0' : p0 ∈ affineSpan k (p '' s1) ⊓ affineSpan k (p '' s2) := ⟨hp0s1, hp0s2⟩
-- 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
s1 s2 : Set ι
p0 : P
hp0s1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1)) p0
hp0s2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s2)) p0
hp0' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1) ⊓ affineSpan k (p '' s2)) p0
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s1 ∩ s2))) p0

Tactic:
rw [ha.inf_affineSpan_eq_affineSpan_inter] at hp0'

Premises used: AffineIndependent.inf_affineSpan_eq_affineSpan_inter
-- 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
s1 s2 : Set ι
p0 : P
hp0s1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1)) p0
hp0s2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s2)) p0
hp0' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s1 ∩ s2))) p0
by_contra : ∀ (he : ¬(s1 ∩ s2).Nonempty), False
⊢ (s1 ∩ s2).Nonempty

Tactic:
by_contra 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
s1 s2 : Set ι
p0 : P
hp0s1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1)) p0
hp0s2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s2)) p0
hp0' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s1 ∩ s2))) p0
he : ¬(s1 ∩ s2).Nonempty
⊢ s1 ∩ s2 = ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at he

Premises used: Set.not_nonempty_iff_eq_empty
-- 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
s1 s2 : Set ι
p0 : P
hp0s1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s1)) p0
hp0s2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s2)) p0
hp0' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s1 ∩ s2))) p0
he : s1 ∩ s2 = ∅
⊢ False

Tactic:
simp [he, AffineSubspace.notMem_bot] at hp0'

Premises used: AffineSubspace.notMem_bot
-- 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
s1 s2 : Set ι
hd : Disjoint s1 s2
⊢ Disjoint (↑(affineSpan k (p '' s1)) : Set P) (↑(affineSpan k (p '' s2)) : Set P)

Tactic:
Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- 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
s1 s2 : Set ι
hd : Disjoint s1 s2
refine :
  ∀ (p0 : P) (hp0s1 : p0 ∈ (↑(affineSpan k (p '' s1)) : Set P)) (hp0s2 : p0 ∈ (↑(affineSpan k (p '' s2)) : Set P)),
    False
⊢ Disjoint (↑(affineSpan k (p '' s1)) : Set P) (↑(affineSpan k (p '' s2)) : Set P)

Tactic:
refine Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- 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
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ (↑(affineSpan k (p '' s1)) : Set P)
hp0s2 : p0 ∈ (↑(affineSpan k (p '' s2)) : Set P)
obtain : ∀ (i : ι) (hi : i ∈ s1 ∩ s2), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := ha.exists_mem_inter_of_exists_mem_inter_affineSpan hp0s1 hp0s2

Premises used: AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan
-- 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
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ (↑(affineSpan k (p '' s1)) : Set P)
hp0s2 : p0 ∈ (↑(affineSpan k (p '' s2)) : Set P)
i : ι
hi : i ∈ s1 ∩ s2
⊢ False

Tactic:
Set.disjoint_iff.1 hd hi

Premises used: Set.Mem, Iff.mp, Set.disjoint_iff
-- 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
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ (↑(affineSpan k (p '' s1)) : Set P)
hp0s2 : p0 ∈ (↑(affineSpan k (p '' s2)) : Set P)
i : ι
hi : i ∈ s1 ∩ s2
⊢ False

Tactic:
exact Set.disjoint_iff.1 hd hi

Premises used: Iff.mp, Set.disjoint_iff
-- 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
i : ι
s : Set ι
mp : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i) → i ∈ s
mpr : i ∈ s → Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i) ↔ i ∈ s

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
i : ι
s : Set ι
hs : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
⊢ ∃ (i_1 : ι), i_1 ∈ s ∩ {i}

Tactic:
have h :=
      AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
        (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
-- 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
i : ι
s : Set ι
hs : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
h : ∃ (i_1 : ι), i_1 ∈ s ∩ {i}
mp : ∀ (h : (s ∩ {i}).Nonempty), i ∈ s
mp₁ mp₂ mp₃ mp₄ : ∀ (h : i ∈ s), i ∈ s
⊢ i ∈ s

Tactic:
rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h

Premises used: Set.nonempty_def, Set.inter_singleton_nonempty
-- 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
i : ι
s : Set ι
⊢ i ∈ s → Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)

Tactic:
fun h => mem_affineSpan k (Set.mem_image_of_mem p h)

Premises used: mem_affineSpan, Set.mem_image_of_mem
-- 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
i : ι
s : Set ι
⊢ i ∈ s → Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)

Tactic:
exact fun h => mem_affineSpan k (Set.mem_image_of_mem p h)

Premises used: mem_affineSpan, Set.mem_image_of_mem
-- 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
i : ι
s : Set ι
⊢ p i ∉ affineSpan k (p '' (s \ {i}))

Tactic:
simp [ha]
-- 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
by_contra :
  ∀ (hn : ¬Injective.{u_4 + 1, u_3 + 1} (β := AffineSubspace k P) fun (s : Set ι) ↦ affineSpan k (p '' s)), False
⊢ Injective.{u_4 + 1, u_3 + 1} (β := AffineSubspace k P) fun (s : Set ι) ↦ affineSpan k (p '' s)

Tactic:
by_contra hn
-- 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
hn : ¬Injective.{u_4 + 1, u_3 + 1} (β := AffineSubspace k P) fun (s : Set ι) ↦ affineSpan k (p '' s)
⊢ ∃ (a : Set ι) (b : Set ι), Eq (α := AffineSubspace k P) (affineSpan k (p '' a)) (affineSpan k (p '' b)) ∧ a ≠ b

Tactic:
rw [not_injective_iff] at hn

Premises used: Function.not_injective_iff
-- 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
hn : ∃ (a : Set ι) (b : Set ι), Eq (α := AffineSubspace k P) (affineSpan k (p '' a)) (affineSpan k (p '' b)) ∧ a ≠ b
obtain :
  ∀ (s₁ s₂ : Set ι) (hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂)))
    (hne : s₁ ≠ s₂), False
⊢ False

Tactic:
obtain ⟨s₁, s₂, hs₁₂, hne⟩ := hn
-- 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 ι
hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂))
hne : s₁ ≠ s₂
apply : s₁ = s₂
⊢ False

Tactic:
apply hne
-- 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 ι
hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂))
hne : s₁ ≠ s₂
h : ∀ (i : ι), i ∈ s₁ ↔ i ∈ s₂
⊢ s₁ = s₂

Tactic:
ext i
-- 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 ι
hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂))
hne : s₁ ≠ s₂
i : ι
h :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁)) (p i) ↔
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₂)) (p i)
⊢ i ∈ s₁ ↔ i ∈ s₂

Tactic:
simp_rw [← ha.mem_affineSpan_iff, hs₁₂]

Premises used: AffineIndependent.mem_affineSpan_iff
-- 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₁.Subsingleton
⊢ s₁.Nontrivial

Tactic:
rw [Set.not_subsingleton_iff] at h₁

Premises used: Set.not_subsingleton_iff
-- 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
obtain :
  ∀ (j : ι) (hj : j ∈ s₁) (hne : j ≠ i), Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
⊢ Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))

Tactic:
obtain ⟨j, hj, hne⟩ := h₁.exists_ne i

Premises used: Set.Nontrivial.exists_ne
-- 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 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (p '' s₁)) (p i -ᵥ p j)

Tactic:
have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ 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 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
hs : Membership.mem (γ := Submodule k V) (vectorSpan k (p '' s₁)) (p i -ᵥ p j)
⊢ ∃ (s : Finset (↑s₂ : Type u_4)) (w : (↑s₂ : Type u_4) → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧
      p i -ᵥ p j =
        (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
            (a : (↑s₂ : Type u_4) → k) → V)
          w

Tactic:
rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs

Premises used: mem_vectorSpan_iff_eq_weightedVSub, Set.image_eq_range
-- 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 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
hs :
  ∃ (s : Finset (↑s₂ : Type u_4)) (w : (↑s₂ : Type u_4) → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧
      p i -ᵥ p j =
        (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
            (a : (↑s₂ : Type u_4) → k) → V)
          w
obtain :
  ∀ (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),
    False
⊢ False

Tactic:
obtain ⟨fs, w, hw, hs⟩ := hs
-- 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 : 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
simp : Eq.{u_1 + 1} (α := k) (∑ x ∈ fs, w' (↑x : ι)) (∑ i ∈ fs, w i)
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0

Tactic:
simp only [sum_map, Embedding.subtype_apply, ← hw]

Premises used: Finset.sum_map, Function.Embedding.subtype_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 ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : 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
t : { x : ι // x ∈ s₂ }
ht : t ∈ fs
⊢ w' (↑t : ι) = w t

Tactic:
simp [w']
-- 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 : 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
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ fs, w' (↑x : ι)) (∑ i ∈ fs, w i)

Tactic:
exact sum_congr rfl fun t ht ↦ by simp [w']

Premises used: Finset.sum_congr, 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 ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : 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
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0

Tactic:
have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']
-- 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 : 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
rw :
  Eq.{u_2 + 1} (α := V)
    ((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 :
      V)
    ((fs.weightedVSub (p ∘ (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s₂) : (a : { x : ι // x ∈ s₂ }) → ι)) :
          (a : { x : ι // x ∈ s₂ } → k) → V)
        (w' ∘ (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s₂) : (a : { x : ι // x ∈ s₂ }) → ι)) :
      V)
⊢ p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'

Tactic:
rw [hs, weightedVSub_map]

Premises used: Finset.weightedVSub_map