-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
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
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
single :
  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] 0) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (0 : (a : κ) → N) k : M ⊗[R] N)
single₁ :
  ∀ (g₁ g₂ : κ →₀ N)
    (hg₁ :
      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))
    (hg₂ :
      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)),
    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₁ + g₂)) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₁ + g₂ : (a : κ) → N) k : M ⊗[R] N)
single₂ :
  ∀ (k' : κ) (n : N),
    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] Finsupp.single k' n) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (Finsupp.single k' n : (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)
              (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 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

Premises used: Prod.mk_inj, LinearMap.single, finsuppTensorFinsupp_single, TensorProduct.tmul_add, Finsupp.single_apply, Submodule.zero, ite_and, Submodule.add