ι : Type ?u.45154
α : Type u
β : Type v
γ : Type w
δ : Type ?u.45163
π : ι → Type ?u.45168
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
ι : Type ?u.45154
α : Type u
β : Type v
γ : Type w
δ : Type ?u.45163
π : ι → Type ?u.45168
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x
rintro rfl
no goals
ι : Type ?u.45154
α : Type u
β : Type v
γ : Type w
δ : Type ?u.45163
π : ι → Type ?u.45168
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
exact (hf.reflect_lt h1).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h2)