-- 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
haas : a ∉ insert a s
⊢ False

Tactic:
apply haas

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
haas : a ∉ insert a s
⊢ a ∈ insert a s

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
haas : a ∉ insert a s
⊢ a ∈ insert a s

Tactic:
exact Finset.mem_insert_self a s

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
⊢ a ∉ insert a s → g a • ⇑a = 0

Tactic:
intro haas

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
haas : 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
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - a x * 0 y = 0 - a x * 0

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 ∈ insert a s
hia : i ≠ a
⊢ g i • ⇑i = 0

Tactic:
rw [Finset.mem_insert] at his

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 = a ∨ i ∈ 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
⊢ 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) =
    ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y

Tactic:
rw [Finset.sum_insert has, Finset.sum_insert has]

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
haas : a ∉ insert a s
⊢ g a • ⇑a = 0

Tactic:
exfalso

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
haas : a ∉ insert a s
⊢ False

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 = g i * a y

Tactic:
exact h

Result:
no goals