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₁
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])
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]))
⊢ (δ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:
simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]

Premises used: add_mul, map_add, add_smul, smul_add
-- 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
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])
⊢ 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:
abel
-- 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 ι
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])
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])
⊢ (δ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])

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

Premises used: add_mul, 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
-- 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 ι
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])
rw₂ 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])
⊢ 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])

Tactic:
rw [← monomial_zero', δAux_monomial, Finsupp.prod_zero_index]

Premises used: Algebra.Generators.H1Cotangent.δAux_monomial, MvPolynomial.monomial_zero', Finsupp.prod_zero_index
-- 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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
x : Q.Ring
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ IsScalarTower Q.Ring Q.Ring T

Tactic:
have : IsScalarTower Q.Ring Q.Ring T := IsScalarTower.left _
-- 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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
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:
simp [MvPolynomial.algebraMap_eq, δAux_C]

Premises used: Algebra.Generators.H1Cotangent.δAux_C, MvPolynomial.algebraMap_eq
-- 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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
p : MvPolynomial ι S
n : ι
IH :
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) p) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : 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]) p)) :
        T ⊗[S] Ω[S⁄R])
⊢ HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R]) +
      (HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (eval₂ (algebraMap S T) (fun (i : ι) ↦ Q.val i) p)
          ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) (f.val n) : T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n)
          ((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]) p)) :
            T ⊗[S] Ω[S⁄R])) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R]) +
      (HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R]) ((aeval Q.val : (a : MvPolynomial ι S) → T) p : T)
          ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) (f.val n) : T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n)
          ((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]) p)) :
            T ⊗[S] Ω[S⁄R]))

Tactic:
rfl
-- 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 σ
x : Generators.Ring (Q.comp P)
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ IsScalarTower (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)) T

Tactic:
have : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T := IsScalarTower.left _
-- 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 σ
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)) T
s : R
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) ((C : (a : R) → MvPolynomial (ι ⊕ σ) R) s)) :
      T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
        ((CotangentSpace.compEquiv Q P :
              (a : (Q.comp P).toExtension.CotangentSpace) →
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
            (1 ⊗ₜ[Generators.Ring (Q.comp P)]
              (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R])
                ((C : (a : R) → MvPolynomial (ι ⊕ σ) R) s))).2 :
      T ⊗[S] Ω[S⁄R])

Tactic:
simp only [algHom_C, δAux_C, derivation_C, Derivation.map_algebraMap,
      tmul_zero, map_zero, MvPolynomial.algebraMap_apply, Prod.snd_zero]

Premises used: Algebra.Generators.H1Cotangent.δAux_C, TensorProduct.tmul_zero, map_zero, MvPolynomial.algebraMap_apply, MvPolynomial.algHom_C, MvPolynomial.derivation_C, Derivation.map_algebraMap, Prod.snd_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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)) T
x₁ x₂ : MvPolynomial (ι ⊕ σ) R
hx₁ :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x₁) :
      T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
        ((CotangentSpace.compEquiv Q P :
              (a : (Q.comp P).toExtension.CotangentSpace) →
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
            (1 ⊗ₜ[Generators.Ring (Q.comp P)]
              (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) x₁)).2 :
      T ⊗[S] Ω[S⁄R])
hx₂ :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x₂) :
      T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
        ((CotangentSpace.compEquiv Q P :
              (a : (Q.comp P).toExtension.CotangentSpace) →
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
            (1 ⊗ₜ[Generators.Ring (Q.comp P)]
              (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) x₂)).2 :
      T ⊗[S] Ω[S⁄R])
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (x₁ + x₂)) :
      T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
        ((CotangentSpace.compEquiv Q P :
              (a : (Q.comp P).toExtension.CotangentSpace) →
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
            (1 ⊗ₜ[Generators.Ring (Q.comp P)]
              (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) (x₁ + x₂))).2 :
      T ⊗[S] Ω[S⁄R])

Tactic:
simp only [map_add, hx₁, hx₂, tmul_add, Prod.snd_add]

Premises used: map_add, TensorProduct.tmul_add, Prod.snd_add
-- 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 σ
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)) T
p : MvPolynomial (ι ⊕ σ) R
IH :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p) :
      T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
        ((CotangentSpace.compEquiv Q P :
              (a : (Q.comp P).toExtension.CotangentSpace) →
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
            (1 ⊗ₜ[Generators.Ring (Q.comp P)]
              (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) p)).2 :
      T ⊗[S] Ω[S⁄R])
n : σ
⊢ HSMul.hSMul (β := T ⊗[S] Ω[S⁄R])
      (eval₂ (algebraMap R T) (fun (i : ι ⊕ σ) ↦ Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) i) p)
      (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) (P.val n) : T ⊗[S] Ω[S⁄R]) =
    HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R]) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T) p : T)
      (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) (P.val n) : T ⊗[S] Ω[S⁄R])

Tactic:
rfl
-- 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 σ
a :
  ∀ (x : P.toExtension.Cotangent),
    Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
      ((((AlgebraTensorModule.curry
                    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) ∘ₗ
                      LinearMap.baseChange T P.toExtension.cotangentComplex) :
                  T →ₗ[T] P.toExtension.Cotangent →ₗ[S] Extension.CotangentSpace (toExtension (Q.comp P))) :
                (a : T) → P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.CotangentSpace)
              1 :
            (a : P.toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
          x :
        Extension.CotangentSpace (toExtension (Q.comp P)))
      ((((AlgebraTensorModule.curry
                    (Extension.cotangentComplex (toExtension (Q.comp P)) ∘ₗ
                      LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
                  T →ₗ[T] P.toExtension.Cotangent →ₗ[S] Extension.CotangentSpace (toExtension (Q.comp P))) :
                (a : T) → P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.CotangentSpace)
              1 :
            (a : P.toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
          x :
        Extension.CotangentSpace (toExtension (Q.comp P)))
⊢ Eq (α := T ⊗[S] P.toExtension.Cotangent →ₗ[T] Extension.CotangentSpace (toExtension (Q.comp P)))
    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) ∘ₗ
      LinearMap.baseChange T P.toExtension.cotangentComplex)
    (Extension.cotangentComplex (toExtension (Q.comp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))

Tactic:
ext x
-- 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 σ
x : P.toExtension.Cotangent
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((((AlgebraTensorModule.curry
                  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) ∘ₗ
                    LinearMap.baseChange T P.toExtension.cotangentComplex) :
                T →ₗ[T] P.toExtension.Cotangent →ₗ[S] Extension.CotangentSpace (toExtension (Q.comp P))) :
              (a : T) → P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.CotangentSpace)
            1 :
          (a : P.toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        x :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((((AlgebraTensorModule.curry
                  (Extension.cotangentComplex (toExtension (Q.comp P)) ∘ₗ
                    LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
                T →ₗ[T] P.toExtension.Cotangent →ₗ[S] Extension.CotangentSpace (toExtension (Q.comp P))) :
              (a : T) → P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.CotangentSpace)
            1 :
          (a : P.toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        x :
      Extension.CotangentSpace (toExtension (Q.comp P)))

Tactic:
simp [Extension.CotangentSpace.map_cotangentComplex]

Premises used: Algebra.Extension.CotangentSpace.map_cotangentComplex
-- 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₃
σ : Type w₂
σ' : Type w₄
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
W : Generators R T τ
h :
  ∀ (x : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.CotangentSpace)
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
              Extension.cotangentComplex (toExtension (Q.comp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.CotangentSpace)
          x :
        Q.toExtension.CotangentSpace)
      ((Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.CotangentSpace)
          x :
        Q.toExtension.CotangentSpace)
⊢ Eq (α := Extension.Cotangent (toExtension (Q.comp P)) →ₗ[T] Q.toExtension.CotangentSpace)
    (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
      Extension.cotangentComplex (toExtension (Q.comp P)))
    (Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)))

Tactic:
ext