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

Proof state:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ pred^[(-toZ i0 i).toNat] i0 ≤ pred^[(-toZ i0 j).toNat] i0

Tactic:
refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat ?_)

Result:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ -toZ i0 j ≤ -toZ i0 i

Proof state:
case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ succ^[(toZ i0 i).toNat] i0 ≤ succ^[(toZ i0 j).toNat] i0

Tactic:
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ _) (Int.toNat_le_toNat h_le)

Result:
no goals

Proof state:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j

Tactic:
rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]

Result:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ pred^[(-toZ i0 i).toNat] i0 ≤ pred^[(-toZ i0 j).toNat] i0

Proof state:
case inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : j < i0
⊢ i ≤ j

Tactic:
exact absurd ((toZ_neg hj).trans_le (toZ_nonneg hi)) (not_lt.mpr h_le)

Result:
no goals

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

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

Result:
case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ i ≤ j

case inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : j < i0
⊢ i ≤ j

case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j

Proof state:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ -toZ i0 j ≤ -toZ i0 i

Tactic:
exact Int.neg_le_neg h_le

Result:
no goals

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

Tactic:
rw [← iterate_succ_toZ i hi, ← iterate_succ_toZ j hj]

Result:
case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ succ^[(toZ i0 i).toNat] i0 ≤ succ^[(toZ i0 j).toNat] i0

Proof state:
case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

Tactic:
exact hi.le.trans hj

Result:
no goals