awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
h :
  ∀ (y : N →ₗ[R] Q),
    (fun (g' : N →ₗ[R] Q) ↦
          (↑R :
                  {S : Type u_1} →
                    {M : Type v₂} →
                      {M₂ : Type (max (max v₁ v₂) u_1)} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                g' ∘ₗ
              (↑e : M →ₗ[R] N) =
            g)
        y →
      y = g ∘ₗ (↑e.symm : N →ₗ[R] M)
⊢ ∃! g' : N →ₗ[R] Q,
    (↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑e : M →ₗ[R] N) =
      g

Tactic:
refine
    ⟨g.comp e.symm.toLinearMap, by
      ext
      simp, ?_⟩
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
I₄ : IsScalarTower R R Q
y : N →ₗ[R] Q
h :
  ∀ (x : N),
    Eq (α := Q) ((y : (a : N) → Q) x : Q)
      ((((↑R :
                    {S : Type u_1} →
                      {M : Type v₂} →
                        {M₂ : Type (max (max v₁ v₂) u_1)} →
                          [inst : Semiring R] →
                            [inst_5 : Semiring S] →
                              [inst_6 : AddCommMonoid M] →
                                [inst_7 : AddCommMonoid M₂] →
                                  [inst_8 : Module R M] →
                                    [inst_9 : Module R M₂] →
                                      [inst_10 : Module S M] →
                                        [inst_11 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  y ∘ₗ
                (↑e : M →ₗ[R] N)) ∘ₗ
              (↑e.symm : N →ₗ[R] M) :
            (a : N) → Q)
          x :
        Q)
⊢ y =
    ((↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          y ∘ₗ
        (↑e : M →ₗ[R] N)) ∘ₗ
      (↑e.symm : N →ₗ[R] M)

Tactic:
ext
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
I₄ : IsScalarTower R R Q
y : N →ₗ[R] Q
x : N
⊢ Eq (α := Q) ((y : (a : N) → Q) x : Q)
    ((((↑R :
                  {S : Type u_1} →
                    {M : Type v₂} →
                      {M₂ : Type (max (max v₁ v₂) u_1)} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                y ∘ₗ
              (↑e : M →ₗ[R] N)) ∘ₗ
            (↑e.symm : N →ₗ[R] M) :
          (a : N) → Q)
        x :
      Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
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
h :
  ∀ (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] (g_1 : M →ₗ[R] 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 =
        g_1
⊢ IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_20 : Semiring S] →
                    [inst_21 : AddCommMonoid M] →
                      [inst_22 : AddCommMonoid M₂] →
                        [inst_23 : Module R M] →
                          [inst_24 : Module R M₂] →
                            [inst_25 : Module S M] →
                              [inst_26 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g ∘ₗ
      f)

Tactic:
apply IsBaseChange.of_lift_unique

Premises used: IsBaseChange.of_lift_unique
-- Module: Mathlib.RingTheory.IsTensorProduct
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 : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
rw : HSMul.hSMul (α := T) ((algebraMap S T : (a : S) → T) x : T) (y • z) = x • y • z
⊢ (x • y) • z = x • y • z

Tactic:
rw [Algebra.smul_def, mul_smul]

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.IsTensorProduct
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 : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ HSMul.hSMul (α := T) ((algebraMap S T : (a : S) → T) x : T) (y • z) = x • y • z

Tactic:
rfl
-- Module: Mathlib.RingTheory.IsTensorProduct
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 : Module S Q := Module.compHom Q (algebraMap S T)
⊢ IsScalarTower S T Q

Tactic:
haveI : IsScalarTower S T Q :=
    ⟨fun x y z => by
      rw [Algebra.smul_def, mul_smul]
      rfl⟩
-- Module: Mathlib.RingTheory.IsTensorProduct
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 : IsScalarTower S T Q
⊢ IsScalarTower R S Q

Tactic:
have : IsScalarTower R S Q := IsScalarTower.to₁₂₄ _ _ T _
-- Module: Mathlib.RingTheory.IsTensorProduct
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
x : M
⊢ Eq (α := 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₂)
              (hg.lift (hf.lift i)) ∘ₗ
            (↑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 :
          (a : M) → Q)
        x :
      Q)
    ((i : (a : M) → Q) x : Q)

Tactic:
simp [IsBaseChange.lift_eq]

Premises used: IsBaseChange.lift_eq
-- Module: Mathlib.RingTheory.IsTensorProduct
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
e :
  (↑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
⊢ g' = hg.lift (hf.lift i)

Tactic:
hg.algHom_ext' _ _ (hf.algHom_ext' _ _ ?_)

Premises used: IsBaseChange.algHom_ext'
-- Module: Mathlib.RingTheory.IsTensorProduct
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
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_20 : Semiring S] →
                    [inst_21 : AddCommMonoid M] →
                      [inst_22 : AddCommMonoid M₂] →
                        [inst_23 : Module R M] →
                          [inst_24 : Module R M₂] →
                            [inst_25 : Module S M] →
                              [inst_26 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
h₁ :
  ∀ (Q : Type (max v₂ u_5 u_4)) [inst : AddCommMonoid Q] [inst_20 : Module S Q] [inst_21 : Module T Q]
    [inst_22 : IsScalarTower S T Q] (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [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₂)
            g' ∘ₗ
          h =
        g
⊢ IsBaseChange T h

Tactic:
apply IsBaseChange.of_lift_unique

Premises used: IsBaseChange.of_lift_unique
-- Module: Mathlib.RingTheory.IsTensorProduct
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
h : N →ₗ[S] O
hc :
  IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_20 : Semiring S] →
                    [inst_21 : AddCommMonoid M] →
                      [inst_22 : AddCommMonoid M₂] →
                        [inst_23 : Module R M] →
                          [inst_24 : Module R M₂] →
                            [inst_25 : Module S M] →
                              [inst_26 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h ∘ₗ
      f)
Q : Type (max v₂ u_5 u_4)
h₁ :
  ∀ [inst : AddCommMonoid Q] [inst_20 : Module S Q] [inst_21 : Module T Q] [inst_22 : IsScalarTower S T Q]
    (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [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₂)
            g' ∘ₗ
          h =
        g
⊢ ∀ [inst : AddCommMonoid Q] [inst_20 : Module S Q] [inst_21 : Module T Q] [inst_22 : IsScalarTower S T Q]
    (g : N →ₗ[S] Q),
    ∃! g' : O →ₗ[T] Q,
      (↑S :
              {S_1 : Type u_4} →
                {M : Type u_5} →
                  {M₂ : Type (max (max v₂ u_5) u_4)} →
                    [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₂)
            g' ∘ₗ
          h =
        g

Tactic:
_