awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ pred^[n.succ] i0 < i0

Tactic:
lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn ?_

Premises used: Order.pred_iterate_le, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
refine : ∀ (h_pred_iterate_eq : pred^[n.succ] i0 = i0), IsMin (pred^[n + 1] i0)
⊢ pred^[n.succ] i0 < i0

Tactic:
refine lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn ?_

Premises used: Order.pred_iterate_le, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
rwa : pred^[n.succ] i0 = id i0
rwa₁ rwa₂ rwa₃ rwa₄ : pred^[n.succ] i0 = i0
⊢ pred^[n.succ] i0 = pred^[0] i0

Tactic:
rwa [Function.iterate_zero, id]

Premises used: Function.iterate_zero, id
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
⊢ pred^[n.succ] i0 = pred^[0] i0

Tactic:
have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by
      rwa [Function.iterate_zero, id]
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0
⊢ IsMin (pred^[n + 1] i0)

Tactic:
isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)

Premises used: Nat.succ_ne_zero, Order.isMin_iterate_pred_of_eq_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0
⊢ IsMin (pred^[n + 1] i0)

Tactic:
exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)

Premises used: Nat.succ_ne_zero, Order.isMin_iterate_pred_of_eq_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ pred^[n.succ] i0 < i0

Tactic:
have : pred^[n.succ] i0 < i0 := by
    refine lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn ?_
    have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by
      rwa [Function.iterate_zero, id]
    exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
⊢ pred^[m] i0 = pred^[n.succ] i0

Tactic:
have h_eq : pred^[m] i0 = pred^[n.succ] i0 := iterate_pred_toZ _ this
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
pos : ∀ (hmn : m = n + 1), toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
neg : ∀ (hmn : ¬m = n + 1), toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)

Tactic:
by_cases hmn : m = n + 1
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
pos : toZ i0 (pred^[n + 1] i0) = -(↑m : ℤ)
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)

Tactic:
nth_rw 2 [← hmn]
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
pos : LE.le (α := ℤ) 0 (- -(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) ⋯) : ℤ))
⊢ toZ i0 (pred^[n + 1] i0) = -(↑m : ℤ)

Tactic:
rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]

Premises used: neg_neg, max_eq_left, Int.toNat_eq_max, toZ_of_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
pos : LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) ⋯) : ℤ)
⊢ LE.le (α := ℤ) 0 (- -(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) ⋯) : ℤ))

Tactic:
rw [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) ⋯) : ℤ)

Tactic:
Int.natCast_nonneg _

Premises used: Int.natCast_nonneg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) ⋯) : ℤ)

Tactic:
exact Int.natCast_nonneg _

Premises used: Int.natCast_nonneg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
neg : IsMin (pred^[n.succ] i0)
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)

Tactic:
suffices IsMin (pred^[n.succ] i0) from absurd this hn
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ IsMin (pred^[n.succ] i0)

Tactic:
isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)

Premises used: Ne.symm, Order.isMin_iterate_pred_of_eq_of_ne, Eq.symm
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ IsMin (pred^[n.succ] i0)

Tactic:
exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)

Premises used: Ne.symm, Order.isMin_iterate_pred_of_eq_of_ne, Eq.symm
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : j < i
contrapose! : ∀ (h_le : toZ i0 i ≤ toZ i0 j), i ≤ j
⊢ toZ i0 j < toZ i0 i

Tactic:
contrapose! h_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
inl : ∀ (hi : i0 ≤ i), i ≤ j
inr : ∀ (hi : i < i0), i ≤ j
⊢ i ≤ j

Tactic:
rcases le_or_gt i0 i with hi | hi

Premises used: le_or_gt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
inl : ∀ (hj : i0 ≤ j), i ≤ j
inl₁ : ∀ (hj : j < i0), i ≤ j
⊢ i ≤ j

Tactic:
rcases le_or_gt i0 j with hj | hj

Premises used: le_or_gt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
inr : ∀ (hj : i0 ≤ j), i ≤ j
inr₁ : ∀ (hj : j < i0), i ≤ j
⊢ i ≤ j

Tactic:
rcases le_or_gt i0 j with hj | hj

Premises used: le_or_gt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
inl : succ^[(toZ i0 i).toNat] i0 ≤ succ^[(toZ i0 j).toNat] i0
⊢ i ≤ j

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

Premises used: iterate_succ_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
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:
Monotone.monotone_iterate_of_le_map succ_mono (le_succ _) (Int.toNat_le_toNat h_le)

Premises used: Int.toNat_le_toNat, Monotone.monotone_iterate_of_le_map, Order.succ_mono, Order.le_succ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
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)

Premises used: Int.toNat_le_toNat, Monotone.monotone_iterate_of_le_map, Order.succ_mono, Order.le_succ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : j < i0
⊢ i ≤ j

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

Premises used: Iff.mpr, toZ_nonneg, absurd, not_lt, LT.lt.trans_le, toZ_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
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)

Premises used: Iff.mpr, toZ_nonneg, absurd, not_lt, LT.lt.trans_le, toZ_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

Tactic:
hi.le.trans hj

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

Tactic:
exact hi.le.trans hj

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
inr : pred^[(-toZ i0 i).toNat] i0 ≤ pred^[(-toZ i0 j).toNat] i0
⊢ i ≤ j

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

Premises used: iterate_pred_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
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:
Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat ?_)

Premises used: Int.toNat_le_toNat, Order.pred_mono, Order.pred_le, Monotone.antitone_iterate_of_map_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
inr : -toZ i0 j ≤ -toZ i0 i
⊢ 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 ?_)

Premises used: Int.toNat_le_toNat, Order.pred_mono, Order.pred_le, Monotone.antitone_iterate_of_map_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ -toZ i0 j ≤ -toZ i0 i

Tactic:
Int.neg_le_neg h_le

Premises used: Int.neg_le_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
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

Premises used: Int.neg_le_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
⊢ Function.Injective (toZ i0)

Tactic:
toZ_strictMono.injective

Premises used: toZ_strictMono, StrictMono.injective
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i j : ι
⊢ toZ i0 i ≤ toZ i0 j ↔ i ≤ j

Tactic:
toZ_strictMono.le_iff_le

Premises used: toZ_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i j : ι
⊢ toZ i0 i < toZ i0 j ↔ i < j

Tactic:
toZ_strictMono.lt_iff_lt

Premises used: toZ_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i j : ι
⊢ toZ i0 i = toZ i0 j ↔ i = j

Tactic:
injective_toZ.eq_iff

Premises used: Function.Injective.eq_iff, injective_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
inst_4 : NoMaxOrder ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)

Tactic:
toZ_iterate_succ_of_not_isMax n (not_isMax _)

Premises used: not_isMax, toZ_iterate_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
inst_4 : NoMinOrder ι
n : ℕ
⊢ toZ i0 (pred^[n] i0) = -(↑n : ℤ)

Tactic:
toZ_iterate_pred_of_not_isMin n (not_isMin _)

Premises used: not_isMin, toZ_iterate_pred_of_not_isMin
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
hι : Nonempty ι
⊢ ∀ {a b : ι},
    LE.le (α := (↑(Set.range (toZ hι.some)) : Type))
        ((Equiv.ofInjective (toZ hι.some) ⋯ : (a : ι) → (↑(Set.range (toZ hι.some)) : Type)) a :
          (↑(Set.range (toZ hι.some)) : Type))
        ((Equiv.ofInjective (toZ hι.some) ⋯ : (a : ι) → (↑(Set.range (toZ hι.some)) : Type)) b :
          (↑(Set.range (toZ hι.some)) : Type)) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inl : IsEmpty ι → Countable ι
inr : ∀ (hι : Nonempty ι), Countable ι
⊢ Countable ι

Tactic:
rcases isEmpty_or_nonempty ι with _ | hι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
h : IsEmpty ι
⊢ Countable ι

Tactic:
infer_instance
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
hι : Nonempty ι
⊢ Countable ι

Tactic:
Countable.of_equiv _ orderIsoRangeToZOfLinearSuccPredArch.symm.toEquiv

Premises used: Countable.of_equiv, OrderIso.symm, orderIsoRangeToZOfLinearSuccPredArch, RelIso.toEquiv
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
hι : Nonempty ι
⊢ Countable ι

Tactic:
exact Countable.of_equiv _ orderIsoRangeToZOfLinearSuccPredArch.symm.toEquiv

Premises used: Countable.of_equiv, OrderIso.symm, orderIsoRangeToZOfLinearSuccPredArch, RelIso.toEquiv
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
inl :
  ∀ (hi : hι.some ≤ i),
    (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
inr :
  ∀ (hi : i < hι.some),
    (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
rcases le_or_gt hι.some i with hi | hi

Premises used: Nonempty.some, le_or_gt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
⊢ 0 ≤ toZ hι.some i

Tactic:
have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
inl : succ^[(toZ hι.some i).toNat] hι.some = i
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
simp_rw [if_pos h_nonneg]

Premises used: if_pos
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ succ^[(toZ hι.some i).toNat] hι.some = i

Tactic:
iterate_succ_toZ i hi

Premises used: iterate_succ_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ succ^[(toZ hι.some i).toNat] hι.some = i

Tactic:
exact iterate_succ_toZ i hi

Premises used: iterate_succ_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
⊢ toZ hι.some i < 0

Tactic:
have h_neg : toZ hι.some i < 0 := toZ_neg hi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
inr : pred^[(-toZ hι.some i).toNat] hι.some = i
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
simp_rw [if_neg (not_le.mpr h_neg)]

Premises used: not_le, Iff.mpr, if_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
⊢ pred^[(-toZ hι.some i).toNat] hι.some = i

Tactic:
iterate_pred_toZ i hi

Premises used: iterate_pred_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
⊢ pred^[(-toZ hι.some i).toNat] hι.some = i

Tactic:
exact iterate_pred_toZ i hi

Premises used: iterate_pred_toZ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
n : ℤ
inl :
  ∀ (hn : 0 ≤ n),
    toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
inr :
  ∀ (hn : n < 0),
    toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
⊢ toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

Tactic:
rcases le_or_gt 0 n with hn | hn

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
inl : toZ hι.some (succ^[n.toNat] hι.some) = n
⊢ toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

Tactic:
simp_rw [if_pos hn]

Premises used: if_pos
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
inl : (↑n.toNat : ℤ) = n
⊢ toZ hι.some (succ^[n.toNat] hι.some) = n

Tactic:
rw [toZ_iterate_succ]

Premises used: toZ_iterate_succ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ (↑n.toNat : ℤ) = n

Tactic:
Int.toNat_of_nonneg hn

Premises used: Int.toNat_of_nonneg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ (↑n.toNat : ℤ) = n

Tactic:
exact Int.toNat_of_nonneg hn

Premises used: Int.toNat_of_nonneg