-- Mathlib/RingTheory/Finiteness/Basic.lean
lemma FG.of_restrictScalars (R) {A M} [CommSemiring R] [Semiring A] [AddCommMonoid M]
    [Algebra R A] [Module R M] [Module A M] [IsScalarTower R A M] (S : Submodule A M)
    (hS : (S.restrictScalars R).FG) : S.FG

Proof state:
case intro.refine_2
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)

Tactic:
rw [← e]

Result:
case intro.refine_2
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ span R ↑s ≤ restrictScalars R (span A ↑s)

Proof state:
case intro
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ S.FG

Tactic:
refine ⟨s, Submodule.restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩

Result:
case intro.refine_1
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R (span A ↑s) ≤ restrictScalars R S

case intro.refine_2
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)

Proof state:
case intro.refine_1
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
this : ↑s ⊆ ↑(restrictScalars R S)
⊢ span A ↑s ≤ S

Tactic:
rwa [Submodule.span_le]

Result:
no goals

Proof state:
case intro.refine_1
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R (span A ↑s) ≤ restrictScalars R S

Tactic:
show Submodule.span A s ≤ S

Result:
case intro.refine_1
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ span A ↑s ≤ S

Proof state:
case intro.refine_1
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ span A ↑s ≤ S

Tactic:
have := Submodule.span_le.mp e.le

Result:
case intro.refine_1
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
this : ↑s ⊆ ↑(restrictScalars R S)
⊢ span A ↑s ≤ S

Proof state:
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
hS : (restrictScalars R S).FG
⊢ S.FG

Tactic:
obtain ⟨s, e⟩ := hS

Result:
case intro
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ S.FG

Proof state:
case intro.refine_2
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ span R ↑s ≤ restrictScalars R (span A ↑s)

Tactic:
exact Submodule.span_le_restrictScalars _ _ _

Result:
no goals