awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun (n : ℕ) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Finset.Icc i j) (succ^[n] i) ⋯
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
inl : ∀ (h_le : n ≤ m), ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
inr : ∀ (h_le : m ≤ n), ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i

Tactic:
rcases le_total n m with h_le | h_le

Premises used: le_total
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun (n : ℕ) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Finset.Icc i j) (succ^[n] i) ⋯
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : n ≤ m
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i

Tactic:
⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩

Premises used: And.intro, Exists.intro, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun (n : ℕ) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Finset.Icc i j) (succ^[n] i) ⋯
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : n ≤ m
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i

Tactic:
exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun (n : ℕ) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Finset.Icc i j) (succ^[n] i) ⋯
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : m ≤ n
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i

Tactic:
⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩

Premises used: Ne.symm, And.intro, Exists.intro, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun (n : ℕ) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Finset.Icc i j) (succ^[n] i) ⋯
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : m ≤ n
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i

Tactic:
exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
inl : ∀ (n m : ℕ) (hnm : n < m) (h_eq : succ^[n] i = succ^[m] i), False
⊢ False

Tactic:
obtain ⟨n, m, hnm, h_eq⟩ : ∃ n m, n < m ∧ succ^[n] i = succ^[m] i := by
      let f : ℕ → Finset.Icc i j := fun n ↦ ⟨succ^[n] i, h_mem n⟩
      obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m :=
        Finite.exists_ne_map_eq_of_infinite f
      have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [f, Subtype.mk_eq_mk] using hfnm
      rcases le_total n m with h_le | h_le
      · exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
      · exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
n m : ℕ
hnm : n < m
h_eq : succ^[n] i = succ^[m] i
⊢ IsMax (succ^[n] i)

Tactic:
have h_max : IsMax (succ^[n] i) := isMax_iterate_succ_of_eq_of_ne h_eq hnm.ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
n m : ℕ
hnm : n < m
h_eq : succ^[n] i = succ^[m] i
h_max : IsMax (succ^[n] i)
⊢ False

Tactic:
not_le.mpr (h_lt n) (h_max (h_lt n).le)

Premises used: not_le, Iff.mpr, LT.lt.le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
n m : ℕ
hnm : n < m
h_eq : succ^[n] i = succ^[m] i
h_max : IsMax (succ^[n] i)
⊢ False

Tactic:
exact not_le.mpr (h_lt n) (h_max (h_lt n).le)

Premises used: not_le, Iff.mpr, LT.lt.le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : PredOrder ι
⊢ IsPredArchimedean ι

Tactic:
inferInstanceAs (IsPredArchimedean ιᵒᵈᵒᵈ)

Premises used: _private.0.LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder._proof_1
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ toZ i0 i = (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯) : ℤ)

Tactic:
dif_pos hi

Premises used: toZ, dif_pos
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i = -(↑(Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) ⋯) : ℤ)

Tactic:
dif_neg (not_le.mpr hi)

Premises used: not_le, Iff.mpr, toZ, dif_neg
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
rw : Eq (α := ℤ) (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯) : ℤ) 0
⊢ toZ i0 i0 = 0

Tactic:
rw [toZ_of_ge le_rfl]

Premises used: le_rfl, toZ_of_ge
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
norm_cast : Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯ = 0
⊢ Eq (α := ℤ) (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯) : ℤ) 0

Tactic:
norm_cast
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
rw : Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯ ≤ 0
⊢ Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯ = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
hn : succ^[0] i0 = i0
⊢ Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯ ≤ 0

Tactic:
apply Nat.find_le

Premises used: Nat.find_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
hn : id i0 = i0
hn₁ hn₂ : i0 = i0
⊢ succ^[0] i0 = i0

Tactic:
rw [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 i : ι
hi : i0 ≤ i
rw : succ^[Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯] i0 = i
⊢ succ^[(toZ i0 i).toNat] i0 = i

Tactic:
rw [toZ_of_ge hi, Int.toNat_natCast]

Premises used: Int.toNat_natCast, toZ_of_ge
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯] i0 = i

Tactic:
Nat.find_spec (exists_succ_iterate_of_le hi)

Premises used: IsSuccArchimedean.exists_succ_iterate_of_le, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯] i0 = i

Tactic:
exact Nat.find_spec (exists_succ_iterate_of_le hi)

Premises used: IsSuccArchimedean.exists_succ_iterate_of_le, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
rw : pred^[Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) ⋯] i0 = i
⊢ pred^[(-toZ i0 i).toNat] i0 = i

Tactic:
rw [toZ_of_lt hi, neg_neg, Int.toNat_natCast]

Premises used: Int.toNat_natCast, neg_neg, toZ_of_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) ⋯] i0 = i

Tactic:
Nat.find_spec (exists_pred_iterate_of_le hi.le)

Premises used: IsPredArchimedean.exists_pred_iterate_of_le, LT.lt.le, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) ⋯] i0 = i

Tactic:
exact Nat.find_spec (exists_pred_iterate_of_le hi.le)

Premises used: IsPredArchimedean.exists_pred_iterate_of_le, LT.lt.le, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i0 ≤ i
rw : LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯) : ℤ)
⊢ 0 ≤ toZ i0 i

Tactic:
rw [toZ_of_ge hi]

Premises used: toZ_of_ge
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯) : ℤ)

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 i : ι
hi : i0 ≤ i
⊢ LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) ⋯) : ℤ)

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 i : ι
hi : i < i0
⊢ toZ i0 i < 0

Tactic:
lt_of_le_of_ne ?_ ?_

Premises used: 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 i : ι
hi : i < i0
refine_1 : toZ i0 i ≤ 0
refine_2 : toZ i0 i ≠ 0
⊢ toZ i0 i < 0

Tactic:
refine lt_of_le_of_ne ?_ ?_

Premises used: 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 i : ι
hi : i < i0
refine_1 : LE.le (α := ℤ) (-(↑(Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) ⋯) : ℤ)) 0
⊢ toZ i0 i ≤ 0

Tactic:
rw [toZ_of_lt hi]

Premises used: toZ_of_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
⊢ LE.le (α := ℤ) (-(↑(Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) ⋯) : ℤ)) 0

Tactic:
lia
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
refine_2 : ∀ (h : toZ i0 i = 0), False
⊢ toZ i0 i ≠ 0

Tactic:
by_contra h
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
⊢ pred^[(-toZ i0 i).toNat] i0 = i

Tactic:
have h_eq := iterate_pred_toZ i hi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ pred^[Int.toNat (-0)] i0 < i0

Tactic:
rw [← h_eq, h] at hi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
hi₁ : pred^[Int.toNat (-0)] i0 < i0
⊢ toZ i0 i = 0

Tactic:
rw [← h_eq, h] at hi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
hi₁ : pred^[Int.toNat (-0)] i0 < i0
h₁ : toZ i0 i = 0
⊢ pred^[(-toZ i0 i).toNat] i0 = i

Tactic:
rw [← h_eq, h] at hi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 i : ι
hi : pred^[Int.toNat (-0)] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Tactic:
simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id, lt_self_iff_false] at hi

Premises used: Function.iterate_zero, id, Int.toNat_zero, lt_self_iff_false, neg_zero
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
rw : LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯) : ℤ) (↑n : ℤ)
⊢ toZ i0 (succ^[n] i0) ≤ (↑n : ℤ)

Tactic:
rw [toZ_of_ge (le_succ_iterate _ _)]

Premises used: toZ_of_ge, Order.le_succ_iterate
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
norm_cast : Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯ ≤ n
⊢ LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯) : ℤ) (↑n : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯ ≤ n

Tactic:
Nat.find_min' _ rfl

Premises used: Nat.find_min', rfl
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯ ≤ n

Tactic:
exact Nat.find_min' _ rfl

Premises used: Nat.find_min', rfl
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
inl : ∀ (h : i0 ≤ pred^[n] i0), -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
inr : ∀ (h : pred^[n] i0 < i0), -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)

Tactic:
rcases le_or_gt i0 (pred^[n] i0) with h | h

Premises used: Nat.iterate, le_or_gt, Order.pred
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
⊢ pred^[n] i0 = i0

Tactic:
have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
inl : LE.le (α := ℤ) (-(↑n : ℤ)) 0
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)

Tactic:
rw [h_eq, toZ_of_eq]

Premises used: toZ_of_eq
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ LE.le (α := ℤ) (-(↑n : ℤ)) 0

Tactic:
lia
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
inr : LE.le (α := ℤ) (-(↑n : ℤ)) (-(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯) : ℤ))
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)

Tactic:
rw [toZ_of_lt h]

Premises used: 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 : ℕ
h : pred^[n] i0 < i0
⊢ LE.le (α := ℤ) (-(↑n : ℤ)) (-(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯) : ℤ))

Tactic:
Int.neg_le_neg ?_

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 : ι
n : ℕ
h : pred^[n] i0 < i0
inr : LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯) : ℤ) (↑n : ℤ)
⊢ LE.le (α := ℤ) (-(↑n : ℤ)) (-(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯) : ℤ))

Tactic:
refine Int.neg_le_neg ?_

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 : ι
n : ℕ
h : pred^[n] i0 < i0
inr : Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯ ≤ n
⊢ LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯) : ℤ) (↑n : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯ ≤ n

Tactic:
Nat.find_min' _ rfl

Premises used: Nat.find_min', rfl
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯ ≤ n

Tactic:
exact Nat.find_min' _ rfl

Premises used: Nat.find_min', rfl
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
⊢ succ^[m] i0 = succ^[n] i0

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

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

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 : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
pos : LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯) : ℤ)
⊢ toZ i0 (succ^[n] i0) = (↑m : ℤ)

Tactic:
rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]

Premises used: toZ_of_ge, max_eq_left, Int.toNat_eq_max, Order.le_succ_iterate
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] 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 : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] 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 : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
neg : IsMax (succ^[n] i0)
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)

Tactic:
suffices IsMax (succ^[n] 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 : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ IsMax (succ^[n] i0)

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

Premises used: Ne.symm, Order.isMax_iterate_succ_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 : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ IsMax (succ^[n] i0)

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

Premises used: Ne.symm, Order.isMax_iterate_succ_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] i0)
zero : ∀ (hn : ¬IsMin (pred^[0] i0)), toZ i0 (pred^[0] i0) = -(↑0 : ℤ)
succ : ∀ (n : ℕ) (hn : ¬IsMin (pred^[n + 1] i0)), toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
⊢ toZ i0 (pred^[n] i0) = -(↑n : ℤ)

Tactic:
rcases n with - | n
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
hn : ¬IsMin (pred^[0] i0)
⊢ toZ i0 (pred^[0] i0) = -(↑0 : ℤ)

Tactic:
simp