case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤

R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups (↑OrderDual.toDual ∘ f)) n = ↑(partialSups (↑OrderDual.toDual ∘ f)) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
obtain ⟨n, w⟩ := monotone_stabilizes (partialSups (OrderDual.toDual ∘ f))
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups (↑OrderDual.toDual ∘ f)) n = ↑(partialSups (↑OrderDual.toDual ∘ f)) m
m : ℕ
p : n ≤ m
⊢ ↑OrderDual.toDual f (m + 1) = ⊤
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups (↑OrderDual.toDual ∘ f)) n = ↑(partialSups (↑OrderDual.toDual ∘ f)) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
refine' ⟨n, fun m p => _⟩
no goals
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups (↑OrderDual.toDual ∘ f)) n = ↑(partialSups (↑OrderDual.toDual ∘ f)) m
m : ℕ
p : n ≤ m
⊢ ↑OrderDual.toDual f (m + 1) = ⊤
exact (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
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
⊢ ∀ (m : ℕ), n + 1 ≤ m → f m = ⊤
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
use n + 1
case intro.zero
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
p : n + 1 ≤ Nat.zero
⊢ f Nat.zero = ⊤

case intro.succ
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ f (Nat.succ m) = ⊤
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual 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
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual 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
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ n ≤ m
case intro.succ
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual 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
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ n ≤ m
exact Nat.succ_le_succ_iff.mp p