case zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hn : ¬IsMin ((pred^[Nat.zero]) i0)
⊢ toZ i0 ((pred^[Nat.zero]) i0) = -↑Nat.zero

case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[n]) i0)
⊢ toZ i0 ((pred^[n]) i0) = -↑n
cases' n with n n
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
have : (pred^[n.succ]) i0 < i0 := by
  refine' lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn _
  have h_pred_eq_pred : (pred^[n.succ]) i0 = (pred^[0]) i0 := by
    rwa [Function.iterate_zero, id.def]
  exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
let m := (-toZ i0 ((pred^[n.succ]) i0)).toNat
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
have h_eq : (pred^[m]) i0 = (pred^[n.succ]) i0 := iterate_pred_toZ _ this
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
by_cases hmn : m = n.succ
no goals
case zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hn : ¬IsMin ((pred^[Nat.zero]) i0)
⊢ toZ i0 ((pred^[Nat.zero]) i0) = -↑Nat.zero
simp only [Nat.zero_eq, Function.iterate_zero, id.def, toZ_of_eq, Nat.cast_zero, neg_zero]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
h_pred_iterate_eq : (pred^[Nat.succ n]) i0 = i0
⊢ IsMin ((pred^[Nat.succ n]) i0)
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
⊢ (pred^[Nat.succ n]) i0 < i0
refine' lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn _
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
h_pred_iterate_eq : (pred^[Nat.succ n]) i0 = i0
h_pred_eq_pred : (pred^[Nat.succ n]) i0 = (pred^[0]) i0
⊢ IsMin ((pred^[Nat.succ n]) i0)
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
h_pred_iterate_eq : (pred^[Nat.succ n]) i0 = i0
⊢ IsMin ((pred^[Nat.succ n]) i0)
have h_pred_eq_pred : (pred^[n.succ]) i0 = (pred^[0]) i0 := by
  rwa [Function.iterate_zero, id.def]
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
h_pred_iterate_eq : (pred^[Nat.succ n]) i0 = i0
h_pred_eq_pred : (pred^[Nat.succ n]) i0 = (pred^[0]) i0
⊢ IsMin ((pred^[Nat.succ n]) i0)
exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
h_pred_iterate_eq : (pred^[Nat.succ n]) i0 = i0
⊢ (pred^[Nat.succ n]) i0 = (pred^[0]) i0
rwa [Function.iterate_zero, id.def]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑m
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
nth_rw 2 [← hmn]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ 0 ≤ - -↑(Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[Nat.succ n]) i0))
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑m
rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[Nat.succ n]) i0))
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ 0 ≤ - -↑(Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[Nat.succ n]) i0))
rw [neg_neg]
no goals
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : m = Nat.succ n
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n_1, (pred^[n_1]) i0 = (pred^[Nat.succ n]) i0))
exact Nat.cast_nonneg _
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this✝ : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
this : IsMin ((pred^[Nat.succ n]) i0)
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)

case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
⊢ IsMin ((pred^[Nat.succ n]) i0)
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)
suffices : IsMin ((pred^[n.succ]) i0)
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
⊢ IsMin ((pred^[Nat.succ n]) i0)
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this✝ : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
this : IsMin ((pred^[Nat.succ n]) i0)
⊢ toZ i0 ((pred^[Nat.succ n]) i0) = -↑(Nat.succ n)

case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
⊢ IsMin ((pred^[Nat.succ n]) i0)
exact absurd this hn
no goals
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin ((pred^[Nat.succ n]) i0)
this : (pred^[Nat.succ n]) i0 < i0
m : ℕ := Int.toNat (-toZ i0 ((pred^[Nat.succ n]) i0))
h_eq : (pred^[m]) i0 = (pred^[Nat.succ n]) i0
hmn : ¬m = Nat.succ n
⊢ IsMin ((pred^[Nat.succ n]) i0)
exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)