ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b, b > a ∧ P n b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
simp only [frequently_atTop'] at h
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b, b > a ∧ P n b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
choose u hu hu' using h
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ (StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) ∧
    ∀ (n : ℕ), P n ((fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) n)
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
use (fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v : ℕ → ℕ)
case left
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v

case right
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n ((fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) n)
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ (StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) ∧
    ∀ (n : ℕ), P n ((fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) n)
constructor
case left.hf
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), (Nat.recOn n (u 0 0) fun n v => u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v => u (n + 1) v
case left
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v
apply strictMono_nat_of_lt_succ
case left.hf
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ (Nat.recOn n (u 0 0) fun n v => u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v => u (n + 1) v
case left.hf
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), (Nat.recOn n (u 0 0) fun n v => u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v => u (n + 1) v
intro n
no goals
case left.hf
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ (Nat.recOn n (u 0 0) fun n v => u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v => u (n + 1) v
apply hu
case right
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P n ((fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) n)
case right
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n ((fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) n)
intro n
no goals
case right
ι : Type ?u.59096
ι' : Type ?u.59099
α : Type ?u.59102
β : Type ?u.59105
γ : Type ?u.59108
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P n ((fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) n)
cases n <;> simp [hu']