-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst : Algebra P.Ring (Generators.Ring (comp (localizationAway T g) P)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Hom.toAlgHom (toComp (localizationAway T g) P)))
f : P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2 :=
  (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)
π : Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
  Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) :=
  compLocalizationAwayAlgHom T g P
x : P.toExtension.Cotangent
hx :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((lift
            ((↑S :
                {S_1 M : Type u_3} →
                  {M₂ : Type (max u_1 u_4)} →
                    [inst : Semiring S] →
                      [inst_8 : Semiring S_1] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [inst_13 : Module S_1 M] →
                                  [inst_14 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (S := T)
              (((↑(LinearEquiv.symm
                        (LinearMap.ringLmapEquivSelf T T
                          (P.toExtension.Cotangent →ₗ[S] Extension.Cotangent (toExtension (Q.comp P))))) :
                    (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →ₗ[T]
                      T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) :
                  (a : P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →
                    T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)
                (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))) :
          (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
        (((TensorProduct.mk S T P.toExtension.Cotangent :
                (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
              1 :
            (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
          x) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (0 : Extension.Cotangent (toExtension (Q.comp P)))
⊢ Eq (α := T ⊗[S] P.toExtension.Cotangent)
    (((TensorProduct.mk S T P.toExtension.Cotangent :
              (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
            1 :
          (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
        x :
      T ⊗[S] P.toExtension.Cotangent)
    (0 : T ⊗[S] P.toExtension.Cotangent)
have obtain : ∀ (x : ↥P.toExtension.ker)
  (hx :
    Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
      ((lift
              ((↑S :
                  {S_1 M : Type u_3} →
                    {M₂ : Type (max u_1 u_4)} →
                      [inst : Semiring S] →
                        [inst_8 : Semiring S_1] →
                          [inst_9 : AddCommMonoid M] →
                            [inst_10 : AddCommMonoid M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [inst_13 : Module S_1 M] →
                                    [inst_14 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (S := T)
                (((↑(LinearEquiv.symm
                          (LinearMap.ringLmapEquivSelf T T
                            (P.toExtension.Cotangent →ₗ[S] Extension.Cotangent (toExtension (Q.comp P))))) :
                      (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →ₗ[T]
                        T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) :
                    (a : P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →
                      T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)
                  (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))) :
            (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
          (((TensorProduct.mk S T P.toExtension.Cotangent :
                  (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
                1 :
              (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
            ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x)) :
        Extension.Cotangent (toExtension (Q.comp P)))
      (0 : Extension.Cotangent (toExtension (Q.comp P)))),
  Eq (α := T ⊗[S] P.toExtension.Cotangent)
    (((TensorProduct.mk S T P.toExtension.Cotangent :
              (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
            1 :
          (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x) :
      T ⊗[S] P.toExtension.Cotangent)
    (0 : T ⊗[S] P.toExtension.Cotangent)
Tactic: obtain ⟨x, rfl⟩ := Algebra.Extension.Cotangent.mk_surjective x
Cleared hypotheses: x, hx