-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module R Q
inst_22 : Module T Q
inst_23 : IsScalarTower R T Q
i : M →ₗ[R] Q
this_1 : Module S Q := Module.compHom Q (algebraMap S T)
this_2 : IsScalarTower S T Q
this : IsScalarTower R S Q
⊢ ∃! g' : O →ₗ[T] Q,
    (↑R :
            {S : Type u_4} →
              {M : Type u_5} →
                {M₂ : Type (max (max v₁ u_5) u_4)} →
                  [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₂)
          g' ∘ₗ
        (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type u_5} →
                    [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₂)
            g ∘ₗ
          f =
      i
have h : ∀ (y : O →ₗ[T] Q),
  (fun (g' : O →ₗ[T] Q) ↦
        (↑R :
                {S : Type u_4} →
                  {M : Type u_5} →
                    {M₂ : Type (max (max v₁ u_5) u_4)} →
                      [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₂)
              g' ∘ₗ
            (↑R :
                  {S : Type v₃} →
                    {M : Type v₂} →
                      {M₂ : Type u_5} →
                        [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₂)
                g ∘ₗ
              f =
          i)
      y →
    y = hg.lift (hf.lift i)
Tactic: refine
    ⟨hg.lift (hf.lift i), by
      ext
      simp [IsBaseChange.lift_eq], ?_⟩