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 σ
x : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
hy :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).2
rw :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R]) z :
      T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
hy₁ :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((↑(Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
            ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
        Q.toExtension.Cotangent) :
      Q.toExtension.Cotangent)
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
have hz : Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
  ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
        (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
      z :
    Extension.CotangentSpace (toExtension (Q.comp P)))
  ((Extension.cotangentComplex (toExtension (Q.comp P)) :
        (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
      y :
    Extension.CotangentSpace (toExtension (Q.comp P)))
Tactic: rw [H1Cotangent.δ_eq (y := y) (z := z)]
-- 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 σ
x : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
hy :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).2
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R]) z :
      T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
have rw : Eq (α := T ⊗[S] Ω[S⁄R])
  ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R]) z :
    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])
              (↑(Q.kerCompPreimage P x) : (Q.comp P).Ring))).2 :
    T ⊗[S] Ω[S⁄R])
Tactic: rw [← ofComp_kerCompPreimage Q P x, δAux_ofComp]
-- 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 σ
x : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
hy :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).2
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        z :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y :
      Extension.CotangentSpace (toExtension (Q.comp P)))
have hz : Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
  (((↑(LinearEquiv.symm (CotangentSpace.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)
      z :
    Extension.CotangentSpace (toExtension (Q.comp P)))
  ((Extension.cotangentComplex (toExtension (Q.comp P)) :
        (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
      y :
    Extension.CotangentSpace (toExtension (Q.comp P)))
Tactic: rw [← CotangentSpace.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 σ
x : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
hy :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).2
⊢ Eq (α := Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
    (0,
      ((CotangentSpace.compEquiv Q P :
            (a : (Q.comp P).toExtension.CotangentSpace) →
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
          ((Extension.cotangentComplex (toExtension (Q.comp P)) :
              (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
            y)).2)
    ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y))
have hz : Eq (α := Q.toExtension.CotangentSpace)
  (0,
      ((CotangentSpace.compEquiv Q P :
            (a : (Q.comp P).toExtension.CotangentSpace) →
              Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
          ((Extension.cotangentComplex (toExtension (Q.comp P)) :
              (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
            y)).2).1
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).1
Tactic: ext
-- 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 σ
x : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
hy :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).2
⊢ Eq (α := Q.toExtension.CotangentSpace) (0 : Q.toExtension.CotangentSpace)
    ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
            (↑(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)
        ((Extension.cotangentComplex (toExtension (Q.comp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
          y) :
      Q.toExtension.CotangentSpace)
have hz : Eq (α := Q.toExtension.CotangentSpace) (0 : Q.toExtension.CotangentSpace)
  ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
        (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y) :
    Q.toExtension.CotangentSpace)
Tactic: rw [CotangentSpace.fst_compEquiv, Extension.CotangentSpace.map_cotangentComplex, hy, hx]
-- 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 σ
x : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
hy :
  Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P :
        (a : (Q.comp P).toExtension.CotangentSpace) →
          Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
      ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y)).2
hz :
  Eq (α := Q.toExtension.CotangentSpace) (0 : Q.toExtension.CotangentSpace)
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
        ((Extension.cotangentComplex (toExtension (Q.comp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
          y) :
      Q.toExtension.CotangentSpace)
⊢ Eq (α := Q.toExtension.CotangentSpace) (0 : Q.toExtension.CotangentSpace)
    ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
            (↑(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)
        ((Extension.cotangentComplex (toExtension (Q.comp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
          y) :
      Q.toExtension.CotangentSpace)
have hz₁ : Eq (α := Q.toExtension.CotangentSpace) (0 : Q.toExtension.CotangentSpace)
  ((Q.toExtension.cotangentComplex : (a : Q.toExtension.Cotangent) → Q.toExtension.CotangentSpace)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y) :
    Q.toExtension.CotangentSpace)
Tactic: rw [CotangentSpace.fst_compEquiv, Extension.CotangentSpace.map_cotangentComplex, hy, hx]
-- 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₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
⊢ δ Q P = δ Q P'
have h : ∀ (x : Q.toExtension.Cotangent) (hx : x ∈ Q.toExtension.cotangentComplex.ker),
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker) x hx) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker) x hx) :
      T ⊗[S] Ω[S⁄R])
Tactic: ext ⟨x, hx⟩
-- 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₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
x : Q.toExtension.Cotangent
hx : x ∈ Q.toExtension.cotangentComplex.ker
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker) x hx) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker) x hx) :
      T ⊗[S] Ω[S⁄R])
have h : ∀ (x : ↥Q.toExtension.ker)
  (hx :
    Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)),
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
Tactic: obtain ⟨x, rfl⟩ := Extension.Cotangent.mk_surjective x
Cleared hypotheses: x, hx
-- 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₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
x : ↥Q.toExtension.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
have h : Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
  ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
      (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
        ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
    T ⊗[S] Ω[S⁄R])
Tactic: rw [δ_eq_δAux, δ_eq_δAux]
-- 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₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
x : ↥Q.toExtension.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
h :
  Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
    ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((δ Q P : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
    ((δ Q P' : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
        (Subtype.mk (p := fun (x : Q.toExtension.Cotangent) ↦ x ∈ Q.toExtension.cotangentComplex.ker)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x) hx) :
      T ⊗[S] Ω[S⁄R])
have h₁ : Eq (α := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
  ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (↑x : Q.Ring) : T ⊗[S] Ω[S⁄R])
Tactic: rw [δ_eq_δAux, δ_eq_δAux]
-- 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 σ
⊢ Eq (α := Extension.H1Cotangent (toExtension (Q.comp P)) →ₗ[T] Q.toExtension.Cotangent)
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ Extension.h1Cotangentι)
    (Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P)))
have hF : ∀ (x : Extension.H1Cotangent (toExtension (Q.comp P))),
  Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ Extension.h1Cotangentι :
          (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.Cotangent)
        x))
    (Extension.Cotangent.val
      ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.Cotangent)
        x))
Tactic: ext x