-- 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 : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P))) x
y : Generators.Ring (Q.comp P)
hy : y ∈ HMul.hMul (α := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) (ker (Q.comp P))
e :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) (x - y)
z : ↥(ker (Q.comp P)) :=
  Subtype.mk (p := fun (x : Generators.Ring (Q.comp P)) ↦
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x) (x - y) ⋯
hz :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (↑z : (Q.comp P).Ring)
this :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
            x)
          x hx') :
      Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent) z :
      Extension.Cotangent (toExtension (Q.comp P)))
w : P.Ring
hw : w ∈ P.ker
⊢ Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) w hw)) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (((Extension.Cotangent.mk :
            LinearMap (R := Extension.Ring (toExtension (Q.comp P)))
              (RingHom.id (Extension.Ring (toExtension (Q.comp P)))) (↥(Extension.ker (toExtension (Q.comp P))))
              (Extension.Cotangent (toExtension (Q.comp P)))) :
          (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
        (Subtype.mk (p := fun (a : Generators.Ring (Q.comp P)) ↦
          Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
            (Extension.ker (toExtension (Q.comp P))) a)
          ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) w) ⋯) :
      Extension.Cotangent (toExtension (Q.comp P)))
have h2 : Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
  ((Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
      (Subtype.mk (p := fun (x : Extension.Ring (toExtension (Q.comp P))) ↦
        Membership.mem (γ := Ideal (Extension.Ring (toExtension (Q.comp P)))) (Extension.ker (toExtension (Q.comp P)))
          x)
        ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
          (↑(Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) w hw) : P.toExtension.Ring))
        sorry) :
    Extension.Cotangent (toExtension (Q.comp P)))
  (((Extension.Cotangent.mk :
          LinearMap (R := Extension.Ring (toExtension (Q.comp P)))
            (RingHom.id (Extension.Ring (toExtension (Q.comp P)))) (↥(Extension.ker (toExtension (Q.comp P))))
            (Extension.Cotangent (toExtension (Q.comp P)))) :
        (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
      (Subtype.mk (p := fun (a : Generators.Ring (Q.comp P)) ↦
        Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
          (Extension.ker (toExtension (Q.comp P))) a)
        ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) w) sorry) :
    Extension.Cotangent (toExtension (Q.comp P)))
Tactic: rw [map_mk]