awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ 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)
have 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)
Tactic: rw [← fst_compEquiv, ← compEquiv_symm_inr]
-- 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ 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)
have 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)
Tactic: rw [LinearEquiv.conj_exact_iff_exact]
-- 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 ι
i : ι
⊢ 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])
have 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
Tactic: rw [X, δAux_monomial]
-- 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
m : ι →₀ ℕ
s : S
⊢ (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := Q.Ring) (β := Q.Ring) ((monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
        ((monomial m : (a : S) → MvPolynomial ι S) s : MvPolynomial ι S)) =
    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]) ((monomial m : (a : S) → MvPolynomial ι S) s) : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((monomial m : (a : S) → MvPolynomial ι S) s : MvPolynomial ι S)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((monomial n : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
have 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])
Tactic: simp only [monomial_mul, δAux_monomial, Derivation.leibniz, tmul_add, tmul_smul,
        smul_tmul', Algebra.smul_def, algebraMap_apply, aeval_monomial, mul_assoc]
-- 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
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) (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])
have 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])
Tactic: rw [mul_comm (m.prod _) (n.prod _)]
-- 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 ι
y : Q.Ring
n : ι →₀ ℕ
r : S
⊢ (δ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])
have monomial : ∀ (m : ι →₀ ℕ) (s : S),
  (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
      (HMul.hMul (α := Q.Ring) (β := Q.Ring) ((monomial n : (a : S) → MvPolynomial ι S) r : MvPolynomial ι S)
        ((monomial m : (a : S) → MvPolynomial ι S) s : MvPolynomial ι S)) =
    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]) ((monomial m : (a : S) → MvPolynomial ι S) s) : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (α := Q.Ring) (β := T ⊗[S] Ω[S⁄R]) ((monomial m : (a : S) → MvPolynomial ι S) s : MvPolynomial ι S)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((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
Cleared hypotheses: y
-- 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 ι
y : Q.Ring
x₁ x₂ : MvPolynomial ι S
hx₁ :
  (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (x₁ * y) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₁ ((δ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]) x₁ : T ⊗[S] Ω[S⁄R])
hx₂ :
  (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (x₂ * y) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₂ ((δ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]) x₂ : T ⊗[S] Ω[S⁄R])
⊢ (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((x₁ + x₂) * y) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (x₁ + x₂) ((δ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]) (x₁ + x₂) : T ⊗[S] Ω[S⁄R])
have add : HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₁ ((δ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]) x₁ : T ⊗[S] Ω[S⁄R]) +
    (HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₂ ((δ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]) x₂ : T ⊗[S] Ω[S⁄R])) =
  HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₁ ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) y : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₂ ((δ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]) x₁ : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) y ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) x₂ : T ⊗[S] Ω[S⁄R]))
Tactic: simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]
-- 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 ι
x y : Q.Ring
⊢ (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (x * y) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x ((δ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]) x : T ⊗[S] Ω[S⁄R])
have monomial : ∀ (n : ι →₀ ℕ) (r : S),
  (δ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])
Tactic: induction x using MvPolynomial.induction_on' with
  | monomial n r =>
    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
  | add x₁ x₂ hx₁ hx₂ => simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]; abel
Cleared hypotheses: x
-- 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 ι
x y : Q.Ring
monomial :
  ∀ (n : ι →₀ ℕ) (r : S),
    (δ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]) (x * y) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x ((δ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]) x : T ⊗[S] Ω[S⁄R])
have add : ∀ (x₁ x₂ : MvPolynomial ι S)
  (hx₁ :
    (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (x₁ * y) =
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₁ ((δ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]) x₁ : T ⊗[S] Ω[S⁄R]))
  (hx₂ :
    (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (x₂ * y) =
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) x₂ ((δ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]) x₂ : T ⊗[S] Ω[S⁄R])),
  (δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((x₁ + x₂) * y) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (x₁ + x₂) ((δ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]) (x₁ + x₂) : T ⊗[S] Ω[S⁄R])
Tactic: induction x using MvPolynomial.induction_on' with
  | monomial n r =>
    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
  | add x₁ x₂ hx₁ hx₂ => simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]; abel
Cleared hypotheses: x
-- 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 ι
r : S
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((C : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
have rw : Eq (α := T ⊗[S] Ω[S⁄R])
  ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((monomial 0 : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
  (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
Tactic: rw [← monomial_zero', δAux_monomial, Finsupp.prod_zero_index]
-- 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 ι
r : S
rw :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((monomial 0 : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((C : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
have rw₁ : Eq (α := T ⊗[S] Ω[S⁄R])
  ((Finsupp.prod 0 fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
  (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
Tactic: rw [← monomial_zero', δAux_monomial, Finsupp.prod_zero_index]
-- 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 ι
r : S
rw :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((monomial 0 : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
rw₁ :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((Finsupp.prod 0 fun (x1 : ι) (x2 : ℕ) ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((C : (a : S) → MvPolynomial ι S) r) : T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
have rw₂ : Eq (α := T ⊗[S] Ω[S⁄R]) (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
  (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) r : T ⊗[S] Ω[S⁄R])
Tactic: rw [← monomial_zero', δAux_monomial, Finsupp.prod_zero_index]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (hypothesis)
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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
x : Q.Ring
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) x) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) x : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) x)) :
        T ⊗[S] Ω[S⁄R])
have this₁ : IsScalarTower Q.Ring Q.Ring T
Tactic: have : IsScalarTower Q.Ring Q.Ring T := IsScalarTower.left _
-- 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₁
ι' : Type w₃
Q : Generators S T ι
Q' : Generators S T ι'
f : Q.Hom Q'
x : Q.Ring
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
⊢ (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) x) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) x : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) x)) :
        T ⊗[S] Ω[S⁄R])
have C : ∀ (s : S),
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R])
      ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) ((C : (a : S) → MvPolynomial ι S) s)) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((C : (a : S) → MvPolynomial ι S) s) : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) ((C : (a : S) → MvPolynomial ι S) s))) :
        T ⊗[S] Ω[S⁄R])
Tactic: induction x using MvPolynomial.induction_on with
  | C s => simp [MvPolynomial.algebraMap_eq, δAux_C]
  | add x₁ x₂ hx₁ hx₂ =>
    simp only [map_add, hx₁, hx₂, tmul_add]
    rw [add_add_add_comm]
  | mul_X p n IH =>
    simp only [map_mul, Hom.toAlgHom_X, δAux_mul, algebraMap_apply, Hom.algebraMap_toAlgHom,
      ← @IsScalarTower.algebraMap_smul Q'.Ring T, algebraMap_self, δAux_X,
      RingHom.id_apply, coe_eval₂Hom, IH, Hom.aeval_val, smul_add, map_aeval, tmul_add, tmul_smul,
      ← @IsScalarTower.algebraMap_smul Q.Ring T, smul_zero, aeval_X, zero_add, Derivation.leibniz,
      Basis.repr_self, map_add, one_smul, map_smul, Finsupp.linearCombination_single,
      RingHomCompTriple.comp_eq, Function.comp_apply, ← cotangentSpaceBasis_apply]
    rw [add_left_comm]
    rfl
Cleared hypotheses: x