case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
⊢ x ∈ M'
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'
⊢ x ∈ M'
obtain ⟨s', hs₁, hs₂⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
H : ∀ (r : { x // x ∈ s' }), ∃ n, ↑r ^ n • x ∈ M'
⊢ x ∈ M'
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
⊢ x ∈ M'
replace H : ∀ r : s', ∃ n : ℕ, ((r : R) ^ n  : R) • x ∈ M' := fun r => H ⟨_, hs₁ r.2⟩
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
⊢ x ∈ M'
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
H : ∀ (r : { x // x ∈ s' }), ∃ n, ↑r ^ n • x ∈ M'
⊢ x ∈ M'
choose n₁ n₂ using H
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
⊢ x ∈ M'
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
⊢ x ∈ M'
let N := s'.attach.sup n₁
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
⊢ x ∈ M'
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
⊢ x ∈ M'
have hs' := Ideal.span_pow_eq_top (s' : Set R) hs₂ N
case intro.intro.H
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
⊢ ∀ (r : ↑((fun x => x ^ N) '' ↑s')), ↑r • x ∈ M'
case intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
⊢ x ∈ M'
apply M'.mem_of_span_top_of_smul_mem _ hs'
case intro.intro.H.mk.intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
r : R
hr : r ∈ ↑s'
⊢ ↑{ val := (fun x => x ^ N) r, property := (_ : ∃ a, a ∈ ↑s' ∧ (fun x => x ^ N) a = (fun x => x ^ N) r) } • x ∈ M'
case intro.intro.H
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
⊢ ∀ (r : ↑((fun x => x ^ N) '' ↑s')), ↑r • x ∈ M'
rintro ⟨_, r, hr, rfl⟩
case h.e'_4
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
r : R
hr : r ∈ ↑s'
⊢ ↑{ val := (fun x => x ^ N) r, property := (_ : ∃ a, a ∈ ↑s' ∧ (fun x => x ^ N) a = (fun x => x ^ N) r) } • x =
    r ^ (N - n₁ { val := r, property := hr }) • ↑{ val := r, property := hr } ^ n₁ { val := r, property := hr } • x
case intro.intro.H.mk.intro.intro
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
r : R
hr : r ∈ ↑s'
⊢ ↑{ val := (fun x => x ^ N) r, property := (_ : ∃ a, a ∈ ↑s' ∧ (fun x => x ^ N) a = (fun x => x ^ N) r) } • x ∈ M'
convert M'.smul_mem (r ^ (N - n₁ ⟨r, hr⟩)) (n₂ ⟨r, hr⟩) using 1
case h.e'_4
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
r : R
hr : r ∈ ↑s'
⊢ r ^ Finset.sup (Finset.attach s') n₁ • x =
    r ^ (Finset.sup (Finset.attach s') n₁ - n₁ { val := r, property := hr } + n₁ { val := r, property := hr }) • x
case h.e'_4
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
r : R
hr : r ∈ ↑s'
⊢ ↑{ val := (fun x => x ^ N) r, property := (_ : ∃ a, a ∈ ↑s' ∧ (fun x => x ^ N) a = (fun x => x ^ N) r) } • x =
    r ^ (N - n₁ { val := r, property := hr }) • ↑{ val := r, property := hr } ^ n₁ { val := r, property := hr } • x
simp only [Subtype.coe_mk, smul_smul, ← pow_add]
no goals
case h.e'_4
R : Type u
M : Type v
F : Type ?u.123597
G : Type ?u.123600
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
s' : Finset R
hs₁ : ↑s' ⊆ s
hs₂ : Ideal.span ↑s' = ⊤
n₁ : { x // x ∈ s' } → ℕ
n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'
N : ℕ := Finset.sup (Finset.attach s') n₁
hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤
r : R
hr : r ∈ ↑s'
⊢ r ^ Finset.sup (Finset.attach s') n₁ • x =
    r ^ (Finset.sup (Finset.attach s') n₁ - n₁ { val := r, property := hr } + n₁ { val := r, property := hr }) • x
rw [tsub_add_cancel_of_le (Finset.le_sup (s'.mem_attach _) : n₁ ⟨r, hr⟩ ≤ N)]