case intro
R✝ : Type ?u.286765
M✝ : Type ?u.286768
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
P : Type ?u.286804
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R✝ P
f : M✝ →ₗ[R✝] P
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ↑(algebraMap R S)
X : Finset M
⊢ FG (restrictScalars R (span S ↑X))
R✝ : Type ?u.286765
M✝ : Type ?u.286768
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
P : Type ?u.286804
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R✝ P
f : M✝ →ₗ[R✝] P
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
N : Submodule S M
hfin : FG N
h : Surjective ↑(algebraMap R S)
⊢ FG (restrictScalars R N)
obtain ⟨X, rfl⟩ := hfin
case intro
R✝ : Type ?u.286765
M✝ : Type ?u.286768
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
P : Type ?u.286804
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R✝ P
f : M✝ →ₗ[R✝] P
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ↑(algebraMap R S)
X : Finset M
⊢ span R ↑X = restrictScalars R (span S ↑X)
case intro
R✝ : Type ?u.286765
M✝ : Type ?u.286768
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
P : Type ?u.286804
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R✝ P
f : M✝ →ₗ[R✝] P
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ↑(algebraMap R S)
X : Finset M
⊢ FG (restrictScalars R (span S ↑X))
use X
no goals
case intro
R✝ : Type ?u.286765
M✝ : Type ?u.286768
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
P : Type ?u.286804
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R✝ P
f : M✝ →ₗ[R✝] P
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ↑(algebraMap R S)
X : Finset M
⊢ span R ↑X = restrictScalars R (span S ↑X)
exact (Submodule.restrictScalars_span R S h (X : Set M)).symm