-- 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 ι
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])
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])
⊢ (δ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])

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

Premises used: Algebra.Generators.algebraMap_apply, mul_assoc, MvPolynomial.monomial, TensorProduct.tmul_smul, Finsupp.prod_add_index', pow_add, Algebra.Generators.H1Cotangent.δAux_monomial, map_add, pow_zero, Derivation.leibniz, TensorProduct.smul_tmul', MvPolynomial.monomial_mul, add_smul, TensorProduct.tmul_add, Algebra.smul_def, mul_add, implies_true, MvPolynomial.aeval_monomial, smul_add