awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : n < 0
inr : toZ hι.some (pred^[(-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_neg (not_le.mpr hn)]

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 ι
n : ℤ
hn : n < 0
inr : -(↑(-n).toNat : ℤ) = n
⊢ toZ hι.some (pred^[(-n).toNat] hι.some) = n

Tactic:
rw [toZ_iterate_pred]

Premises used: toZ_iterate_pred
-- 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 : n < 0
⊢ -(↑(-n).toNat : ℤ) = n

Tactic:
simp only [hn.le, Int.toNat_of_nonneg, Int.neg_nonneg_of_nonpos, Int.neg_neg]

Premises used: Int.toNat_of_nonneg, LT.lt.le, Int.neg_nonneg_of_nonpos, Int.neg_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 ι
⊢ ∀ {a b : ι},
    LE.le (α := ℤ)
        (({ toFun := toZ hι.some,
                invFun := fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some,
                left_inv := ⋯, right_inv := ⋯ : ι ≃ ℤ } :
              (a : ι) → ℤ)
            a :
          ℤ)
        (({ toFun := toZ hι.some,
                invFun := fun (n : ℤ) ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some,
                left_inv := ⋯, right_inv := ⋯ : ι ≃ ℤ } :
              (a : ι) → ℤ)
            b :
          ℤ) ↔
      a ≤ b

Tactic:
simp
-- 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 : OrderBot ι
i : ι
⊢ succ^[(toZ ⊥ i).toNat] ⊥ = i

Tactic:
iterate_succ_toZ i bot_le

Premises used: iterate_succ_toZ, bot_le
-- 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 : OrderBot ι
i : ι
⊢ succ^[(toZ ⊥ i).toNat] ⊥ = i

Tactic:
exact iterate_succ_toZ i bot_le

Premises used: iterate_succ_toZ, bot_le
-- 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 : OrderBot ι
n : ℕ
rw : Int.toNat (↑n : ℤ) = n
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[n] ⊥)).toNat = 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 : OrderBot ι
n : ℕ
⊢ Int.toNat (↑n : ℤ) = n

Tactic:
Int.toNat_natCast n

Premises used: Int.toNat_natCast
-- 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 : OrderBot ι
n : ℕ
⊢ Int.toNat (↑n : ℤ) = n

Tactic:
exact Int.toNat_natCast n

Premises used: Int.toNat_natCast
-- 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 : OrderBot ι
i j : ι
simp : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ 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

Tactic:
simp only [Equiv.coe_fn_mk, Int.toNat_le]

Premises used: Int.toNat_le, Equiv.coe_fn_mk
-- 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 : OrderBot ι
i j : ι
rw : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ toZ ⊥ i ≤ toZ ⊥ j
rw₁ rw₂ : toZ ⊥ i ≤ toZ ⊥ j ↔ toZ ⊥ i ≤ toZ ⊥ j
⊢ toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j

Tactic:
rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

Premises used: Int.toNat_of_nonneg, toZ_nonneg, toZ_le_toZ, bot_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
a :
  (↑((fun (i : ι) ↦
            (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat ⋯ :
              ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))))
          ((fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ (succ^[(↑n : ℕ)] ⊥ : ι)) n)) :
      ℕ) =
    (↑n : ℕ)
⊢ (fun (i : ι) ↦
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat ⋯ :
          ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))))
      ((fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ (succ^[(↑n : ℕ)] ⊥ : ι)) n) =
    n

Tactic:
ext1
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
a : (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat = (↑n : ℕ)
⊢ (↑((fun (i : ι) ↦
            (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat ⋯ :
              ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))))
          ((fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ (succ^[(↑n : ℕ)] ⊥ : ι)) n)) :
      ℕ) =
    (↑n : ℕ)

Tactic:
simp only
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat = (↑n : ℕ)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
a : (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat ≤ (↑n : ℕ)
a₁ : (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat = (↑n : ℕ)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
a : toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥) ≤ (↑(↑n : ℕ) : ℤ)
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat ≤ (↑n : ℕ)

Tactic:
rw [Int.toNat_le]

Premises used: Int.toNat_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥) ≤ (↑(↑n : ℕ) : ℤ)

Tactic:
toZ_iterate_succ_le _

Premises used: toZ_iterate_succ_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥) ≤ (↑(↑n : ℕ) : ℤ)

Tactic:
exact toZ_iterate_succ_le _

Premises used: toZ_iterate_succ_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
pos : ∀ (hn_max : IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)), (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
neg :
  ∀ (hn_max : ¬IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)), (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat

Tactic:
by_cases hn_max : IsMax (succ^[↑n] (⊥ : ι))

Premises used: Order.succ, Bot.bot, Nat.iterate, Subtype.val, IsMax
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)
⊢ Eq.{u_1 + 1} (α := ι) (succ^[(↑n : ℕ)] ⊥) ⊤

Tactic:
rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max

Premises used: isTop_iff_isMax, isTop_iff_eq_top
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : Eq.{u_1 + 1} (α := ι) (succ^[(↑n : ℕ)] ⊥) ⊤
pos : (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ ⊤).toNat
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat

Tactic:
rw [hn_max]
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : Eq.{u_1 + 1} (α := ι) (succ^[(↑n : ℕ)] ⊥) ⊤
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ ⊤).toNat

Tactic:
Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)

Premises used: Finset.mem_range, Nat.lt_succ_iff, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : Eq.{u_1 + 1} (α := ι) (succ^[(↑n : ℕ)] ⊥) ⊤
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ ⊤).toNat

Tactic:
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)

Premises used: Finset.mem_range, Nat.lt_succ_iff, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)
neg : (↑n : ℕ) ≤ Int.toNat (↑(↑n : ℕ) : ℤ)
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat

Tactic:
rw [toZ_iterate_succ_of_not_isMax _ hn_max]

Premises used: toZ_iterate_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)
⊢ (↑n : ℕ) ≤ Int.toNat (↑(↑n : ℕ) : ℤ)

Tactic:
simp only [Int.toNat_natCast, le_refl]

Premises used: Int.toNat_natCast, le_refl
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
i j : ι
simp : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
⊢ LE.le (α := ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)))
      ((({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat
                    ⋯,
                invFun := fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ succ^[(↑n : ℕ)] ⊥,
                left_inv := ⋯, right_inv := ⋯ } :
              ι ≃ ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) :
            (a : ι) → ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1)))
          i :
        ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)))
      ((({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat
                    ⋯,
                invFun := fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ succ^[(↑n : ℕ)] ⊥,
                left_inv := ⋯, right_inv := ⋯ } :
              ι ≃ ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) :
            (a : ι) → ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1)))
          j :
        ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↔
    i ≤ j

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Int.toNat_le]

Premises used: Int.toNat_le, Equiv.coe_fn_mk, Subtype.mk_le_mk
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
i j : ι
rw : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ toZ ⊥ i ≤ toZ ⊥ j
rw₁ rw₂ : toZ ⊥ i ≤ toZ ⊥ j ↔ toZ ⊥ i ≤ toZ ⊥ j
⊢ toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j

Tactic:
rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

Premises used: Int.toNat_of_nonneg, toZ_nonneg, toZ_le_toZ, bot_le
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
⊢ Countable ι

Tactic:
have := LinearLocallyFiniteOrder.succOrder ι
  have := LinearLocallyFiniteOrder.predOrder ι
  countable_of_linear_succ_pred_arch

Premises used: LinearLocallyFiniteOrder.predOrder, countable_of_linear_succ_pred_arch, LinearLocallyFiniteOrder.succOrder
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico n m, r i (succ i)
hnm : n ≤ m
revert : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
⊢ ReflTransGen r n m

Tactic:
revert h
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m

Tactic:
Succ.rec ?_ ?_ hnm

Premises used: Succ.rec
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
refine_1 : ∀ (h : ∀ i ∈ Ico n n, r i (succ i)), ReflTransGen r n n
refine_2 :
  ∀ (n_1 : α) (hmn : n ≤ n_1),
    (∀ (h : ∀ i ∈ Ico n n_1, r i (succ i)), ReflTransGen r n n_1) →
      ∀ (h : ∀ i ∈ Ico n (succ n_1), r i (succ i)), ReflTransGen r n (succ n_1)
⊢ ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m

Tactic:
refine Succ.rec ?_ ?_ hnm
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
h : ∀ i ∈ Ico n n, r i (succ i)
⊢ ReflTransGen r n n

Tactic:
ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
h : ∀ i ∈ Ico n n, r i (succ i)
⊢ ReflTransGen r n n

Tactic:
exact ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
⊢ ReflTransGen r n m

Tactic:
have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
refine_2 : ∀ (hm : m = succ m), ReflTransGen r n (succ m)
refine_2₁ : ∀ (hm : m < succ m), ReflTransGen r n (succ m)
⊢ ReflTransGen r n (succ m)

Tactic:
rcases (le_succ m).eq_or_lt with hm | hm

Premises used: LE.le.eq_or_lt, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
hm : m = succ m
refine_2 refine_2₁ refine_2₂ refine_2₃ : ReflTransGen r n m
⊢ ReflTransGen r n (succ m)

Tactic:
rwa [← hm]
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
hm : m < succ m
⊢ ReflTransGen r n (succ m)

Tactic:
this.tail (h m ⟨hnm, hm⟩)

Premises used: And.intro, Relation.ReflTransGen.tail
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
hm : m < succ m
⊢ ReflTransGen r n (succ m)

Tactic:
exact this.tail (h m ⟨hnm, hm⟩)

Premises used: And.intro, Relation.ReflTransGen.tail
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
rw : ReflTransGen (swap (φ := fun (a a_1 : α) ↦ Prop) r) m n
⊢ ReflTransGen r n m

Tactic:
rw [← reflTransGen_swap]

Premises used: Relation.reflTransGen_swap
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap (φ := fun (a a_1 : α) ↦ Prop) r) m n

Tactic:
reflTransGen_of_succ_of_le (swap r) h hmn

Premises used: Function.swap, reflTransGen_of_succ_of_le
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap (φ := fun (a a_1 : α) ↦ Prop) r) m n

Tactic:
exact reflTransGen_of_succ_of_le (swap r) h hmn

Premises used: Function.swap, reflTransGen_of_succ_of_le
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico n m, r i (succ i)
hnm : n < m
⊢ TransGen r n m

Tactic:
(reflTransGen_iff_eq_or_transGen.mp <| reflTransGen_of_succ_of_le r h hnm.le).resolve_left
    hnm.ne'

Premises used: LT.lt.le, Or.resolve_left, reflTransGen_of_succ_of_le, LT.lt.ne', Relation.reflTransGen_iff_eq_or_transGen, Iff.mp
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m < n
⊢ TransGen r n m

Tactic:
(reflTransGen_iff_eq_or_transGen.mp <| reflTransGen_of_succ_of_ge r h hmn.le).resolve_left
    hmn.ne

Premises used: reflTransGen_of_succ_of_ge, LT.lt.le, Or.resolve_left, Relation.reflTransGen_iff_eq_or_transGen, Iff.mp, LT.lt.ne
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
⊢ ReflTransGen r n m

Tactic:
(le_total n m).elim (reflTransGen_of_succ_of_le r h1) <| reflTransGen_of_succ_of_ge r h2

Premises used: reflTransGen_of_succ_of_ge, le_total, reflTransGen_of_succ_of_le, Or.elim
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hnm : n ≠ m
⊢ TransGen r n m

Tactic:
(reflTransGen_iff_eq_or_transGen.mp (reflTransGen_of_succ r h1 h2)).resolve_left hnm.symm

Premises used: Or.resolve_left, Ne.symm, Relation.reflTransGen_iff_eq_or_transGen, Iff.mp, reflTransGen_of_succ
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
inl : ∀ (h1 : ∀ i ∈ Ico m m, r i (succ i)) (h2 : ∀ i ∈ Ico m m, r (succ i) i), TransGen r m m
inr : ∀ (hmn : m ≠ n), TransGen r n m
⊢ TransGen r n m

Tactic:
rcases eq_or_ne m n with (rfl | hmn)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico m m, r i (succ i)
h2 : ∀ i ∈ Ico m m, r (succ i) i
⊢ TransGen r m m

Tactic:
TransGen.single (refl m)

Premises used: Relation.TransGen.single, refl
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico m m, r i (succ i)
h2 : ∀ i ∈ Ico m m, r (succ i) i
⊢ TransGen r m m

Tactic:
exact TransGen.single (refl m)

Premises used: Relation.TransGen.single, refl
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m

Tactic:
transGen_of_succ_of_ne r h1 h2 hmn.symm

Premises used: transGen_of_succ_of_ne, Ne.symm
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m

Tactic:
exact transGen_of_succ_of_ne r h1 h2 hmn.symm

Premises used: transGen_of_succ_of_ne, Ne.symm
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ioc m n, r i (pred i)
hnm : m ≤ n
⊢ ReflTransGen r n m

Tactic:
reflTransGen_of_succ_of_le (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hnm

Premises used: reflTransGen_of_succ_of_le, And.right, And.left, And.intro, OrderDual
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ioc n m, r (pred i) i
hmn : n ≤ m
⊢ ReflTransGen r n m

Tactic:
reflTransGen_of_succ_of_ge (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hmn

Premises used: reflTransGen_of_succ_of_ge, And.right, And.left, And.intro, OrderDual