-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
rw₁ :
  Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        (f : (a : R) → S)
          (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
rw₂ rw₃ rw₄ :
  Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := S) (β := S)
        ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S))
rw₅ :
  ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
    (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
      HMul.hMul (α := S) (β := S)
        ((coeff x.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff x.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
have rw₆ : ∀ (i j : σ →₀ ℕ),
  (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n →
    (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
      HMul.hMul (α := S) (β := S)
        ((coeff (i, j).1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff (i, j).2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S)
Tactic: classical
        rw [coeff_mul, map_sum, coeff_mul]
        apply Finset.sum_congr rfl
        rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl