-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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) ((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])
monomial :
  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]) +
      (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])) =
    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 (α := 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]) +
        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:
simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]

Premises used: map_add, add_smul, mul_add, smul_add