-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.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'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
refine_1 :
  Eq.{w' + 1} (α := P'.Cotangent)
    ((((↑R :
                {S M M₂ : Type w'} →
                  [inst : Semiring R] →
                    [inst_24 : Semiring S] →
                      [inst_25 : AddCommMonoid M] →
                        [inst_26 : AddCommMonoid M₂] →
                          [inst_27 : Module R M] →
                            [inst_28 : Module R M₂] →
                              [inst_29 : Module S M] →
                                [inst_30 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              Cotangent.mk ∘ₗ
            f.subToKer g :
          LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
        (a : P.Ring) → P'.Cotangent)
      1)
    0
⊢ Derivation.{u, w, w'} R P.Ring P'.Cotangent
have refine_2 : ∀ (a b : P.Ring),
  (((↑R :
                {S M M₂ : Type w'} →
                  [inst : Semiring R] →
                    [inst_24 : Semiring S] →
                      [inst_25 : AddCommMonoid M] →
                        [inst_26 : AddCommMonoid M₂] →
                          [inst_27 : Module R M] →
                            [inst_28 : Module R M₂] →
                              [inst_29 : Module S M] →
                                [inst_30 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              Cotangent.mk ∘ₗ
            f.subToKer g :
          LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
        (a : P.Ring) → P'.Cotangent)
      (a * b) =
    HSMul.hSMul (β := P'.Cotangent) a
        ((((↑R :
                      {S M M₂ : Type w'} →
                        [inst : Semiring R] →
                          [inst_24 : Semiring S] →
                            [inst_25 : AddCommMonoid M] →
                              [inst_26 : AddCommMonoid M₂] →
                                [inst_27 : Module R M] →
                                  [inst_28 : Module R M₂] →
                                    [inst_29 : Module S M] →
                                      [inst_30 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    Cotangent.mk ∘ₗ
                  f.subToKer g :
                LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
              (a : P.Ring) → P'.Cotangent)
            b :
          P'.Cotangent) +
      HSMul.hSMul (β := P'.Cotangent) b
        ((((↑R :
                      {S M M₂ : Type w'} →
                        [inst : Semiring R] →
                          [inst_24 : Semiring S] →
                            [inst_25 : AddCommMonoid M] →
                              [inst_26 : AddCommMonoid M₂] →
                                [inst_27 : Module R M] →
                                  [inst_28 : Module R M₂] →
                                    [inst_29 : Module S M] →
                                      [inst_30 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    Cotangent.mk ∘ₗ
                  f.subToKer g :
                LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
              (a : P.Ring) → P'.Cotangent)
            a :
          P'.Cotangent)
Tactic: refine
  { __ := Cotangent.mk.restrictScalars R ∘ₗ f.subToKer g
    map_one_eq_zero' := ?_
    leibniz' := ?_ }