-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem toZ_mono {i j : ι} (h_le : 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
⊢ j ≤ pred j

Tactic:
refine (@le_of_toZ_le _ _ _ _ _ i0 j i ?_).trans ?_

Result:
case neg.refine_1
ι : 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
⊢ toZ i0 j ≤ toZ i0 i

case neg.refine_2
ι : 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
⊢ i ≤ pred 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
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
rcases le_or_lt i0 i with hi | hi <;> rcases le_or_lt i0 j with hj | hj

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
⊢ toZ i0 i ≤ toZ i0 j

case neg.inl.inr
ι : 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 : 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 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 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

Proof state:
case neg.inr.inr
ι : 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 ⋯
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
have hm : pred^[m] j = i := Nat.find_spec (exists_pred_iterate_of_le (α := ι) h_le)

Result:
case neg.inr.inr
ι : 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
⊢ 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
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
⊢ j = succ^[(toZ i0 i).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 : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
⊢ succ^[m] i = succ^[m + (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 : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find ⋯
hm : succ^[m] i = j
⊢ succ^[m] i = succ^[m + (toZ i0 i).toNat] i0

Tactic:
nth_rw 1 [← iterate_succ_toZ i hi]

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 + (toZ i0 i).toNat] i0

Proof state:
case neg.inr.inr
ι : 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
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
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

Result:
case neg.inr.inr
ι : 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
⊢ 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 : j = i
hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 i
hm0 : m = 0
⊢ False

Tactic:
exact h (le_of_eq rfl)

Result:
no goals

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 : 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 [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 : 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 i
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 : 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
⊢ 1 ≤ m

Tactic:
exact Nat.one_le_iff_ne_zero.mpr hm0

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
⊢ pred^[m] j = pred^[m + (-toZ i0 j).toNat] i0

Tactic:
nth_rw 1 [← iterate_pred_toZ j hj]

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] (pred^[(-toZ i0 j).toNat] i0) = pred^[m + (-toZ i0 j).toNat] i0

Proof state:
case neg.refine_1
ι : 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
⊢ toZ i0 j ≤ toZ i0 i

Tactic:
exact le_of_not_le h

Result:
no goals