R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid N
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module S N
inst✝⁸ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type ?u.487928
Q✝ : Type ?u.487931
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
inst✝⁵ : AddCommMonoid Q✝
inst✝⁴ : Module S Q✝
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
⊢ ∃! g', LinearMap.comp (↑R g') f = g
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type ?u.487928
Q : Type ?u.487931
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
h : IsBaseChange S f
⊢ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', LinearMap.comp (↑R g') f = g
intros Q _ _ _ _ g
no goals
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid N
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module S N
inst✝⁸ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type ?u.487928
Q✝ : Type ?u.487931
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
inst✝⁵ : AddCommMonoid Q✝
inst✝⁴ : Module S Q✝
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
⊢ ∃! g', LinearMap.comp (↑R g') f = g
exact ⟨h.lift g, h.lift_comp g, fun g' e => h.alg_hom_ext' _ _ (e.trans (h.lift_comp g).symm)⟩