awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R I) f
have supp_f₁ : (↑f.support : Set ι) ⊆ I ∪ {i}
Tactic: simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
Cleared hypotheses: supp_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
supp_f : (↑f.support : Set ι) ⊆ I ∪ {i}
x : ι
hx : x ∈ (↑f.support : Set ι)
⊢ x ∈ I
have refine : ¬x = i
Tactic: refine (memJ.mp (supp_f hx)).resolve_left ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
Tactic: have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have right : Membership.mem (γ := Submodule R M) (span R (v '' I))
  (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
Tactic: use f i, hfi
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
have hfi' : i ∈ f.support
Tactic: have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
have sum_f₁ : HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
  -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
Tactic: rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
Cleared hypotheses: sum_f, f_ne, hfi, hfi'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
have right : Membership.mem (γ := Submodule R M) (span R (v '' I))
  (-∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x))
Tactic: rw [sum_f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (-∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x))
have right : ∀ (c : ι) (hc : c ∈ f.support.erase i), c ∈ I
Tactic: refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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 : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have rcases : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
  ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
Tactic: classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
rcases :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
    ∃ (s : Set ι),
      LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have right : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
  ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
rcases :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
    ∃ (s : Set ι),
      LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
right right₁ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t)
    (i : ι) (hi : i ∉ I), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have right₂ : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I)
  (hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}),
  ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
rcases :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
    ∃ (s : Set ι),
      LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
right right₁ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t)
    (i : ι) (hi : i ∉ I), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
right₂ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I)
    (hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}),
    ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have right₃ : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I),
  let J := I ∪ {i};
  ∀ (hImaximal : LinearIndepOn R v J → I = J) (hJ : J = I ∪ {i}),
    ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
rcases :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
    ∃ (s : Set ι),
      LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
right right₁ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t)
    (i : ι) (hi : i ∉ I), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
right₂ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I)
    (hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}),
    ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
right₃ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I),
    let J := I ∪ {i};
    ∀ (hImaximal : LinearIndepOn R v J → I = J) (hJ : J = I ∪ {i}),
      ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have right₄ : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I),
  let J := I ∪ {i};
  ∀ (hImaximal : LinearIndepOn R v J → I = J) (hJ : J = I ∪ {i}) (memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I),
    ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (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
rcases :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
    ∃ (s : Set ι),
      LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
right right₁ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t)
    (i : ι) (hi : i ∉ I), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
right₂ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I)
    (hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}),
    ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
right₃ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I),
    let J := I ∪ {i};
    ∀ (hImaximal : LinearIndepOn R v J → I = J) (hJ : J = I ∪ {i}),
      ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
right₄ :
  ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I),
    let J := I ∪ {i};
    ∀ (hImaximal : LinearIndepOn R v J → I = J) (hJ : J = I ∪ {i}) (memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I),
      ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have right₅ : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (i : ι) (hi : i ∉ I),
  let J := I ∪ {i};
  ∀ (hImaximal : LinearIndepOn R v J → I = J) (hJ : J = I ∪ {i}) (memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I)
    (hiJ : i ∈ J), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_6
M : Type u_7
L : Type u_8
inst : CommSemiring K
inst_1 : Semiring M
inst_2 : Algebra K M
inst_3 : CommRing L
inst_4 : IsDomain L
inst_5 : Algebra K L
⊢ LinearIndependent (ι := M →ₐ[K] L) L AlgHom.toLinearMap
have apply : LinearIndependent (ι := M →ₐ[K] L) L (M := M → L) ((⇑(ltoFun K M L L) : (a : M →ₗ[K] L) → M → L) ∘ AlgHom.toLinearMap)
Tactic: apply LinearIndependent.of_comp (LinearMap.ltoFun K M L L)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
⊢ Injective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have refine : ∀ (x : M) (hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)), x = 0
Tactic: refine (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
x : M
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
have rw : Membership.mem (γ := Submodule R M) ⊤ x
Tactic: rw [hv]