α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
⊢ succ ((succ^[n]) a) ≤ (succ^[m]) a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
⊢ IsMax ((succ^[n]) a)
refine' max_of_succ_le (le_trans _ h_eq.symm.le)
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
this : succ ((succ^[n]) a) = (succ^[n + 1]) a
⊢ succ ((succ^[n]) a) ≤ (succ^[m]) a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
⊢ succ ((succ^[n]) a) ≤ (succ^[m]) a
have : succ ((succ^[n]) a) = (succ^[n + 1]) a := by rw [Function.iterate_succ', comp]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
this : succ ((succ^[n]) a) = (succ^[n + 1]) a
⊢ (succ^[n + 1]) a ≤ (succ^[m]) a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
this : succ ((succ^[n]) a) = (succ^[n + 1]) a
⊢ succ ((succ^[n]) a) ≤ (succ^[m]) a
rw [this]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
this : succ ((succ^[n]) a) = (succ^[n + 1]) a
h_le : n + 1 ≤ m
⊢ (succ^[n + 1]) a ≤ (succ^[m]) a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
this : succ ((succ^[n]) a) = (succ^[n + 1]) a
⊢ (succ^[n + 1]) a ≤ (succ^[m]) a
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
this : succ ((succ^[n]) a) = (succ^[n + 1]) a
h_le : n + 1 ≤ m
⊢ (succ^[n + 1]) a ≤ (succ^[m]) a
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_lt : n < m
⊢ succ ((succ^[n]) a) = (succ^[n + 1]) a
rw [Function.iterate_succ', comp]