-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem toZ_mono {i j : ι} (h_le : i ≤ j) : toZ i0 i ≤ toZ i0 j

Proof state:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : pred^[m] j = i
hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

Tactic:
rw [hm0, Function.iterate_zero, id] at hm

Result:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : j = i
hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

Proof state:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : i = j
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

Tactic:
rw [hm] at h

Result:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : i = j
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
h : ¬toZ i0 j ≤ toZ i0 j
hm0 : m = 0
⊢ False

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

Tactic:
by_cases hj_min : IsMin j

Result:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 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 j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
⊢ toZ i0 i ≤ toZ i0 j

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
by_cases hi_max : IsMax i

Result:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 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 j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
⊢ toZ i0 i ≤ toZ i0 j

Proof state:
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
have hm : succ^[m] i = j := Nat.find_spec (exists_succ_iterate_of_le h_le)

Result:
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
⊢ toZ i0 i ≤ toZ i0 j

Proof state:
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : pred^[m] j = i
hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False

Tactic:
refine hj_min (min_of_le_pred ?_)

Result:
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : pred^[m] j = i
hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ j ≤ pred j

Proof state:
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 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

Tactic:
let m := Nat.find (exists_succ_iterate_of_le h_le)

Result:
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
⊢ toZ i0 i ≤ toZ i0 j

Proof state:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

Tactic:
rw [hm0, Function.iterate_zero, id] at hm

Result:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : i = j
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
⊢ succ^[m] (succ^[(toZ i0 i).toNat] i0) = succ^[m + (toZ i0 i).toNat] i0

Tactic:
rw [Function.iterate_add]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
⊢ succ^[m] (succ^[(toZ i0 i).toNat] i0) = (succ^[m] ∘ succ^[(toZ i0 i).toNat]) i0

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : pred^[m] j = i
⊢ pred^[m] (pred^[(-toZ i0 j).toNat] i0) = (pred^[m] ∘ pred^[(-toZ i0 j).toNat]) i0

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : pred^[m] j = i
⊢ i = pred^[(-toZ i0 j).toNat + m] i0

Tactic:
rw [← hm, add_comm]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find ⋯
hm : pred^[m] j = i
⊢ pred^[m] j = pred^[m + (-toZ i0 j).toNat] i0