awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1 =
    (∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) 1
have rw : ∀ x ∈ s, HSMul.hSMul (β := (a : G) → L) (g x) (⇑x : (a : G) → L) = 0
Tactic: rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ Eq.{u_7 + 1} (α := L) ((∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) 1) 0
have rw : Eq.{u_7 + 1} (α := L) (0 1) 0
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ ∀ i ∈ insert a s, g i = 0
have h4 : g a = 0
Tactic: have h4 : g a = 0 :=
    calc
      g a = g a * 1 := (mul_one _).symm
      _ = (g a • a : G → L) 1 := by rw [← a.map_one]; rfl
      _ = (∑ i ∈ insert a s, g i • i : G → L) 1 := by
        rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
        simp +contextual [h3]
      _ = 0 := by rw [hg]; rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
v : ι → M
inst_5 : Unique ι
⊢ LinearIndependent R v ↔ v default ≠ 0
have refine : LinearIndependent R v → v default ≠ 0
Tactic: refine ⟨?_, .of_subsingleton _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
have inl : ∀ (he : IsEmpty ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic: obtain (he | he) := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
inl : ∀ (he : IsEmpty ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
have inr : ∀ (he : Nonempty ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic: obtain (he | he) := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
have inr : ∀ (val : Unique ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic: obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
val : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
have inr : f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
Tactic: rw [linearIndependent_unique_iff]
-- 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
hv : LinearIndependent R v
i : ι
⊢ Injective.{u_2 + 1, u_4 + 1} (β := M) fun (r : R) ↦ r • v i
have h : ∀ (x : R), x • v i = comp (β := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) (Finsupp.single i) x
Tactic: convert! hv.comp (Finsupp.single_injective i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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 : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ False
have this : Eq (α := ι →₀ R) (Finsupp.single i 1) 0
Tactic: have := @hv (Finsupp.single i 1 : ι →₀ R) 0 (by simpa using h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
f : ι → M
⊢ LinearIndependent R f ↔ IsEmpty ι
have rw : LinearIndependent.{u', u_2, u_4} (ι := ι) R (M := M) 0 ↔ IsEmpty ι
Tactic: rw [Subsingleton.elim f 0, linearIndependent_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
f : ι → M
rw : LinearIndependent.{u', u_2, u_4} (ι := ι) R (M := M) 0 ↔ IsEmpty ι
⊢ LinearIndependent R f ↔ IsEmpty ι
have rw₁ : IsEmpty ι ↔ IsEmpty ι
Tactic: rw [Subsingleton.elim f 0, linearIndependent_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
⊢ f i = g i
have h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
Tactic: have h :=
        hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
⊢ f i = (Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single i (f i))
have rw : f i = (Finsupp.single i (f i) : (a : ι) → R) i
Tactic: rw [Finsupp.lapply_apply, Finsupp.single_eq_same]
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
rw : f i = (Finsupp.single i (f i) : (a : ι) → R) i
⊢ f i = (Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single i (f i))
have rw₁ : f i = f i
Tactic: rw [Finsupp.lapply_apply, Finsupp.single_eq_same]
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
⊢ f i = (Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single i (f i))
have rw : f i = (Finsupp.single i (f i) : (a : ι) → R) i
Tactic: { rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
rw : f i = (Finsupp.single i (f i) : (a : ι) → R) i
⊢ f i = (Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single i (f i))
have rw₁ : f i = f i
Tactic: { rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ Eq.{u_2 + 1} (α := R) ((Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single j (f j)) : R) (0 : R)
have rw : Eq.{u_2 + 1} (α := R) ((Finsupp.single j (f j) : (a : ι) → R) i : R) (0 : R)
Tactic: rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji]
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
rw : Eq.{u_2 + 1} (α := R) ((Finsupp.single j (f j) : (a : ι) → R) i : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single j (f j)) : R) (0 : R)
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
⊢ f i = g i
have this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i
Tactic: have (f : ι → R) : f i = (∑ j ∈ s, Finsupp.single j (f j)) i :=
        calc
          f i = (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single i (f i)) := by
            { rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }
          _ = ∑ j ∈ s, (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single j (f j)) :=
            Eq.symm <|
              Finset.sum_eq_single i
                (fun j _hjs hji => by rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji])
                fun hnis => hnis.elim his
          _ = (∑ j ∈ s, Finsupp.single j (f j)) i := (map_sum ..).symm
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i
⊢ f i = g i
have rw : (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i = g i
Tactic: rw [this f, this g, h]
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i
rw : (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i = g i
⊢ f i = g i
have rw₁ : Eq.{u_2 + 1} (α := R) ((∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i : R)
  ((∑ j ∈ s, Finsupp.single j (g j) : (a : ι) → R) i : R)
Tactic: rw [this f, this g, h]
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i
rw : (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i = g i
rw₁ :
  Eq.{u_2 + 1} (α := R) ((∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i : R)
    ((∑ j ∈ s, Finsupp.single j (g j) : (a : ι) → R) i : R)
⊢ f i = g i
have rw₂ : Eq.{u_2 + 1} (α := R) ((∑ i ∈ s, Finsupp.single i (g i) : (a : ι) → R) i : R)
  ((∑ j ∈ s, Finsupp.single j (g j) : (a : ι) → R) i : R)
Tactic: rw [this f, this g, h]
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have refine_1 : ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)),
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
Tactic: refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
refine_1 :
  ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)),
    Eq.{u_4 + 1} (α := M)
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have refine_2 : ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)), x ∈ f.support ∪ g.support
Tactic: refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
have refine_1 : ∀ x ∈ f.support ∪ g.support, x ∉ g.support → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) x : R) (v x) = 0
Tactic: rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right]
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
refine_1 :
  ∀ x ∈ f.support ∪ g.support, x ∉ g.support → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) x : R) (v x) = 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
have refine_1₁ : ∀ x ∈ f.support ∪ g.support, x ∉ f.support → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x) = 0
Tactic: rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right]
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
i : ι
hi : i ∉ g.support
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i) = 0
have refine_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
Tactic: rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
i : ι
hi : i ∉ g.support
refine_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i) = 0
have refine_1₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
i : ι
hi : i ∉ f.support
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) = 0
have refine_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
Tactic: rw [Finsupp.notMem_support_iff.mp hi, zero_smul]