case refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0

case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i < 0
refine' lt_of_le_of_ne _ _
case refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n, (pred^[n]) i0 = i))
case refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0
rw [toZ_of_lt hi, neg_nonpos]
no goals
case refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n, (pred^[n]) i0 = i))
exact Nat.cast_nonneg _
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
⊢ False
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0
by_contra h
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : (pred^[Int.toNat (-toZ i0 i)]) i0 = i
⊢ False
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
⊢ False
have h_eq := iterate_pred_toZ i hi
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : (pred^[Int.toNat (-0)]) i0 < i0
h : toZ i0 i = 0
h_eq : (pred^[Int.toNat (-toZ i0 i)]) i0 = i
⊢ False
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : (pred^[Int.toNat (-toZ i0 i)]) i0 = i
⊢ False
rw [← h_eq, h] at hi
no goals
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : (pred^[Int.toNat (-0)]) i0 < i0
h : toZ i0 i = 0
h_eq : (pred^[Int.toNat (-toZ i0 i)]) i0 = i
⊢ False
simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id.def, lt_self_iff_false] at hi