-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δAux_mul (x y) :
    δAux R Q (x * y) = x • (δAux R Q y) + y • (δAux R Q x)

Proof state:
case h1.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
m : Q.vars →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 => Q.val x1 ^ x2) * m.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((m.prod fun x1 x2 => Q.val x1 ^ x2) * n.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r

Tactic:
rw [mul_comm (m.prod _) (n.prod _)]

Result:
case h1.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
m : Q.vars →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 => Q.val x1 ^ x2) * m.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((n.prod fun x1 x2 => Q.val x1 ^ x2) * m.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r

Proof state:
case h1.h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
y₁ y₂ : MvPolynomial Q.vars S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (δAux R Q) ((monomial n) r * (y₁ + y₂)) =
    (monomial n) r • (δAux R Q) (y₁ + y₂) + (y₁ + y₂) • (δAux R Q) ((monomial n) r)

Tactic:
simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]

Result:
case h1.h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
y₁ y₂ : MvPolynomial Q.vars S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r) +
      ((monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)) =
    (monomial n) r • (δAux R Q) y₁ + (monomial n) r • (δAux R Q) y₂ +
      (y₁ • (δAux R Q) ((monomial n) r) + y₂ • (δAux R Q) ((monomial n) r))

Proof state:
case h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
y : Q.Ring
x₁ x₂ : MvPolynomial Q.vars S
hx₁ : (δAux R Q) (x₁ * y) = x₁ • (δAux R Q) y + y • (δAux R Q) x₁
hx₂ : (δAux R Q) (x₂ * y) = x₂ • (δAux R Q) y + y • (δAux R Q) x₂
⊢ x₁ • (δAux R Q) y + y • (δAux R Q) x₁ + (x₂ • (δAux R Q) y + y • (δAux R Q) x₂) =
    x₁ • (δAux R Q) y + x₂ • (δAux R Q) y + (y • (δAux R Q) x₁ + y • (δAux R Q) x₂)

Tactic:
abel

Result:
no goals

Proof state:
case h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
y : Q.Ring
n : Q.vars →₀ ℕ
r : S
⊢ (δAux R Q) ((monomial n) r * y) = (monomial n) r • (δAux R Q) y + y • (δAux R Q) ((monomial n) r)

Tactic:
induction' y using MvPolynomial.induction_on' with m s y₁ y₂ hy₁ hy₂

Result:
case h1.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
m : Q.vars →₀ ℕ
s : S
⊢ (δAux R Q) ((monomial n) r * (monomial m) s) =
    (monomial n) r • (δAux R Q) ((monomial m) s) + (monomial m) s • (δAux R Q) ((monomial n) r)

case h1.h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
y₁ y₂ : MvPolynomial Q.vars S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (δAux R Q) ((monomial n) r * (y₁ + y₂)) =
    (monomial n) r • (δAux R Q) (y₁ + y₂) + (y₁ + y₂) • (δAux R Q) ((monomial n) r)

Proof state:
case h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
y : Q.Ring
x₁ x₂ : MvPolynomial Q.vars S
hx₁ : (δAux R Q) (x₁ * y) = x₁ • (δAux R Q) y + y • (δAux R Q) x₁
hx₂ : (δAux R Q) (x₂ * y) = x₂ • (δAux R Q) y + y • (δAux R Q) x₂
⊢ (δAux R Q) ((x₁ + x₂) * y) = (x₁ + x₂) • (δAux R Q) y + y • (δAux R Q) (x₁ + x₂)

Tactic:
simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]

Result:
case h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
y : Q.Ring
x₁ x₂ : MvPolynomial Q.vars S
hx₁ : (δAux R Q) (x₁ * y) = x₁ • (δAux R Q) y + y • (δAux R Q) x₁
hx₂ : (δAux R Q) (x₂ * y) = x₂ • (δAux R Q) y + y • (δAux R Q) x₂
⊢ x₁ • (δAux R Q) y + y • (δAux R Q) x₁ + (x₂ • (δAux R Q) y + y • (δAux R Q) x₂) =
    x₁ • (δAux R Q) y + x₂ • (δAux R Q) y + (y • (δAux R Q) x₁ + y • (δAux R Q) x₂)

Proof state:
case h1.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
m : Q.vars →₀ ℕ
s : S
⊢ (δAux R Q) ((monomial n) r * (monomial m) s) =
    (monomial n) r • (δAux R Q) ((monomial m) s) + (monomial m) s • (δAux R Q) ((monomial n) r)

Tactic:
simp only [monomial_mul, δAux_monomial, Derivation.leibniz, tmul_add, tmul_smul,
  smul_tmul', smul_eq_mul, Algebra.smul_def, algebraMap_apply, aeval_monomial, mul_assoc]

Result:
case h1.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
m : Q.vars →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 => Q.val x1 ^ x2) * m.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((m.prod fun x1 x2 => Q.val x1 ^ x2) * n.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r