-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
R'' : Type u_4
S'' : Type u_5
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension.{u_6, u_4, u_5} R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Cotangent
⊢ Eq.{u_6 + 1} (α := P''.ker.Cotangent)
    (val
      (((map (g.comp f) : LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) :
          (a : P.Cotangent) → P''.Cotangent)
        x))
    (val
      ((((↑S :
                  {S_1 : Type u_2} →
                    {M : Type u_3} →
                      {M₂ : Type u_6} →
                        [inst : Semiring S] →
                          [inst_23 : Semiring S_1] →
                            [inst_24 : AddCommMonoid M] →
                              [inst_25 : AddCommMonoid M₂] →
                                [inst_26 : Module S M] →
                                  [inst_27 : Module S M₂] →
                                    [inst_28 : Module S_1 M] →
                                      [inst_29 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (map g) ∘ₗ
              map f :
            LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) :
          (a : P.Cotangent) → P''.Cotangent)
        x))
have h : ∀ (x : ↥P.ker),
  Eq.{u_6 + 1} (α := P''.ker.Cotangent)
    (val
      (((map (g.comp f) : LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) :
          (a : P.Cotangent) → P''.Cotangent)
        ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val
      ((((↑S :
                  {S_1 : Type u_2} →
                    {M : Type u_3} →
                      {M₂ : Type u_6} →
                        [inst : Semiring S] →
                          [inst_23 : Semiring S_1] →
                            [inst_24 : AddCommMonoid M] →
                              [inst_25 : AddCommMonoid M₂] →
                                [inst_26 : Module S M] →
                                  [inst_27 : Module S M₂] →
                                    [inst_28 : Module S_1 M] →
                                      [inst_29 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (map g) ∘ₗ
              map f :
            LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) :
          (a : P.Cotangent) → P''.Cotangent)
        ((mk : (a : ↥P.ker) → P.Cotangent) x)))
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x