awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ 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])
have this₁ : 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 _
-- 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 (α := 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))))
have 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)))
Tactic: ext 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₁
ι' : 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 τ
⊢ 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)))
have 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)
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 σ
⊢ Eq (α := T ⊗[S] P.toExtension.CotangentSpace →ₗ[T] Ω[T⁄R])
    (mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler)
    (Extension.toKaehler (toExtension (Q.comp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))))
have hF : ∀ (i : σ),
  Eq.{u₃ + 1} (α := Ω[T⁄R])
    ((mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) ∘ₗ
            LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Ω[T⁄R])
Tactic: apply (P.cotangentSpaceBasis.baseChange T).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 σ
i : σ
⊢ Eq.{u₃ + 1} (α := Ω[T⁄R])
    ((mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) ∘ₗ
            LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Ω[T⁄R])
have hF : Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
  ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        ((P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i)) :
    Ω[T⁄R])
Tactic: simp only [Basis.baseChange_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.baseChange_tmul, toKaehler_cotangentSpaceBasis, mapBaseChange_tmul, map_D,
      one_smul, LinearMap.liftBaseChange_tmul]
-- 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 σ
i : σ
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i)) :
      Ω[T⁄R])
have hF : Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
  ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
    Ω[T⁄R])
Tactic: rw [cotangentSpaceBasis_apply]
-- 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 σ
i : σ
| ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
    Ω[T⁄R])
have enter : ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
      (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
    (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
  Extension.CotangentSpace (toExtension (Q.comp P)))
Tactic: enter [2]
-- 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 σ
i : σ
| ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
    Ω[T⁄R])
have enter : ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
      (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
    (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
  Extension.CotangentSpace (toExtension (Q.comp P)))
Tactic: enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..
-- 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 σ
i : σ
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
      Ω[T⁄R])
have hF : Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
  ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((algebraMap S T : (a : S) → T) 1 ⊗ₜ[Extension.Ring (toExtension (Q.comp P))]
        (D R (Extension.Ring (toExtension (Q.comp P))) :
            (a : (Q.comp P).toExtension.Ring) → Ω[(Q.comp P).toExtension.Ring⁄R])
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
              (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
            (X i))) :
    Ω[T⁄R])
Tactic: conv_rhs => enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..
-- 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 σ
i : σ
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((algebraMap S T : (a : S) → T) 1 ⊗ₜ[Extension.Ring (toExtension (Q.comp P))]
          (D R (Extension.Ring (toExtension (Q.comp P))) :
              (a : (Q.comp P).toExtension.Ring) → Ω[(Q.comp P).toExtension.Ring⁄R])
            ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
                (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
              (X i))) :
      Ω[T⁄R])
have hF : Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
  ((D R T : (a : T) → Ω[T⁄R])
      ((algebraMap (Extension.Ring (toExtension (Q.comp P))) T : (a : (Q.comp P).toExtension.Ring) → T)
        ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
              (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
            (X i) :
          Extension.Ring (toExtension (Q.comp P)))) :
    Ω[T⁄R])
Tactic: simp only [map_one, mapBaseChange_tmul, map_D, one_smul]
-- 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)
⊢ 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)
have simp : Eq (α := Q.toExtension.Cotangent)
  ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
      (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
        ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Ring) → Q.toExtension.Ring)
          (↑(Q.kerCompPreimage P x) : (Q.comp P).toExtension.Ring))
        sorry) :
    Q.toExtension.Cotangent)
  ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
Tactic: simp only [y, Extension.Cotangent.map_mk]
-- 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)
⊢ Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Ring) → Q.toExtension.Ring)
            (↑(Q.kerCompPreimage P x) : (Q.comp P).toExtension.Ring))
          ⋯) :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
have h : (Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.ofComp P)) : (a : (Q.comp P).toExtension.Ring) → Q.toExtension.Ring)
    (↑(Q.kerCompPreimage P x) : (Q.comp P).toExtension.Ring) =
  (↑x : Q.toExtension.Ring)
Tactic: congr
-- 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 ι
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)
⊢ 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 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)
Tactic: have hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x := by
    simp only [y, Extension.Cotangent.map_mk]
    congr
    exact ofComp_kerCompPreimage Q P 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₁
σ : 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])
    ((δ 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 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])
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
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])
⊢ 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 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)
Tactic: rw [H1Cotangent.δ_eq (y := y) (z := z)]