ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
⊢ toZ i0 ((succ^[n]) i0) = ↑n
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
⊢ toZ i0 ((succ^[n]) i0) = ↑n
let m := (toZ i0 ((succ^[n]) i0)).toNat
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
⊢ toZ i0 ((succ^[n]) i0) = ↑n
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
⊢ toZ i0 ((succ^[n]) i0) = ↑n
have h_eq : (succ^[m]) i0 = (succ^[n]) i0 := iterate_succ_toZ _ (le_succ_iterate _ _)
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : m = n
⊢ toZ i0 ((succ^[n]) i0) = ↑n

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

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

case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : ¬m = n
⊢ IsMax ((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 : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : ¬m = n
⊢ IsMax ((succ^[n]) i0)
exact isMax_iterate_succ_of_eq_of_ne h_eq.symm (Ne.symm hmn)
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : m = n
⊢ toZ i0 ((succ^[n]) i0) = ↑m
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : m = n
⊢ toZ i0 ((succ^[n]) i0) = ↑n
nth_rw 2 [← hmn]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : m = n
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n_1, (succ^[n_1]) i0 = (succ^[n]) i0))
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : m = n
⊢ toZ i0 ((succ^[n]) i0) = ↑m
rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
no goals
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax ((succ^[n]) i0)
m : ℕ := Int.toNat (toZ i0 ((succ^[n]) i0))
h_eq : (succ^[m]) i0 = (succ^[n]) i0
hmn : m = n
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n_1, (succ^[n_1]) i0 = (succ^[n]) i0))
exact Nat.cast_nonneg _