-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
y : Q.Ring
n : ι →₀ ℕ
r : S
monomial :
  ∀ (m : ι →₀ ℕ) (s : S),
    (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
        (HMul.hMul (α := Q.Ring) (β := Q.Ring)
          ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
          ((MvPolynomial.monomial m : (a : S) → MvPolynomial ι S) s : MvPolynomial ι S)) =
      HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R])
          ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.monomial m : (a : S) → MvPolynomial ι S) s) :
            T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R])
          ((MvPolynomial.monomial m : (a : S) → MvPolynomial ι S) s : MvPolynomial ι S)
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r) :
            T ⊗[S] Ω[S⁄R])
⊢ (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := Q.Ring) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S) y) =
    HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R])
        ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) y
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r) :
          T ⊗[S] Ω[S⁄R])
have monomial₁ : ∀ (y₁ y₂ : MvPolynomial ι S)
  (hy₁ :
    (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
        (HMul.hMul (α := Q.Ring) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S) y₁) =
      HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R])
          ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) y₁ : T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) y₁
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r) :
            T ⊗[S] Ω[S⁄R]))
  (hy₂ :
    (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
        (HMul.hMul (α := Q.Ring) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S) y₂) =
      HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R])
          ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) y₂ : T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) y₂
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r) :
            T ⊗[S] Ω[S⁄R])),
  (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := Q.Ring) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
        (y₁ + y₂)) =
    HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R])
        ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (y₁ + y₂) : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (y₁ + y₂)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.monomial n : (a : S) → MvPolynomial ι S) r) :
          T ⊗[S] Ω[S⁄R])
Tactic: induction y using MvPolynomial.induction_on' with
    | monomial m s =>
      simp only [monomial_mul, δAux_monomial, Derivation.leibniz, tmul_add, tmul_smul,
        smul_tmul', Algebra.smul_def, algebraMap_apply, aeval_monomial, mul_assoc]
      rw [mul_comm (m.prod _) (n.prod _)]
      simp only [pow_zero, implies_true, pow_add, Finsupp.prod_add_index']
    | add y₁ y₂ hy₁ hy₂ => simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]; abel
Cleared hypotheses: y