awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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 :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
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)
⊢ ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)
have ha₁ : (↑fs₁ : Set ι).indicator w₁ = (↑fs₂ : Set ι).indicator w₂
Tactic: replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)
have h : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁ ∩ fs₂, w₁ i) 1
Tactic: refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁ ∩ fs₂, w₁ i) 1
⊢ ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)
have h₁ : Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
  ((affineCombination k (fs₁ ∩ fs₂) p : (a : ι → k) → P) w₁ : P)
Tactic: refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁ ∩ fs₂, w₁ i) 1
have h : HAdd.hAdd (α := k) (∑ x ∈ fs₁ ∩ fs₂, w₁ x) (∑ x ∈ fs₁ \ fs₂, w₁ x) = ∑ i ∈ fs₁ ∩ fs₂, w₁ i
Tactic: rw [← hw₁, ← fs₁.sum_inter_add_sum_diff fs₂, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ HAdd.hAdd (α := k) (∑ x ∈ fs₁ ∩ fs₂, w₁ x) (∑ x ∈ fs₁ \ fs₂, w₁ x) = ∑ i ∈ fs₁ ∩ fs₂, w₁ i
have h : Eq.{u_1 + 1} (α := k) (∑ x ∈ fs₁ \ fs₂, w₁ x) 0
Tactic: convert! add_zero _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ fs₁ \ fs₂, w₁ x) 0
have h : ∀ x ∈ fs₁ \ fs₂, w₁ x = 0
Tactic: refine Finset.sum_eq_zero ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₁ \ fs₂
⊢ w₁ i = 0
have h : (↑fs₁ : Set ι).indicator w₁ i = 0
Tactic: rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₁ \ fs₂
h : (↑fs₁ : Set ι).indicator w₁ i = 0
⊢ w₁ i = 0
have h₁ : (↑fs₂ : Set ι).indicator w₂ i = 0
Tactic: rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₁ \ fs₂
h : (↑fs₁ : Set ι).indicator w₁ i = 0
h₁ : (↑fs₂ : Set ι).indicator w₂ i = 0
⊢ w₁ i = 0
have h₂ : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k (fs₁ ∩ fs₂) p : (a : ι → k) → P) w₁ : P)
have h : Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
  ((affineCombination k fs₁ p : (a : ι → k) → P) ((↑(fs₁ ∩ fs₂) : Set ι).indicator w₁) : P)
Tactic: rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₁ p : (a : ι → k) → P) ((↑(fs₁ ∩ fs₂) : Set ι).indicator w₁) : P)
have h : ∀ i ∈ fs₁, w₁ i = (↑(fs₁ ∩ fs₂) : Set ι).indicator w₁ i
Tactic: refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₁
⊢ w₁ i = (↑(fs₁ ∩ fs₂) : Set ι).indicator w₁ i
have h : w₁ i = if i ∈ (↑fs₂ : Set ι) then w₁ i else 0
Tactic: rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₁
⊢ w₁ i = if i ∈ (↑fs₂ : Set ι) then w₁ i else 0
have h : i ∉ fs₂ → w₁ i = 0
Tactic: simp only [mem_coe, left_eq_ite_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂
⊢ w₁ i = 0
have h : (↑fs₂ : Set ι).indicator w₂ i = 0
Tactic: rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 ι
⊢ Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) (affineSpan k (p '' (s₁ ∩ s₂)))
have h : ∀ (p' : P),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) p' ↔
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s₁ ∩ s₂))) p'
Tactic: classical
  ext p'
  simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]
  constructor
  · rintro ⟨⟨fs₁, hfs₁, w₁, hw₁, rfl⟩, ⟨fs₂, hfs₂, w₂, hw₂, hw₁₂⟩⟩
    rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
    replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
    refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
    · rw [← hw₁, ← fs₁.sum_inter_add_sum_diff fs₂, eq_comm]
      convert! add_zero _
      refine Finset.sum_eq_zero ?_
      intro i hi
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
    · rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
      refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
      intro i hi
      rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
      simp only [mem_coe, left_eq_ite_iff]
      intro hi₂
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
      simp [hi₂]
  · grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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' : P),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) p' ↔
      Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s₁ ∩ s₂))) p'
⊢ Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) (affineSpan k (p '' (s₁ ∩ s₂)))
have h₁ : ∀ (p' : P),
  ((∃ (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) ↔
    ∃ (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
Tactic: classical
  ext p'
  simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]
  constructor
  · rintro ⟨⟨fs₁, hfs₁, w₁, hw₁, rfl⟩, ⟨fs₂, hfs₂, w₂, hw₂, hw₁₂⟩⟩
    rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
    replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
    refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
    · rw [← hw₁, ← fs₁.sum_inter_add_sum_diff fs₂, eq_comm]
      convert! add_zero _
      refine Finset.sum_eq_zero ?_
      intro i hi
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
    · rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
      refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
      intro i hi
      rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
      simp only [mem_coe, left_eq_ite_iff]
      intro hi₂
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
      simp [hi₂]
  · grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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' : P),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) p' ↔
      Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s₁ ∩ s₂))) p'
h₁ :
  ∀ (p' : P),
    ((∃ (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) ↔
      ∃ (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
⊢ Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) (affineSpan k (p '' (s₁ ∩ s₂)))
have h₂ : ∀ (p' : P),
  ((∃ (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) →
    ∃ (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
Tactic: classical
  ext p'
  simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]
  constructor
  · rintro ⟨⟨fs₁, hfs₁, w₁, hw₁, rfl⟩, ⟨fs₂, hfs₂, w₂, hw₂, hw₁₂⟩⟩
    rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
    replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
    refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
    · rw [← hw₁, ← fs₁.sum_inter_add_sum_diff fs₂, eq_comm]
      convert! add_zero _
      refine Finset.sum_eq_zero ?_
      intro i hi
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
    · rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
      refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
      intro i hi
      rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
      simp only [mem_coe, left_eq_ite_iff]
      intro hi₂
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
      simp [hi₂]
  · grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ ∃ (i : ι), i ∈ s1 ∩ s2
have hp0' : 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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ ∃ (i : ι), i ∈ s1 ∩ s2
have hp0'₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s1 ∩ s2))) p0
Tactic: rw [ha.inf_affineSpan_eq_affineSpan_inter] at hp0'
Cleared hypotheses: hp0'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ (s1 ∩ s2).Nonempty
have by_contra : ∀ (he : ¬(s1 ∩ s2).Nonempty), False
Tactic: by_contra he
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ False
have he₁ : s1 ∩ s2 = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
have refine : ∀ (p0 : P) (hp0s1 : p0 ∈ (↑(affineSpan k (p '' s1)) : Set P)) (hp0s2 : p0 ∈ (↑(affineSpan k (p '' s2)) : Set P)), False
Tactic: refine Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
⊢ False
have obtain : ∀ (i : ι) (hi : i ∈ s1 ∩ s2), False
Tactic: obtain ⟨i, hi⟩ := ha.exists_mem_inter_of_exists_mem_inter_affineSpan hp0s1 hp0s2