awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
simp_rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
simp_rw₁ :
  (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) ↔
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
mp :
  (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) →
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
⊢ LinearIndepOn R v (↑s : Set ι) ↔ ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
have mpr : (∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) →
  ∀ (g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
      ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0
Tactic: classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
  constructor
  · rintro hv f hf i hi
    rw [← s.sum_attach] at hf
    exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩
  · rintro hv f hf₀ i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (l : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0
f : ι →₀ R
hf : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f
g : ι →₀ R
hg : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) g
eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (f - g) : M) (0 : M)
have rw : HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
  0
Tactic: rw [map_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (l : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0
f : ι →₀ R
hf : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f
g : ι →₀ R
hg : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) g
eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
rw :
  HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
    0
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (f - g) : M) (0 : M)
have rw₁ : HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
  0
Tactic: rw [map_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (l : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0
f : ι →₀ R
hf : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f
g : ι →₀ R
hg : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) g
eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
rw :
  HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
    0
rw₁ :
  HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
    0
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (f - g) : M) (0 : M)
have rw₂ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [map_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔
    Disjoint (α := Submodule R (ι →₀ R)) (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
have rw : (∀ (l : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0) ↔
  Disjoint (α := Submodule R (ι →₀ R)) (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
Tactic: rw [linearIndepOn_iff, LinearMap.disjoint_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (∀ (l : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
        Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0) ↔
    Disjoint (α := Submodule R (ι →₀ R)) (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
⊢ LinearIndepOn R v s ↔
    Disjoint (α := Submodule R (ι →₀ R)) (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
have rw₁ : (∀ (l : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0) ↔
  ∀ (x : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) x →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M) (0 : M) → x = 0
Tactic: rw [linearIndepOn_iff, LinearMap.disjoint_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have rw : (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
  ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
Tactic: rw [LinearIndepOn, linearIndependent_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have refine_1 : ∀
  (h :
    ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
  (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
  (hit : i ∈ t), g i = 0
Tactic: refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
refine_1 :
  ∀
    (h :
      ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
    (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
    (hit : i ∈ t), g i = 0
⊢ (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have refine_2 : ∀ (h : ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0)
  (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
  (i : (↑s : Type u')) (hit : i ∈ t), g i = 0
Tactic: refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
⊢ g i = 0
have refine_1 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ t.preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) sorry,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : (↑s : Type u')) ↦ g (↑i : ι)) i) (v (↑i : ι)))
  0
Tactic: refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t.preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ⋯,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : (↑s : Type u')) ↦ g (↑i : ι)) i) (v (↑i : ι)))
    0
have refine_1 : ∀ x ∈ t, x ∉ range (ι := { x : ι // x ∈ s }) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) → g x • v x = 0
Tactic: rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
⊢ ∀ x ∈ t, x ∉ range (ι := { x : ι // x ∈ s }) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) → g x • v x = 0
have refine_1 : ∀ x ∈ t, x ∉ s → g x • v x = 0
Tactic: simp only [Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
t : Finset (↑s : Type u')
g : (↑s : Type u') → R
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0
i : (↑s : Type u')
hit : i ∈ t
⊢ g i = 0
have h₁ : ∀ (i : ι) (hi : i ∈ s),
  Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi ∈ t → ∀ (h : i ∈ s), g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) = 0
Tactic: replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have rw : (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
  ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
Tactic: classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have rw₁ : (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
  ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
Tactic: classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
rw₁ rw₂ rw₃ :
  (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have refine_1 : ∀
  (h :
    ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
  (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
  (hit : i ∈ t), g i = 0
Tactic: classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
rw₁ rw₂ rw₃ :
  (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
refine_1 :
  ∀
    (h :
      ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
    (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
    (hit : i ∈ t), g i = 0
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have refine_2 : ∀ (h : ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0)
  (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
  (i : (↑s : Type u')) (hit : i ∈ t), g i = 0
Tactic: classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
rw₁ rw₂ rw₃ :
  (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
refine_1 :
  ∀
    (h :
      ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
    (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
    (hit : i ∈ t), g i = 0
refine_2 refine_2₁ :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0)
    (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
    (i : (↑s : Type u')) (hit : i ∈ t), g i = 0
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
have refine_2₂ : ∀ (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
  (i : (↑s : Type u')) (hit : i ∈ t)
  (h :
    ∀ (i : ι) (hi : i ∈ s),
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi ∈ t →
        ∀ (h : i ∈ s), g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) = 0),
  g i = 0
Tactic: classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
⊢ l = 0
have h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
⊢ Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
have h : Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
Tactic: simp only [Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
⊢ Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
have h : ∀ (hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ False
have h : Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i})))
  (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i))
Tactic: refine hn (H i _ ?_)