R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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, Set.Finite S ∧ Submodule.span R S = ⊤
⊢ ∃ S, Set.Finite S ∧ Submodule.span A S = ⊤
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Finite R M
⊢ Finite A M
rw [finite_def, Submodule.fg_def] at hM⊢
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
⊢ ∃ S, Set.Finite S ∧ Submodule.span A S = ⊤
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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, Set.Finite S ∧ Submodule.span R S = ⊤
⊢ ∃ S, Set.Finite S ∧ Submodule.span A S = ⊤
obtain ⟨S, hSfin, hSgen⟩ := hM
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
⊢ ⊤ ≤ Submodule.span A S
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
⊢ ∃ S, Set.Finite S ∧ Submodule.span A S = ⊤
refine' ⟨S, hSfin, eq_top_iff.2 _⟩
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
this : Submodule.span R S ≤ Submodule.restrictScalars R (Submodule.span A S)
⊢ ⊤ ≤ Submodule.span A S
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
⊢ ⊤ ≤ Submodule.span A S
have := Submodule.span_le_restrictScalars R A S
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
this : ⊤ ≤ Submodule.restrictScalars R (Submodule.span A S)
⊢ ⊤ ≤ Submodule.span A S
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
this : Submodule.span R S ≤ Submodule.restrictScalars R (Submodule.span A S)
⊢ ⊤ ≤ Submodule.span A S
rw [hSgen] at this
no goals
case intro.intro
R✝ : Type ?u.395725
A✝ : Type ?u.395728
B : Type ?u.395731
M✝ : Type ?u.395734
N : Type ?u.395737
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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 : Set.Finite S
hSgen : Submodule.span R S = ⊤
this : ⊤ ≤ Submodule.restrictScalars R (Submodule.span A S)
⊢ ⊤ ≤ Submodule.span A S
exact this