-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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 _
s : Finset (G →* L)
empty :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ ∅, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 →
      ∀ (i : G →* L), Membership.mem (γ := Finset (G →* L)) ∅ i → g i = 0
insert :
  ∀ (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),
    Eq (α := G → L) (∑ i ∈ Insert.insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 →
      ∀ i ∈ Insert.insert a s, g i = 0
⊢ ∀ (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

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
  intro g hg
  -- Here
  -- * `a` is a new character we will insert into the `Finset` of characters `s`,
  -- * `ih` is the fact that only the trivial linear combination of characters in `s` is zero
  -- * `hg` is the fact that `g` are the coefficients of a linear combination summing to zero
  -- and it remains to prove that `g` vanishes on `insert a s`.
  -- We now make the key calculation:
  -- For any character `i` in the original `Finset`, we have `g i • i = g i • a` as functions
  -- on the monoid `G`.
  have h1 (i) (his : i ∈ s) : (g i • i : G → L) = g i • a := by
    ext x
    rw [← sub_eq_zero]
    apply ih (fun j => g j * j x - g j * a x) _ i his
    ext y
    -- After that, it's just a chase scene.
    calc
      (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp
  -- On the other hand, since `a` is not already in `s`, for any character `i ∈ s`
  -- there is some element of the monoid on which it differs from `a`.
  have h2 (i) (his : i ∈ s) : ∃ y, i y ≠ a y := by
    by_contra! hia
    obtain rfl : i = a := MonoidHom.ext hia
    contradiction
  -- From these two facts we deduce that `g` actually vanishes on `s`,
  have h3 (i) (his : i ∈ s) : g i = 0 := by
    let ⟨y, hy⟩ := h2 i his
    have h : g i • i y = g i • a y := congr_fun (h1 i his) y
    rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
    exact h.resolve_right (sub_ne_zero_of_ne hy)
  -- And so, using the fact that the linear combination over `s` and over `insert a s` both
  -- vanish, we deduce that `g a = 0`.
  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
  -- Now we're done; the last two facts together imply that `g` vanishes on every element
  -- of `insert a s`.
  exact (Finset.forall_mem_insert ..).2 ⟨h4, h3⟩

Premises used: Insert.insert