ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
choose u hu hu' using h
case refine_1
ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ (u^[n + 1]) 0 < (u^[n + 1 + 1]) 0

case refine_2
ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ P ((fun n => (u^[n + 1]) 0) n)
ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
refine ⟨fun n => (u^[n + 1]) 0, strictMono_nat_of_lt_succ fun n => ?_, fun n => ?_⟩
no goals
case refine_1
ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ (u^[n + 1]) 0 < (u^[n + 1 + 1]) 0
exact Trans.trans (hu _) (Function.iterate_succ_apply' _ _ _).symm
no goals
case refine_2
ι : Type ?u.57426
ι' : Type ?u.57429
α : Type ?u.57432
β : Type ?u.57435
γ : Type ?u.57438
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ P ((fun n => (u^[n + 1]) 0) n)
simpa only [Function.iterate_succ_apply'] using hu' _