awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
apply :
  Function.Injective (α := T ⊗[S] P.toExtension.CotangentSpace) (β :=
    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
⊢ Function.Injective (α := T ⊗[S] P.toExtension.CotangentSpace) (β := Extension.CotangentSpace (toExtension (Q.comp P)))
    (⇑((↑(LinearEquiv.symm (compEquiv Q P)) :
            Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
              (Q.comp P).toExtension.CotangentSpace) ∘ₗ
          LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)

Tactic:
apply (compEquiv Q P).symm.injective.comp

Premises used: LinearEquiv.symm, Algebra.Generators.CotangentSpace.compEquiv, Function.Injective.comp, LinearEquiv.injective
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Injective (α := T ⊗[S] P.toExtension.CotangentSpace) (β :=
    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)

Tactic:
Prod.mk_right_injective _

Premises used: Function.prod, Prod.mk_right_injective
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Injective (α := T ⊗[S] P.toExtension.CotangentSpace) (β :=
    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)

Tactic:
exact Prod.mk_right_injective _

Premises used: Prod.mk_right_injective
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
rw :
  Function.Surjective (α := Extension.CotangentSpace (toExtension (Q.comp P))) (β := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
          (↑(compEquiv Q P) :
            (Q.comp P).toExtension.CotangentSpace →ₗ[T]
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
⊢ Function.Surjective (α := Extension.CotangentSpace (toExtension (Q.comp P))) (β := Q.toExtension.CotangentSpace)
    (⇑(Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
rw [← fst_compEquiv]

Premises used: Algebra.Generators.CotangentSpace.fst_compEquiv
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Surjective (α := Extension.CotangentSpace (toExtension (Q.comp P))) (β := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
          (↑(compEquiv Q P) :
            (Q.comp P).toExtension.CotangentSpace →ₗ[T]
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
(Prod.fst_surjective).comp (compEquiv Q P).surjective

Premises used: Prod.fst_surjective, Algebra.Generators.CotangentSpace.compEquiv, LinearEquiv.surjective, Function.Surjective.comp
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Surjective (α := Extension.CotangentSpace (toExtension (Q.comp P))) (β := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
          (↑(compEquiv Q P) :
            (Q.comp P).toExtension.CotangentSpace →ₗ[T]
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
exact (Prod.fst_surjective).comp (compEquiv Q P).surjective

Premises used: Prod.fst_surjective, Algebra.Generators.CotangentSpace.compEquiv, LinearEquiv.surjective, Function.Surjective.comp
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
rw :
  Function.Exact (M := T ⊗[S] P.toExtension.CotangentSpace) (N := Extension.CotangentSpace (toExtension (Q.comp P)))
    (P := Q.toExtension.CotangentSpace)
    (⇑((↑(LinearEquiv.symm (compEquiv Q P)) :
            Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
              (Q.comp P).toExtension.CotangentSpace) ∘ₗ
          LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
          (↑(compEquiv Q P) :
            (Q.comp P).toExtension.CotangentSpace →ₗ[T]
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
⊢ Function.Exact (M := T ⊗[S] P.toExtension.CotangentSpace) (N := Extension.CotangentSpace (toExtension (Q.comp P)))
    (P := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)))) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
    (⇑(Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
rw [← fst_compEquiv, ← compEquiv_symm_inr]

Premises used: Algebra.Generators.CotangentSpace.compEquiv_symm_inr, Algebra.Generators.CotangentSpace.fst_compEquiv
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
rw :
  Function.Exact (M := T ⊗[S] P.toExtension.CotangentSpace) (N :=
    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) (P := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
⊢ Function.Exact (M := T ⊗[S] P.toExtension.CotangentSpace) (N := Extension.CotangentSpace (toExtension (Q.comp P)))
    (P := Q.toExtension.CotangentSpace)
    (⇑((↑(LinearEquiv.symm (compEquiv Q P)) :
            Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
              (Q.comp P).toExtension.CotangentSpace) ∘ₗ
          LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
          (↑(LinearEquiv.symm (LinearEquiv.symm (compEquiv Q P))) :
            (Q.comp P).toExtension.CotangentSpace →ₗ[T]
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
rw [LinearEquiv.conj_exact_iff_exact]

Premises used: LinearEquiv.conj_exact_iff_exact
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Exact (M := T ⊗[S] P.toExtension.CotangentSpace) (N :=
    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) (P := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
Function.Exact.inr_fst

Premises used: Function.Exact.inr_fst
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Exact (M := T ⊗[S] P.toExtension.CotangentSpace) (N :=
    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) (P := Q.toExtension.CotangentSpace)
    (⇑(LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace)) :
      (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)

Tactic:
exact Function.Exact.inr_fst

Premises used: Function.Exact.inr_fst
-- 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
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
    ((n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])

Tactic:
Finsupp.lsum_single _ _ _ _

Premises used: Finsupp.lsum_single, TensorProduct.tmul, AddCon.toQuotient, Finsupp.single
-- 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 ι
i : ι
rw :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((Finsupp.prod (Finsupp.single i 1) fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) 1) 0
⊢ Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (X i) : T ⊗[S] Ω[S⁄R]) (0 : T ⊗[S] Ω[S⁄R])

Tactic:
rw [X, δAux_monomial]

Premises used: MvPolynomial.X, Algebra.Generators.H1Cotangent.δAux_monomial
-- 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 ι
i : ι
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((Finsupp.prod (Finsupp.single i 1) fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) 1) 0

Tactic:
simp only [Derivation.map_one_eq_zero, tmul_zero]

Premises used: Derivation.map_one_eq_zero, TensorProduct.tmul_zero
-- 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
m : ι →₀ ℕ
s : S
monomial :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) r : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) s : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R]) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) r : T)
            (HMul.hMul (α := T) (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
            (HMul.hMul (α := T) (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R])
⊢ (δ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])

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

Premises used: Algebra.Generators.algebraMap_apply, mul_assoc, TensorProduct.tmul_smul, Algebra.Generators.H1Cotangent.δAux_monomial, Derivation.leibniz, TensorProduct.smul_tmul', MvPolynomial.monomial_mul, TensorProduct.tmul_add, Algebra.smul_def, MvPolynomial.aeval_monomial
-- 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
m : ι →₀ ℕ
s : S
monomial :
  HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) r : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) s : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R]) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) r : T)
            (HMul.hMul (α := T) (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
            (HMul.hMul (α := T) (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R])
⊢ HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) r : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) s : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R]) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) r : T)
            (HMul.hMul (α := T) (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
            (HMul.hMul (α := T) (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R])

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

Premises used: mul_comm, Finsupp.prod
-- 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
m : ι →₀ ℕ
s : S
⊢ HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) r : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) s : T)
            ((n + m).prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2 : T) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R]) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) r : T)
            (HMul.hMul (α := T) (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) s :
        T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
            (HMul.hMul (α := T) (n.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)
              (m.prod fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2)) ⊗ₜ[S]
          (D R S : (a : S) → Ω[S⁄R]) r :
        T ⊗[S] Ω[S⁄R])

Tactic:
simp only [pow_zero, implies_true, pow_add, Finsupp.prod_add_index']

Premises used: Finsupp.prod_add_index', pow_add, pow_zero, implies_true
-- 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) ((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])
⊢ 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:
abel