-- 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,
        ((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
⊢ 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 (α := 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).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)).2
Tactic: ext