ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ ↑(Nat.find (_ : ∃ n_1, (succ^[n_1]) i0 = (succ^[n]) i0)) ≤ ↑n
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ toZ i0 ((succ^[n]) i0) ≤ ↑n
rw [toZ_of_ge (le_succ_iterate _ _)]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ Nat.find (_ : ∃ n_1, (succ^[n_1]) i0 = (succ^[n]) i0) ≤ n
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ ↑(Nat.find (_ : ∃ n_1, (succ^[n_1]) i0 = (succ^[n]) i0)) ≤ ↑n
norm_cast
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ Nat.find (_ : ∃ n_1, (succ^[n_1]) i0 = (succ^[n]) i0) ≤ n
exact Nat.find_min' _ rfl