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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
⊢ (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) ↔
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
have refine : (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) →
  ∀ (t : Finset ι) (hst : t ⊆ s) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i))
    (i : ι) (hi : i ∈ s) (hfi : ¬f i = 0),
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
Tactic: refine ⟨fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ?_,
    fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ⟨t, hst, f, heq, i, hst hi, hfi⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
have pos : ∀ (hi' : i ∈ t),
  ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
Tactic: by_cases hi' : i ∈ t
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
pos :
  ∀ (hi' : i ∈ t),
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
have neg : ∀ (hi' : i ∉ t),
  ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
Tactic: by_cases hi' : i ∈ t
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
have neg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s \ t, f i • v i) (∑ i ∈ s \ (s \ t), f i • v i)
Tactic: refine ⟨s \ t, Finset.sdiff_subset, f, ?_, i, Finset.mem_sdiff.2 ⟨hi, hi'⟩, hfi⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
hv : LinearIndependent R v
f g : ι →₀ R
h :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R (-v) : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R (-v) : (a : ι →₀ R) → M) g : M)
⊢ f = g
have h₁ : Eq.{u_4 + 1} (α := M) (f.sum fun (a : ι) (b : R) ↦ b • v a) (g.sum fun (a : ι) (b : R) ↦ b • v a)
Tactic: simp only [Finsupp.linearCombination_apply, Pi.neg_apply, smul_neg, Finsupp.sum_neg, neg_inj] at h
Cleared hypotheses: h
-- 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
hv : LinearIndependent R v
f g : ι →₀ R
h : Eq.{u_4 + 1} (α := M) (f.sum fun (a : ι) (b : R) ↦ b • v a) (g.sum fun (a : ι) (b : R) ↦ b • v a)
⊢ f = g
have h₁ : ∀ (m : ι), Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) m : R) ((g : (a : ι) → R) m : R)
Tactic: ext m
-- 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
⊢ LinearIndependent R (-v) ↔ LinearIndependent R v
have refine : ∀ (h : LinearIndependent R (-v)), LinearIndependent R v
Tactic: refine ⟨fun h ↦ ?_, LinearIndependent.neg⟩
-- 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
⊢ LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
have rw : (∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
  ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [linearIndependent_iff'ₛ]
-- 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 ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
have refine_1 : ∀
  (h :
    ∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
  (s : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
Tactic: refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩
-- 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
refine_1 :
  ∀
    (h :
      ∀ (s : Finset ι) (f g : ι → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
    (s : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
⊢ (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
have refine_2 : ∀ (h : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) (s : Finset ι)
  (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
Tactic: refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩
-- 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 : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
have a : (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (0 i) (v i)) →
    ∀ i ∈ s, f i = 0 i
Tactic: convert! h s f 0
-- 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 : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (0 i) (v i)) →
      ∀ i ∈ s, f i = 0 i
have a : (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ x ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x)) → ∀ i ∈ s, f i = 0
Tactic: simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]
-- 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 : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
a :
  (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ x ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x)) →
      ∀ i ∈ s, f i = 0
⊢ (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (0 i) (v i)) →
      ∀ i ∈ s, f i = 0 i
have a₁ : (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ x ∈ s, 0) → ∀ i ∈ s, f i = 0
Tactic: simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]
-- 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 : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
have refine_2 : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i
Tactic: rw [← sub_eq_zero, ← Finset.sum_sub_distrib]
-- 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 : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i
have a : (Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i) ↔
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s, (f - g) i • v i) 0 → ∀ i ∈ s, (f - g) i = 0
Tactic: convert! h s (f - g) using 3
-- 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 : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
simp_rw simp_rw₁ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (if x ∈ s then g x else 0) • v x) 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then g j else 0) i) (v i)) 0
have simp_rw₂ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then g x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x)) 0
Tactic: simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]
-- 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 : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
simp_rw simp_rw₁ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (if x ∈ s then g x else 0) • v x) 0
simp_rw₂ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then g x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x)) 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then g j else 0) i) (v i)) 0
have simp_rw₃ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then g x • v x else 0) 0
Tactic: simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]
-- 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 : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ g i = 0
have h : g i = if i ∈ s then g i else 0
Tactic: convert!
        H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) 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
⊢ ¬LinearIndependent R v ↔ ∃ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 ∧ ∃ i ∈ s, g i ≠ 0
have rw : (¬∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) ↔
  ∃ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 ∧ ∃ i ∈ s, g i ≠ 0
Tactic: rw [linearIndependent_iff']
-- 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
inst_3 : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
have H : ∀ (H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0) (s : Finset ι) (g : ι → R)
  (hg : ∀ i ∉ s, g i = 0) (hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι),
  Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0
Tactic: refine
    ⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
      linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩
-- 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
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
⊢ Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0
have rw : Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) (∑ i ∈ s, g i • v i)
Tactic: rw [← hs]
-- 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
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
⊢ Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) (∑ i ∈ s, g i • v i)
have refine : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ∀ (hi : i ∉ s), g i • v i = 0
Tactic: refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm
-- 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
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i_1 i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ s
⊢ g i • v i = 0
have rw : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
Tactic: rw [hg i hi, zero_smul]
-- 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
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i_1 i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ s
rw : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
⊢ g i • v i = 0
have rw₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [hg i hi, zero_smul]
-- 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 ι
⊢ 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 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
Tactic: simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
-- 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 ι
⊢ (∀ (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
have 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
Tactic: constructor
-- 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 ι
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
⊢ (∀ (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
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: constructor
-- 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 ι
hv :
  ∀ (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
hf : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0
i : ι
hi : i ∈ s
⊢ f i = 0
have mp : ∀ (hf : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) 0) (i : ι) (hi : i ∈ s), f i = 0
Tactic: rw [← s.sum_attach] at hf
Cleared hypotheses: hf, i, hi
-- 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 ι
⊢ 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 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
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
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
⊢ 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 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
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
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
⊢ 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 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
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