awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ False
have hi₁ : pred^[Int.toNat (-0)] i0 < i0
Tactic: rw [← h_eq, h] at hi
Cleared hypotheses: hi, h, h_eq
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) ≤ (↑n : ℤ)
have rw : LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) sorry) : ℤ) (↑n : ℤ)
Tactic: rw [toZ_of_ge (le_succ_iterate _ _)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
⊢ LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) ⋯) : ℤ) (↑n : ℤ)
have norm_cast : Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) sorry ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
have inl : ∀ (h : i0 ≤ pred^[n] i0), -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
Tactic: rcases le_or_gt i0 (pred^[n] i0) with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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)
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
have inr : ∀ (h : pred^[n] i0 < i0), -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
Tactic: rcases le_or_gt i0 (pred^[n] i0) with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
have h_eq : pred^[n] i0 = i0
Tactic: have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
have inl : LE.le (α := ℤ) (-(↑n : ℤ)) 0
Tactic: rw [h_eq, toZ_of_eq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -(↑n : ℤ) ≤ toZ i0 (pred^[n] i0)
have inr : LE.le (α := ℤ) (-(↑n : ℤ)) (-(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) sorry) : ℤ))
Tactic: rw [toZ_of_lt h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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) ⋯) : ℤ))
have inr : LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) sorry) : ℤ) (↑n : ℤ)
Tactic: refine Int.neg_le_neg ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ LE.le (α := ℤ) (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) ⋯) : ℤ) (↑n : ℤ)
have inr : Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n] i0) sorry ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)
have h_eq : succ^[m] i0 = succ^[n] i0
Tactic: have h_eq : succ^[m] i0 = succ^[n] i0 := iterate_succ_toZ _ (le_succ_iterate _ _)
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)
have pos : ∀ (hmn : m = n), toZ i0 (succ^[n] i0) = (↑n : ℤ)
Tactic: by_cases hmn : m = n
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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 : ℤ)
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)
have neg : ∀ (hmn : ¬m = n), toZ i0 (succ^[n] i0) = (↑n : ℤ)
Tactic: by_cases hmn : m = n
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)
have pos : toZ i0 (succ^[n] i0) = (↑m : ℤ)
Tactic: nth_rw 2 [← hmn]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (succ^[n] i0) = (↑m : ℤ)
have pos : LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ succ^[n_1] i0 = succ^[n] i0) sorry) : ℤ)
Tactic: rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (succ^[n] i0) = (↑n : ℤ)
have neg : IsMax (succ^[n] i0)
Tactic: suffices IsMax (succ^[n] i0) from absurd this hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n] i0)
⊢ toZ i0 (pred^[n] i0) = -(↑n : ℤ)
have zero : ∀ (hn : ¬IsMin (pred^[0] i0)), toZ i0 (pred^[0] i0) = -(↑0 : ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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 : ℤ)
⊢ toZ i0 (pred^[n] i0) = -(↑n : ℤ)
have succ : ∀ (n : ℕ) (hn : ¬IsMin (pred^[n + 1] i0)), toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have refine : ∀ (h_pred_iterate_eq : pred^[n.succ] i0 = i0), IsMin (pred^[n + 1] i0)
Tactic: refine lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have rwa : pred^[n.succ] i0 = id i0
Tactic: rwa [Function.iterate_zero, id]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ IsMin (pred^[n + 1] i0)
have h_pred_eq_pred : 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]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
have this : 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)
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
have h_eq : pred^[m] i0 = pred^[n.succ] i0
Tactic: have h_eq : pred^[m] i0 = pred^[n.succ] i0 := iterate_pred_toZ _ this
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
have pos : ∀ (hmn : m = n + 1), toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
Tactic: by_cases hmn : m = n + 1
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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) : ℤ)
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
have neg : ∀ (hmn : ¬m = n + 1), toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
Tactic: by_cases hmn : m = n + 1
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
have pos : toZ i0 (pred^[n + 1] i0) = -(↑m : ℤ)
Tactic: nth_rw 2 [← hmn]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (pred^[n + 1] i0) = -(↑m : ℤ)
have pos : LE.le (α := ℤ) 0 (- -(↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) sorry) : ℤ))
Tactic: rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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) ⋯) : ℤ))
have pos : LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n_1 : ℕ) ↦ pred^[n_1] i0 = pred^[n.succ] i0) sorry) : ℤ)
Tactic: rw [neg_neg]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ i0 (pred^[n + 1] i0) = -(↑(n + 1) : ℤ)
have neg : IsMin (pred^[n.succ] i0)
Tactic: suffices IsMin (pred^[n.succ] i0) from absurd this hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : IsSuccArchimedean ι
inst_3 : PredOrder ι
i0 j i : ι
h_le : j < i
⊢ toZ i0 j < toZ i0 i
have contrapose! : ∀ (h_le : toZ i0 i ≤ toZ i0 j), i ≤ j
Tactic: contrapose! h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inl : ∀ (hi : i0 ≤ i), i ≤ j
Tactic: rcases le_or_gt i0 i with hi | hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inr : ∀ (hi : i < i0), i ≤ j
Tactic: rcases le_or_gt i0 i with hi | hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inl : ∀ (hj : i0 ≤ j), i ≤ j
Tactic: rcases le_or_gt i0 j with hj | hj
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inl₁ : ∀ (hj : j < i0), i ≤ j
Tactic: rcases le_or_gt i0 j with hj | hj
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inr : ∀ (hj : i0 ≤ j), i ≤ j
Tactic: rcases le_or_gt i0 j with hj | hj
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inr₁ : ∀ (hj : j < i0), i ≤ j
Tactic: rcases le_or_gt i0 j with hj | hj
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inl : succ^[(toZ i0 i).toNat] i0 ≤ succ^[(toZ i0 j).toNat] i0
Tactic: rw [← iterate_succ_toZ i hi, ← iterate_succ_toZ j hj]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ i ≤ j
have inr : pred^[(-toZ i0 i).toNat] i0 ≤ pred^[(-toZ i0 j).toNat] i0
Tactic: rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have inr : -toZ i0 j ≤ -toZ i0 i
Tactic: refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat ?_)
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
⊢ Countable ι
have inl : IsEmpty ι → Countable ι
Tactic: rcases isEmpty_or_nonempty ι with _ | hι
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inl : IsEmpty ι → Countable ι
⊢ Countable ι
have inr : ∀ (hι : Nonempty ι), Countable ι
Tactic: rcases isEmpty_or_nonempty ι with _ | hι
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
i : ι
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
have 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
Tactic: rcases le_or_gt hι.some i with hi | hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
have 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
Tactic: rcases le_or_gt hι.some i with hi | hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
have h_nonneg : 0 ≤ toZ hι.some i
Tactic: have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
have inl : succ^[(toZ hι.some i).toNat] hι.some = i
Tactic: simp_rw [if_pos h_nonneg]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
have h_neg : toZ hι.some i < 0
Tactic: have h_neg : toZ hι.some i < 0 := toZ_neg hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ (fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
have inr : pred^[(-toZ hι.some i).toNat] hι.some = i
Tactic: simp_rw [if_neg (not_le.mpr h_neg)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : NoMinOrder ι
hι : Nonempty ι
n : ℤ
⊢ toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
have 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
Tactic: rcases le_or_gt 0 n with hn | hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
have 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
Tactic: rcases le_or_gt 0 n with hn | hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
have inl : toZ hι.some (succ^[n.toNat] hι.some) = n
Tactic: simp_rw [if_pos hn]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ toZ hι.some (succ^[n.toNat] hι.some) = n
have inl : (↑n.toNat : ℤ) = n
Tactic: rw [toZ_iterate_succ]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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 : n < 0
⊢ toZ hι.some ((fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
have inr : toZ hι.some (pred^[(-n).toNat] hι.some) = n
Tactic: simp_rw [if_neg (not_le.mpr hn)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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 : n < 0
⊢ toZ hι.some (pred^[(-n).toNat] hι.some) = n
have inr : -(↑(-n).toNat : ℤ) = n
Tactic: rw [toZ_iterate_pred]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : OrderBot ι
n : ℕ
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[n] ⊥)).toNat = n
have rw : Int.toNat (↑n : ℤ) = n
Tactic: rw [toZ_iterate_succ]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : OrderBot ι
i j : ι
⊢ LE.le (α := ℕ)
      (({ toFun := fun (i : ι) ↦ (toZ ⊥ i).toNat, invFun := fun (n : ℕ) ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } :
            (a : ι) → ℕ)
          i :
        ℕ)
      (({ toFun := fun (i : ι) ↦ (toZ ⊥ i).toNat, invFun := fun (n : ℕ) ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } :
            (a : ι) → ℕ)
          j :
        ℕ) ↔
    i ≤ j
have simp : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
Tactic: simp only [Equiv.coe_fn_mk, Int.toNat_le]