-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Finsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
inst_7 : Fintype ι'
f : ((i : ι) → κ i) × ι' →₀ R
x : (i : ι) → Finsupp.{u_4, u_3} (κ i) R
zero :
  Eq (α := ι' →₀ R)
    (((freeFinsuppEquiv (κ := κ) :
              (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
            0 :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((0 : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)
add :
  ∀ (f g : ((i : ι) → κ i) × ι' →₀ R)
    (hf :
      Eq (α := ι' →₀ R)
        ((((freeFinsuppEquiv (κ := κ) :
                    (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
                  f :
                MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
              (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
            x :
          ι' →₀ R)
        (∑ p : ((i : ι) → κ i) × ι',
            HSMul.hSMul (α := R) (β := ι' →₀ R) ((f : (a : ((i : ι) → κ i) × ι') → R) p : R)
              (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
          ι' →₀ R))
    (hg :
      Eq (α := ι' →₀ R)
        ((((freeFinsuppEquiv (κ := κ) :
                    (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
                  g :
                MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
              (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
            x :
          ι' →₀ R)
        (∑ p : ((i : ι) → κ i) × ι',
            HSMul.hSMul (α := R) (β := ι' →₀ R) ((g : (a : ((i : ι) → κ i) × ι') → R) p : R)
              (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
          ι' →₀ R)),
    Eq (α := ι' →₀ R)
      ((((freeFinsuppEquiv (κ := κ) :
                  (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
                (f + g) :
              MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
            (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
          x :
        ι' →₀ R)
      (∑ p : ((i : ι) → κ i) × ι',
          HSMul.hSMul (α := R) (β := ι' →₀ R) ((f + g : (a : ((i : ι) → κ i) × ι') → R) p : R)
            (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
        ι' →₀ R)
⊢ Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              f :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((f : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)
have single : ∀ (p : ((i : ι) → κ i) × ι') (r : R),
  Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              (Finsupp.single p r) :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p_1 : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((Finsupp.single p r : (a : ((i : ι) → κ i) × ι') → R) p_1 : R)
          (Finsupp.single p_1.2 (∏ i : ι, (x i : (a : κ i) → R) (p_1.1 i))) :
      ι' →₀ R)
Tactic: induction f using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [hf, hg, add_mul, Finset.sum_add_distrib]
  | single p r => simp [Finsupp.single_apply]
Cleared hypotheses: f