case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ (pred^[n]) i0
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)

case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : (pred^[n]) i0 < i0
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)
cases' le_or_lt i0 ((pred^[n]) i0) with h h
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ (pred^[n]) i0
h_eq : (pred^[n]) i0 = i0
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ (pred^[n]) i0
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)
have h_eq : (pred^[n]) i0 = i0 := le_antisymm (pred_iterate_le _ _) h
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ (pred^[n]) i0
h_eq : (pred^[n]) i0 = i0
⊢ -↑n ≤ 0
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ (pred^[n]) i0
h_eq : (pred^[n]) i0 = i0
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)
rw [h_eq, toZ_of_eq]
no goals
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ (pred^[n]) i0
h_eq : (pred^[n]) i0 = i0
⊢ -↑n ≤ 0
simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : (pred^[n]) i0 < i0
⊢ ↑(Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[n]) i0)) ≤ ↑n
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : (pred^[n]) i0 < i0
⊢ -↑n ≤ toZ i0 ((pred^[n]) i0)
rw [toZ_of_lt h, neg_le_neg_iff]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : (pred^[n]) i0 < i0
⊢ Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[n]) i0) ≤ n
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : (pred^[n]) i0 < i0
⊢ ↑(Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[n]) i0)) ≤ ↑n
norm_cast
no goals
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : (pred^[n]) i0 < i0
⊢ Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[n]) i0) ≤ n
exact Nat.find_min' _ rfl