-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[S] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((↑S :
            {S_1 M : Type u_4} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring S] →
                  [inst_12 : Semiring S_1] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] →
                            [inst_17 : Module S_1 M] →
                              [inst_18 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
            (derivationTensorProduct R S A B)) ∘ₗ
        LinearMap.liftBaseChange S
          ((↑R :
              {S M : Type u_3} →
                {M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_12 : Semiring S] →
                      [inst_13 : AddCommMonoid M] →
                        [inst_14 : AddCommMonoid M₂] →
                          [inst_15 : Module R M] →
                            [inst_16 : Module R M₂] →
                              [inst_17 : Module S M] →
                                [inst_18 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map R S A B)) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[S] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (LinearMap.id : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[S] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have refine : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
  ((↑R :
        {S : Type u_2} →
          {M M₂ : Type (max u_2 u_3)} →
            [inst : Semiring R] →
              [inst_12 : Semiring S] →
                [inst_13 : AddCommMonoid M] →
                  [inst_14 : AddCommMonoid M₂] →
                    [inst_15 : Module R M] →
                      [inst_16 : Module R M₂] →
                        [inst_17 : Module S M] →
                          [inst_18 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      ((↑S :
            {S_1 M : Type u_4} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring S] →
                  [inst_12 : Semiring S_1] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] →
                            [inst_17 : Module S_1 M] →
                              [inst_18 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
            (derivationTensorProduct R S A B)) ∘ₗ
        LinearMap.liftBaseChange S
          ((↑R :
              {S M : Type u_3} →
                {M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_12 : Semiring S] →
                      [inst_13 : AddCommMonoid M] →
                        [inst_14 : AddCommMonoid M₂] →
                          [inst_15 : Module R M] →
                            [inst_16 : Module R M₂] →
                              [inst_17 : Module S M] →
                                [inst_18 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map R S A B))) :
    TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
  ((↑R :
        {S : Type u_2} →
          {M M₂ : Type (max u_2 u_3)} →
            [inst : Semiring R] →
              [inst_12 : Semiring S] →
                [inst_13 : AddCommMonoid M] →
                  [inst_14 : AddCommMonoid M₂] →
                    [inst_15 : Module R M] →
                      [inst_16 : Module R M₂] →
                        [inst_17 : Module S M] →
                          [inst_18 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) LinearMap.id :
    TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
Tactic: refine LinearMap.restrictScalars_injective R ?_