-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
zero :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (0 ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((0 : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
add :
  ∀ (f₁ f₂ : ι →₀ M)
    (hf₁ :
      Eq (α := M ⊗[R] N)
        (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                    (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                  (f₁ ⊗ₜ[R] g) :
                ι × κ →₀ M ⊗[R] N) :
              (a : ι × κ) → M ⊗[R] N)
            (i, k) :
          M ⊗[R] N)
        ((f₁ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N))
    (hf₂ :
      Eq (α := M ⊗[R] N)
        (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                    (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                  (f₂ ⊗ₜ[R] g) :
                ι × κ →₀ M ⊗[R] N) :
              (a : ι × κ) → M ⊗[R] N)
            (i, k) :
          M ⊗[R] N)
        ((f₂ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)),
    Eq (α := M ⊗[R] N)
      (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                  (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                ((f₁ + f₂) ⊗ₜ[R] g) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((f₁ + f₂ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (f ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
have single : ∀ (i' : ι) (m : M),
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
Tactic: induction f using Finsupp.induction_linear with
  | zero => simp
  | add f₁ f₂ hf₁ hf₂ => simp [add_tmul, hf₁, hf₂]
  | single i' m =>
    induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp
Cleared hypotheses: f