ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ ↑(Nat.find (_ : ∃ n, (succ^[n]) i0 = i0)) = 0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ toZ i0 i0 = 0
rw [toZ_of_ge le_rfl]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ Nat.find (_ : ∃ n, (succ^[n]) i0 = i0) = 0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ ↑(Nat.find (_ : ∃ n, (succ^[n]) i0 = i0)) = 0
norm_cast
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ (succ^[0]) i0 = i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ Nat.find (_ : ∃ n, (succ^[n]) i0 = i0) = 0
refine' le_antisymm (Nat.find_le _) (zero_le _)
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ (succ^[0]) i0 = i0
rw [Function.iterate_zero, id.def]