-- 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 ι
n : ι →₀ ℕ
r : S
y₁ y₂ : MvPolynomial ι S
hy₁ :
  (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := Q.Ring) ((monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S) y₁) =
    HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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]) ((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) ((monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S) y₂) =
    HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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]) ((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) ((monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S) (y₁ + y₂)) =
    HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
have monomial : HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R]) +
    (HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])) =
  HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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 (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((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]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) y₂
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R]))
Tactic: simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]