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 ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j
succ : Order.succ^[n] i ≤ Order.succ (Order.succ^[n] i)
⊢ Order.succ^[n] i ≤ Order.succ^[n.succ] i

Tactic:
rw [Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≤ succ (succ^[n] i)

Tactic:
le_succ _

Premises used: Order.le_succ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≤ succ (succ^[n] i)

Tactic:
exact le_succ _

Premises used: Order.le_succ
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j
succ : Order.succ^[n] i ≠ j
⊢ Order.succ^[n] i ≠ Order.succ^[n.succ] i

Tactic:
rw [hn_eq]
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≠ j

Tactic:
hn_lt_ne _ (Nat.lt_succ_self n)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≠ j

Tactic:
exact hn_lt_ne _ (Nat.lt_succ_self n)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n] i = j
hn_lt_ne : ∀ m < n, Order.succ^[m] i ≠ j
zero : ∀ (hn_eq : Order.succ^[0] i = j) (hn_lt_ne : ∀ m < 0, Order.succ^[m] i ≠ j), pred^[0] (Order.succ^[0] i) = i
succ :
  ∀ (n : ℕ) (hn_eq : Order.succ^[n + 1] i = j) (hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j),
    pred^[n + 1] (Order.succ^[n + 1] i) = i
⊢ pred^[n] (Order.succ^[n] i) = i

Tactic:
cases n with
    | zero => simp only [Function.iterate_zero, id]
    | succ n =>
      rw [pred_succ_iterate_of_not_isMax]
      rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
      suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
      refine lt_of_le_of_ne ?_ ?_
      · rw [Function.iterate_succ_apply']
        exact le_succ _
      · rw [hn_eq]
        exact hn_lt_ne _ (Nat.lt_succ_self n)

Premises used: Function.iterate_succ_apply', Order.succ, Function.iterate_zero, id, tsub_zero, Order.le_succ, Order.pred_succ_iterate_of_not_isMax, Nat.succ_sub_succ_eq_sub, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsPredArchimedean ι
⊢ IsSuccArchimedean ι

Tactic:
inferInstanceAs (IsSuccArchimedean ιᵒᵈᵒᵈ)

Premises used: _private.0.LinearOrder.isSuccArchimedean_of_isPredArchimedean._proof_1
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i : ι
⊢ IsGLB (Set.Ioi i) (succFn i)

Tactic:
(exists_glb_Ioi i).choose_spec

Premises used: Exists.choose_spec, LinearLocallyFiniteOrder.succFn, exists_glb_Ioi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i : ι
rw : ∀ x ∈ Set.Ioi i, i ≤ x
⊢ i ≤ succFn i

Tactic:
rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]

Premises used: mem_lowerBounds, LinearLocallyFiniteOrder.succFn_spec, le_isGLB_iff
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i : ι
⊢ ∀ x ∈ Set.Ioi i, i ≤ x

Tactic:
fun x hx ↦ le_of_lt hx

Premises used: le_of_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i : ι
⊢ ∀ x ∈ Set.Ioi i, i ≤ x

Tactic:
exact fun x hx ↦ le_of_lt hx

Premises used: le_of_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k

Tactic:
simp_rw [IsGLB, IsGreatest, mem_upperBounds, mem_lowerBounds] at h ⊢

Premises used: mem_lowerBounds, IsGreatest, IsGLB, mem_upperBounds
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
⊢ (∀ x ∈ Set.Ioc i j, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioc i j, x ≤ x_1) → x ≤ k

Tactic:
⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
refine : ∀ (x : ι) (hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1), ∀ x_1 ∈ Set.Ioi i, x ≤ x_1
⊢ (∀ x ∈ Set.Ioc i j, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioc i j, x ≤ x_1) → x ≤ k

Tactic:
refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
inl : ∀ (h_le : y ≤ j), x ≤ y
inr : ∀ (h_lt : j < y), x ≤ y
⊢ x ≤ y

Tactic:
rcases le_or_gt y j with h_le | h_lt

Premises used: le_or_gt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_le : y ≤ j
⊢ x ≤ y

Tactic:
hx y ⟨hy, h_le⟩

Premises used: And.intro
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_le : y ≤ j
⊢ x ≤ y

Tactic:
exact hx y ⟨hy, h_le⟩

Premises used: And.intro
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y

Tactic:
le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le

Premises used: le_rfl, LT.lt.le, And.intro, le_trans
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y

Tactic:
exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le

Premises used: le_rfl, LT.lt.le, And.intro, le_trans
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
⊢ IsMax i

Tactic:
fun j _ ↦ not_lt.mp fun hij_lt ↦ ?_

Premises used: not_lt, Iff.mp, IsMax
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
refine : ∀ (j : ι), i ≤ j → ∀ (hij_lt : i < j), False
⊢ IsMax i

Tactic:
refine fun j _ ↦ not_lt.mp fun hij_lt ↦ ?_

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
⊢ succFn i = i

Tactic:
have h_succFn_eq : succFn i = i := le_antisymm hi (le_succFn i)
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
rw : IsGLB (Set.Ioc i j) i
⊢ IsGLB (↑(Finset.Ioc i j) : Set ι) i

Tactic:
rw [Finset.coe_Ioc]

Premises used: Finset.coe_Ioc
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioi i) (succFn i)

Tactic:
have h := succFn_spec i
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h_1 : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) (succFn i)
⊢ IsGLB (Set.Ioi i) i

Tactic:
rw [h_succFn_eq] at h
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h_1 : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
isGLB_Ioc_of_isGLB_Ioi hij_lt h

Premises used: LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h_1 : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
exact isGLB_Ioc_of_isGLB_Ioi hij_lt h

Premises used: LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (↑(Finset.Ioc i j) : Set ι) i

Tactic:
have h_glb : IsGLB (Finset.Ioc i j : Set ι) i := by
    rw [Finset.coe_Ioc]
    have h := succFn_spec i
    rw [h_succFn_eq] at h
    exact isGLB_Ioc_of_isGLB_Ioi hij_lt h
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
⊢ i ∈ Finset.Ioc i j

Tactic:
Finset.isGLB_mem _ h_glb ?_

Premises used: Finset.isGLB_mem
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
refine : (Finset.Ioc i j).Nonempty
⊢ i ∈ Finset.Ioc i j

Tactic:
refine Finset.isGLB_mem _ h_glb ?_

Premises used: Finset.isGLB_mem
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
⊢ (Finset.Ioc i j).Nonempty

Tactic:
⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩

Premises used: Iff.mpr, le_rfl, And.intro, Exists.intro, Finset.Nonempty, Finset.mem_Ioc
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
⊢ (Finset.Ioc i j).Nonempty

Tactic:
exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
⊢ i ∈ Finset.Ioc i j

Tactic:
have hi_mem : i ∈ Finset.Ioc i j := by
    refine Finset.isGLB_mem _ h_glb ?_
    exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
hi_mem : i ∈ Finset.Ioc i j
⊢ i < i ∧ i ≤ j

Tactic:
rw [Finset.mem_Ioc] at hi_mem

Premises used: Finset.mem_Ioc
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
hi_mem : i < i ∧ i ≤ j
⊢ False

Tactic:
lt_irrefl i hi_mem.1

Premises used: lt_irrefl, And.left
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j) : Set ι) i
hi_mem : i < i ∧ i ≤ j
⊢ False

Tactic:
exact lt_irrefl i hi_mem.1

Premises used: lt_irrefl, And.left
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j : ι
hij : i < j
⊢ IsGLB (Set.Ioi i) (succFn i)

Tactic:
have h := succFn_spec i
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))

Tactic:
rw [IsGLB, IsGreatest, mem_lowerBounds] at h

Premises used: mem_lowerBounds, IsGreatest, IsGLB
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j : ι
hij : i < j
h : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j

Tactic:
h.1 j hij

Premises used: And.left
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
i j : ι
hij : i < j
h : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j

Tactic:
exact h.1 j hij

Premises used: And.left
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ ∃ c ∈ lowerBounds (Set.Ioi i), j < c

Tactic:
rw [lt_isGLB_iff (succFn_spec i)] at hij

Premises used: LinearLocallyFiniteOrder.succFn_spec, lt_isGLB_iff
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
obtain : ∀ (k : ι) (hk_lb : k ∈ lowerBounds (Set.Ioi i)) (hk : j < k), j ≤ i
⊢ j ≤ i

Tactic:
obtain ⟨k, hk_lb, hk⟩ := hij
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ ∀ x ∈ Set.Ioi i, k ≤ x

Tactic:
rw [mem_lowerBounds] at hk_lb

Premises used: mem_lowerBounds
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
hk_lb₁ : ∀ x ∈ Set.Ioi i, k ≤ x
⊢ j < k

Tactic:
rw [mem_lowerBounds] at hk_lb

Premises used: mem_lowerBounds
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
j i k : ι
hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x
hk : j < k
⊢ j ≤ i

Tactic:
not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)

Premises used: not_le, Iff.mpr, not_lt, Iff.mp
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
j i k : ι
hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x
hk : j < k
⊢ j ≤ i

Tactic:
exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)

Premises used: not_le, Iff.mpr, not_lt, Iff.mp
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i ≤ j
⊢ i < j ∨ i = j

Tactic:
rw [le_iff_lt_or_eq] at hij

Premises used: le_iff_lt_or_eq
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
inl : ∀ (hij : i < j), ∃ (n : ℕ), succ^[n] i = j
inr : ∀ (hij : i = j), ∃ (n : ℕ), succ^[n] i = j
⊢ ∃ (n : ℕ), succ^[n] i = j

Tactic:
rcases hij with hij | hij
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i = j
⊢ ∃ (n : ℕ), succ^[n] i = j

Tactic:
⟨0, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i = j
inr : succ^[0] i = j
⊢ ∃ (n : ℕ), succ^[n] i = j

Tactic:
refine ⟨0, ?_⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i = j
⊢ succ^[0] i = j

Tactic:
simpa only [Function.iterate_zero, id] using hij

Premises used: Function.iterate_zero, id
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
inl : ∀ (h : ∀ (n : ℕ), succ^[n] i ≠ j), False
⊢ ∃ (n : ℕ), succ^[n] i = j

Tactic:
by_contra! h
-- 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
⊢ succ^[0] i < j

Tactic:
simpa only [Function.iterate_zero, id] using hij

Premises used: Function.iterate_zero, id
-- 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
n : ℕ
hn : succ^[n] i < j
⊢ succ^[n + 1] i < j

Tactic:
lt_of_le_of_ne ?_ (h _)

Premises used: 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 : ℕ), Order.succ^[n] i ≠ j
n : ℕ
hn : Order.succ^[n] i < j
succ : Order.succ^[n + 1] i ≤ j
⊢ Order.succ^[n + 1] i < j

Tactic:
refine lt_of_le_of_ne ?_ (h _)

Premises used: 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 : ℕ), Order.succ^[n] i ≠ j
n : ℕ
hn : Order.succ^[n] i < j
succ : Order.succ (Order.succ^[n] i) ≤ j
⊢ Order.succ^[n + 1] i ≤ j

Tactic:
rw [Function.iterate_succ', Function.comp_apply]

Premises used: Function.iterate_succ', Function.comp_apply
-- 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
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j

Tactic:
succ_le_of_lt hn

Premises used: Order.succ_le_of_lt
-- 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
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j

Tactic:
exact succ_le_of_lt hn

Premises used: Order.succ_le_of_lt
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), Order.succ^[n] i ≠ j
n : ℕ
zero : Order.succ^[0] i < j
succ : ∀ (n : ℕ) (hn : Order.succ^[n] i < j), Order.succ^[n + 1] i < j
⊢ Order.succ^[n] i < j

Tactic:
induction n with
      | zero => simpa only [Function.iterate_zero, id] using hij
      | succ n hn =>
        refine lt_of_le_of_ne ?_ (h _)
        rw [Function.iterate_succ', Function.comp_apply]
        exact succ_le_of_lt hn

Premises used: Order.succ, Function.iterate_zero, Function.iterate_succ', id, Function.comp_apply, 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
⊢ ∀ (n : ℕ), succ^[n] i < j

Tactic:
have h_lt : ∀ n, succ^[n] i < j := fun n ↦ by
      induction n with
      | zero => simpa only [Function.iterate_zero, id] using hij
      | succ n hn =>
        refine lt_of_le_of_ne ?_ (h _)
        rw [Function.iterate_succ', Function.comp_apply]
        exact succ_le_of_lt hn
-- 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
⊢ ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j

Tactic:
have h_mem : ∀ n, succ^[n] i ∈ Finset.Icc i j :=
      fun n ↦ Finset.mem_Icc.mpr ⟨le_succ_iterate n i, (h_lt n).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
f : ℕ → ↥(Finset.Icc i j) := fun (n : ℕ) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Finset.Icc i j) (succ^[n] i) ⋯
⊢ ∃ (n : ℕ) (m : ℕ), n ≠ m ∧ f n = f m

Tactic:
Finite.exists_ne_map_eq_of_infinite f

Premises used: Finite.exists_ne_map_eq_of_infinite
-- 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) ⋯
obtain : ∀ (n m : ℕ) (hnm_ne : n ≠ m) (hfnm : f n = f m), ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i

Tactic:
obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m :=
        Finite.exists_ne_map_eq_of_infinite f

Premises used: Finite.exists_ne_map_eq_of_infinite
-- 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
⊢ succ^[n] i = succ^[m] i

Tactic:
simpa only [f, Subtype.mk_eq_mk] using hfnm

Premises used: Subtype.mk_eq_mk
-- 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
⊢ succ^[n] i = succ^[m] i

Tactic:
have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [f, Subtype.mk_eq_mk] using hfnm