case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : IsMax i
⊢ toZ i0 i ≤ toZ i0 j

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
⊢ toZ i0 i ≤ toZ i0 j
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
⊢ toZ i0 i ≤ toZ i0 j
by_cases hi_max : IsMax i
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : IsMin j
⊢ toZ i0 i ≤ toZ i0 j

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
⊢ toZ i0 i ≤ toZ i0 j
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
⊢ toZ i0 i ≤ toZ i0 j
by_cases hj_min : IsMin j
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ toZ i0 i ≤ toZ i0 j

case neg.inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : j < i0
⊢ toZ i0 i ≤ toZ i0 j

case neg.inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : i0 ≤ j
⊢ toZ i0 i ≤ toZ i0 j

case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
⊢ toZ i0 i ≤ toZ i0 j
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
⊢ toZ i0 i ≤ toZ i0 j
cases' le_or_lt i0 i with hi hi <;> cases' le_or_lt i0 j with hj hj
no goals
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : IsMax i
⊢ toZ i0 i ≤ toZ i0 j
rw [le_antisymm h_le (hi_max h_le)]
no goals
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : IsMin j
⊢ toZ i0 i ≤ toZ i0 j
rw [le_antisymm h_le (hj_min h_le)]
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
⊢ toZ i0 i ≤ toZ i0 j
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ toZ i0 i ≤ toZ i0 j
let m := Nat.find (exists_succ_iterate_of_le h_le)
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ toZ i0 i ≤ toZ i0 j
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
⊢ toZ i0 i ≤ toZ i0 j
have hm : (succ^[m]) i = j := Nat.find_spec (exists_succ_iterate_of_le h_le)
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
⊢ toZ i0 i ≤ toZ i0 j
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ toZ i0 i ≤ toZ i0 j
have hj_eq : j = (succ^[(toZ i0 i).toNat + m]) i0 := by
  rw [← hm, add_comm]
  nth_rw 1 [← iterate_succ_toZ i hi]
  rw [Function.iterate_add]
  rfl
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
⊢ toZ i0 i ≤ toZ i0 j
by_contra h
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False
by_cases hm0 : m = 0
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ succ i ≤ j

case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ toZ i0 j ≤ toZ i0 i
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False
refine' hi_max (max_of_succ_le (le_trans _ (@le_of_toZ_le _ _ _ _ _ i0 j i _)))
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ (succ^[m]) i = (succ^[m + Int.toNat (toZ i0 i)]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ j = (succ^[Int.toNat (toZ i0 i) + m]) i0
rw [← hm, add_comm]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ (succ^[m]) ((succ^[Int.toNat (toZ i0 i)]) i0) = (succ^[m + Int.toNat (toZ i0 i)]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ (succ^[m]) i = (succ^[m + Int.toNat (toZ i0 i)]) i0
nth_rw 1 [← iterate_succ_toZ i hi]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ (succ^[m]) ((succ^[Int.toNat (toZ i0 i)]) i0) = (succ^[m] ∘ succ^[Int.toNat (toZ i0 i)]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ (succ^[m]) ((succ^[Int.toNat (toZ i0 i)]) i0) = (succ^[m + Int.toNat (toZ i0 i)]) i0
rw [Function.iterate_add]
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
⊢ (succ^[m]) ((succ^[Int.toNat (toZ i0 i)]) i0) = (succ^[m] ∘ succ^[Int.toNat (toZ i0 i)]) i0
rfl
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
rw [hm0, Function.iterate_zero, id.def] at hm
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 j ≤ toZ i0 j
hm0 : m = 0
⊢ False
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
rw [hm] at h
no goals
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 j ≤ toZ i0 j
hm0 : m = 0
⊢ False
exact h (le_of_eq rfl)
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
h_succ_le : (succ^[Int.toNat (toZ i0 i) + 1]) i0 ≤ j
⊢ succ i ≤ j
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ succ i ≤ j
have h_succ_le : (succ^[(toZ i0 i).toNat + 1]) i0 ≤ j := by
  rw [hj_eq]
  refine' Monotone.monotone_iterate_of_le_map succ_mono (le_succ i0) (add_le_add_left _ _)
  exact Nat.one_le_iff_ne_zero.mpr hm0
no goals
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
h_succ_le : (succ^[Int.toNat (toZ i0 i) + 1]) i0 ≤ j
⊢ succ i ≤ j
rwa [Function.iterate_succ', Function.comp_apply, iterate_succ_toZ i hi] at h_succ_le
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ (succ^[Int.toNat (toZ i0 i) + 1]) i0 ≤ (succ^[Int.toNat (toZ i0 i) + m]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ (succ^[Int.toNat (toZ i0 i) + 1]) i0 ≤ j
rw [hj_eq]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ 1 ≤ m
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ (succ^[Int.toNat (toZ i0 i) + 1]) i0 ≤ (succ^[Int.toNat (toZ i0 i) + m]) i0
refine' Monotone.monotone_iterate_of_le_map succ_mono (le_succ i0) (add_le_add_left _ _)
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ 1 ≤ m
exact Nat.one_le_iff_ne_zero.mpr hm0
no goals
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, (succ^[n]) i = j)
hm : (succ^[m]) i = j
hj_eq : j = (succ^[Int.toNat (toZ i0 i) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ toZ i0 j ≤ toZ i0 i
exact le_of_not_le h
no goals
case neg.inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : j < i0
⊢ toZ i0 i ≤ toZ i0 j
exact absurd h_le (not_le.mpr (hj.trans_le hi))
no goals
case neg.inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : i0 ≤ j
⊢ toZ i0 i ≤ toZ i0 j
exact (toZ_neg hi).le.trans (toZ_nonneg hj)
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
⊢ toZ i0 i ≤ toZ i0 j
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
⊢ toZ i0 i ≤ toZ i0 j
let m := Nat.find (exists_pred_iterate_of_le h_le)
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ toZ i0 i ≤ toZ i0 j
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
⊢ toZ i0 i ≤ toZ i0 j
have hm : (pred^[m]) j = i := Nat.find_spec (exists_pred_iterate_of_le h_le)
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
⊢ toZ i0 i ≤ toZ i0 j
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ toZ i0 i ≤ toZ i0 j
have hj_eq : i = (pred^[(-toZ i0 j).toNat + m]) i0 := by
  rw [← hm, add_comm]
  nth_rw 1 [← iterate_pred_toZ j hj]
  rw [Function.iterate_add]
  rfl
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
⊢ toZ i0 i ≤ toZ i0 j
by_contra h
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False
by_cases hm0 : m = 0
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ j ≤ pred j
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False
refine' hj_min (min_of_le_pred _)
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ toZ i0 j ≤ toZ i0 i

case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ i ≤ pred j
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ j ≤ pred j
refine' (@le_of_toZ_le _ _ _ _ _ i0 j i _).trans _
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ (pred^[m]) j = (pred^[m + Int.toNat (-toZ i0 j)]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
rw [← hm, add_comm]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ (pred^[m]) ((pred^[Int.toNat (-toZ i0 j)]) i0) = (pred^[m + Int.toNat (-toZ i0 j)]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ (pred^[m]) j = (pred^[m + Int.toNat (-toZ i0 j)]) i0
nth_rw 1 [← iterate_pred_toZ j hj]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ (pred^[m]) ((pred^[Int.toNat (-toZ i0 j)]) i0) = (pred^[m] ∘ pred^[Int.toNat (-toZ i0 j)]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ (pred^[m]) ((pred^[Int.toNat (-toZ i0 j)]) i0) = (pred^[m + Int.toNat (-toZ i0 j)]) i0
rw [Function.iterate_add]
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
⊢ (pred^[m]) ((pred^[Int.toNat (-toZ i0 j)]) i0) = (pred^[m] ∘ pred^[Int.toNat (-toZ i0 j)]) i0
rfl
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
rw [hm0, Function.iterate_zero, id.def] at hm
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 i
hm0 : m = 0
⊢ False
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
rw [hm] at h
no goals
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 i
hm0 : m = 0
⊢ False
exact h (le_of_eq rfl)
no goals
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ toZ i0 j ≤ toZ i0 i
exact le_of_not_le h
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
h_le_pred : i ≤ (pred^[Int.toNat (-toZ i0 j) + 1]) i0
⊢ i ≤ pred j
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ i ≤ pred j
have h_le_pred : i ≤ (pred^[(-toZ i0 j).toNat + 1]) i0 := by
  rw [hj_eq]
  refine' Monotone.antitone_iterate_of_map_le pred_mono (pred_le i0) (add_le_add_left _ _)
  exact Nat.one_le_iff_ne_zero.mpr hm0
no goals
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
h_le_pred : i ≤ (pred^[Int.toNat (-toZ i0 j) + 1]) i0
⊢ i ≤ pred j
rwa [Function.iterate_succ', Function.comp_apply, iterate_pred_toZ j hj] at h_le_pred
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ (pred^[Int.toNat (-toZ i0 j) + m]) i0 ≤ (pred^[Int.toNat (-toZ i0 j) + 1]) i0
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ i ≤ (pred^[Int.toNat (-toZ i0 j) + 1]) i0
rw [hj_eq]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ 1 ≤ m
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ (pred^[Int.toNat (-toZ i0 j) + m]) i0 ≤ (pred^[Int.toNat (-toZ i0 j) + 1]) i0
refine' Monotone.antitone_iterate_of_map_le pred_mono (pred_le i0) (add_le_add_left _ _)
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, (pred^[n]) j = i)
hm : (pred^[m]) j = i
hj_eq : i = (pred^[Int.toNat (-toZ i0 j) + m]) i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ 1 ≤ m
exact Nat.one_le_iff_ne_zero.mpr hm0