-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem linearIndependent_monoidHom (G : Type*) [Monoid G] (L : Type*) [CommRing L]
    [NoZeroDivisors L] : LinearIndependent L (M := G → L) (fun f => f : (G →* L) → G → L)

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y =
    ∑ i ∈ insert a s, g i * i (x * y) - ∑ i ∈ insert a s, a x * (g i * i y)

Tactic:
congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_

Result:
case refine_1
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i✝ : G →* L
his : i✝ ∈ s
x y : G
i : G →* L
⊢ g i * i x * i y = g i * i (x * y)

case refine_2
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i✝ : G →* L
his : i✝ ∈ s
x y : G
i : G →* L
⊢ g i * a x * i y = a x * (g i * i y)

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ 0 1 = 0

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ g a * a 1 = (g a • ⇑a) 1

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ s, g i * i x * i y - ∑ i ∈ s, g i * a x * i y =
    g a * a x * a y + ∑ i ∈ s, g i * i x * i y - (g a * a x * a y + ∑ i ∈ s, g i * a x * i y)

Tactic:
rw [add_sub_add_left_eq_sub]

Result:
no goals

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
⊢ LinearIndependent L fun f => ⇑f

Tactic:
letI := Classical.decEq (G →* L)

Result:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this : DecidableEq (G →* L) := Classical.decEq (G →* L)
⊢ LinearIndependent L fun f => ⇑f

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ 0 - a x * 0 = 0

Tactic:
rw [mul_zero, sub_zero]

Result:
no goals

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (∑ i ∈ insert a s, g i • ⇑i) 1

Tactic:
rw [Finset.sum_eq_single a]

Result:
case h₀
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ ∀ b ∈ insert a s, b ≠ a → g b • ⇑b = 0

case h₁
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ a ∉ insert a s → g a • ⇑a = 0

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • i y = g i • a y
⊢ g i * (i y - a y) = 0

Tactic:
rw [mul_sub, sub_eq_zero]

Result:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • i y = g i • a y
⊢ g i * i y = g i * a y