-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
j : ι →₀ ℕ
this :
  Eq (α := Generators.Ring (Q.comp P))
    ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring)
        ((monomial j : (a : R) → MvPolynomial ι R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x)) :
      Generators.Ring (Q.comp P))
    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)
h :
  Eq (α := MvPolynomial (ι' ⊕ ι) R)
    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)
    ((monomial
            (HAdd.hAdd (α := ι' ⊕ ι →₀ ℕ) (β := ι' ⊕ ι →₀ ℕ)
              ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0) : ι' ⊕ ι →₀ ℕ)
              ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j) : ι' ⊕ ι →₀ ℕ)) :
          (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (1 * coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)
h₁ :
  Eq (α := MvPolynomial (ι' ⊕ ι) R)
    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)
    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) ((i, 0) + (0, j))) :
          (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (1 * coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)
⊢ (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
        MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
        MvPolynomial (ι' ⊕ ι) R)
have h₃ : Eq (α := MvPolynomial (ι' ⊕ ι) R)
  ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
    MvPolynomial (ι' ⊕ ι) R)
  ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i + 0, 0 + j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (1 * coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
    MvPolynomial (ι' ⊕ ι) R)
Tactic: rw [monomial_mul, ← map_add, Prod.mk_add_mk, add_zero, zero_add, one_mul]