R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
t : ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥

case t
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥
case t.intro
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups f) n = ↑(partialSups f) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
case t
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr I (partialSups f)
no goals
case t.intro
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups f) n = ↑(partialSups f) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
exact
  ⟨n, fun m p =>
    (h m).eq_bot_of_ge <| sup_eq_left.1 <| (w (m + 1) <| le_add_right p).symm.trans <| w m p⟩
case intro
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
t : ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
obtain ⟨n, w⟩ := t
case intro
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∀ (m : ℕ), n + 1 ≤ m → f m = ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
use n + 1
case intro.zero
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ Nat.zero
⊢ f Nat.zero = ⊥

case intro.succ
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ f (Nat.succ m) = ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∀ (m : ℕ), n + 1 ≤ m → f m = ⊥
rintro (_ | m) p
no goals
case intro.zero
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ Nat.zero
⊢ f Nat.zero = ⊥
cases p
case intro.succ.a
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ n ≤ m
case intro.succ
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ f (Nat.succ m) = ⊥
apply w
no goals
case intro.succ.a
R : Type u_1
M : Type u_2
P : Type ?u.278074
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ n ≤ m
exact Nat.succ_le_succ_iff.mp p