-- 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:
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

Tactic:
intro i his hia

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
i : G →* L
his : i ∈ insert a s
hia : i ≠ a
⊢ g i • ⇑i = 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
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * i (x * y) - ∑ i ∈ insert a s, a x * (g i * i y) =
    ∑ c ∈ insert a s, (g c • ⇑c) (x * y) - ∑ i ∈ insert a s, a x * (g i • ⇑i) y

Tactic:
rfl

Result:
no goals

Proof state:
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
i : G →* L
his : i = a ∨ i ∈ s
hia : i ≠ a
⊢ g i • ⇑i = 0

Tactic:
rw [h3 i (his.resolve_left hia), zero_smul]

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 ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y = 0 - a x * 0

Tactic:
rw [hg]

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
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - a x * 0 y = 0 - a x * 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
h3 : ∀ i ∈ s, g i = 0
⊢ g a * 1 = (g a • ⇑a) 1

Tactic:
rw [← a.map_one]

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
h3 : ∀ i ∈ s, g i = 0
⊢ g a * a 1 = (g a • ⇑a) 1

Proof state:
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)

Tactic:
rw [map_mul, mul_assoc]

Result:
no goals

Proof state:
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)

Tactic:
rw [mul_assoc, mul_left_comm]

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
⊢ (∑ i ∈ insert a s, g i • ⇑i) 1 = 0

Tactic:
rw [hg]

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
h3 : ∀ i ∈ s, g i = 0
⊢ 0 1 = 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)
⊢ LinearIndependent L fun f => ⇑f

Tactic:
letI : MulAction L L := DistribMulAction.toMulAction

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
⊢ LinearIndependent L fun f => ⇑f