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

Tactic:
exact h (le_of_eq rfl)

Result:
no goals

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 ⋯
hm : succ^[m] i = j
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
by_contra h

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
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ 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
⊢ toZ i0 i ≤ toZ i0 j

Tactic:
rw [le_antisymm h_le (hj_min h_le)]

Result:
no goals

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

Tactic:
exact le_of_not_le h

Result:
no goals

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 : 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:
refine hi_max (max_of_succ_le (le_trans ?_ (@le_of_toZ_le _ _ _ _ _ i0 j i ?_)))

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 : 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
⊢ succ i ≤ j

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

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 ⋯
hm : succ^[m] i = j
⊢ toZ i0 i ≤ toZ i0 j

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

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
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
⊢ 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 ⋯
hm : succ^[m] i = j
hj_eq : j = succ^[(toZ i0 i).toNat + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False

Tactic:
by_cases hm0 : m = 0

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

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

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

Tactic:
refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le i0) (add_le_add_left ?_ _)

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

Proof state:
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
h_le_pred : i ≤ pred^[(-toZ i0 j).toNat + 1] i0
⊢ i ≤ pred j

Tactic:
rwa [Function.iterate_succ', Function.comp_apply, iterate_pred_toZ j hj] at h_le_pred

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

Tactic:
rw [le_antisymm h_le (hi_max h_le)]

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

Tactic:
rw [hj_eq]

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

Tactic:
let m := Nat.find (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 ⋯
⊢ toZ i0 i ≤ toZ i0 j