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

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

Tactic:
have h_le_pred : i ≤ pred^[(-toZ i0 j).toNat + 1] i0 := by
  rw [hj_eq]
  refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le i0) (add_le_add_left ?_ _)
  exact Nat.one_le_iff_ne_zero.mpr hm0

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

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

Tactic:
rwa [Function.iterate_succ', Function.comp_apply, iterate_succ_toZ i hi] at h_succ_le

Result:
no goals

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

Tactic:
have h_succ_le : succ^[(toZ i0 i).toNat + 1] i0 ≤ j := by
  rw [hj_eq]
  refine Monotone.monotone_iterate_of_le_map succ_mono (le_succ i0) (add_le_add_left ?_ _)
  exact Nat.one_le_iff_ne_zero.mpr hm0

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

Tactic:
exact Nat.one_le_iff_ne_zero.mpr hm0

Result:
no goals

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
hj_eq : i = pred^[(-toZ i0 j).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 : 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

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

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 + (-toZ i0 j).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 : 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

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

Tactic:
exact (toZ_neg hi).le.trans (toZ_nonneg hj)

Result:
no goals

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

Tactic:
by_contra h

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

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

Tactic:
refine Monotone.monotone_iterate_of_le_map succ_mono (le_succ 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 : 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
⊢ 1 ≤ m

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

Tactic:
exact absurd h_le (not_le.mpr (hj.trans_le hi))

Result:
no goals