-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem of_restrictScalars_finite (R A M : Type*) [CommSemiring R] [Semiring A] [AddCommMonoid M]
    [Module R M] [Module A M] [Algebra R A] [IsScalarTower R A M] [hM : Module.Finite R M] :
    Module.Finite A M

Proof state:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ⊤ ≤ span A S

Tactic:
have := Submodule.span_le_restrictScalars R A S

Result:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
this : span R S ≤ restrictScalars R (span A S)
⊢ ⊤ ≤ span A S

Proof state:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
hM : ∃ S, S.Finite ∧ span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤

Tactic:
obtain ⟨S, hSfin, hSgen⟩ := hM

Result:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤

Proof state:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
this : ⊤ ≤ restrictScalars R (span A S)
⊢ ⊤ ≤ span A S

Tactic:
exact this

Result:
no goals

Proof state:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
this : span R S ≤ restrictScalars R (span A S)
⊢ ⊤ ≤ span A S

Tactic:
rw [hSgen] at this

Result:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
this : ⊤ ≤ restrictScalars R (span A S)
⊢ ⊤ ≤ span A S

Proof state:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤

Tactic:
refine ⟨S, hSfin, eq_top_iff.2 ?_⟩

Result:
case intro.intro
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ⊤ ≤ span A S

Proof state:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
hM : Module.Finite R M
⊢ Module.Finite A M

Tactic:
rw [finite_def, Submodule.fg_def] at hM ⊢

Result:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
hM : ∃ S, S.Finite ∧ span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤