awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
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
⊢ pred^[n + 1] (succ^[n + 1] i) = i
have succ : ¬IsMax (succ^[n + 1 - 1] i)
Tactic: rw [pred_succ_iterate_of_not_isMax]
-- 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 ι
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
⊢ ¬IsMax (succ^[n + 1 - 1] i)
have succ : ¬IsMax (succ^[n] i)
Tactic: rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
-- 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 ι
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
⊢ ¬IsMax (succ^[n] i)
have succ : succ^[n] i < succ^[n.succ] i
Tactic: suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
-- 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 ι
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^[n.succ] i
have succ : succ^[n] i ≤ succ^[n.succ] i
Tactic: refine lt_of_le_of_ne ?_ ?_
-- 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 ι
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^[n.succ] i
⊢ Order.succ^[n] i < Order.succ^[n.succ] i
have succ₁ : Order.succ^[n] i ≠ Order.succ^[n.succ] i
Tactic: refine lt_of_le_of_ne ?_ ?_
-- 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 ι
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^[n.succ] i
have succ : succ^[n] i ≤ succ (succ^[n] i)
Tactic: rw [Function.iterate_succ_apply']
-- 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 ι
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^[n.succ] i
have succ : succ^[n] i ≠ j
Tactic: rw [hn_eq]
-- 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 ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ pred^[n] (succ^[n] i) = i
have zero : ∀ (hn_eq : succ^[0] i = j) (hn_lt_ne : ∀ m < 0, succ^[m] i ≠ j), pred^[0] (succ^[0] 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)
Cleared hypotheses: n, hn_eq, hn_lt_ne
-- 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 ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
zero : ∀ (hn_eq : succ^[0] i = j) (hn_lt_ne : ∀ m < 0, succ^[m] i ≠ j), pred^[0] (succ^[0] i) = i
⊢ pred^[n] (succ^[n] i) = i
have succ : ∀ (n : ℕ) (hn_eq : succ^[n + 1] i = j) (hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j), pred^[n + 1] (succ^[n + 1] 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)
Cleared hypotheses: n, hn_eq, hn_lt_ne
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
i : ι
⊢ i ≤ succFn i
have rw : ∀ x ∈ Set.Ioi i, i ≤ x
Tactic: rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k
have h₁ : (∀ 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 ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have refine : ∀ (x : ι) (hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1), ∀ x_1 ∈ Set.Ioi i, x ≤ x_1
Tactic: refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ x ≤ y
have inl : ∀ (h_le : y ≤ j), x ≤ y
Tactic: rcases le_or_gt y j with h_le | h_lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ x ≤ y
have inr : ∀ (h_lt : j < y), x ≤ y
Tactic: rcases le_or_gt y j with h_le | h_lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
⊢ IsMax i
have refine : ∀ (j : ι), i ≤ j → ∀ (hij_lt : i < j), False
Tactic: refine fun j _ ↦ not_lt.mp fun hij_lt ↦ ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
h : i ≤ j
hij_lt : i < j
⊢ False
have h_succFn_eq : succFn i = i
Tactic: have h_succFn_eq : succFn i = i := le_antisymm hi (le_succFn i)
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have rw : IsGLB (Set.Ioc i j) i
Tactic: rw [Finset.coe_Ioc]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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.Ioc i j) i
have h : IsGLB (Set.Ioi i) (succFn i)
Tactic: have h := succFn_spec i
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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.Ioc i j) i
have h₁ : IsGLB (Set.Ioi i) i
Tactic: rw [h_succFn_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ False
have h_glb : 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
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have refine : (Finset.Ioc i j).Nonempty
Tactic: refine Finset.isGLB_mem _ h_glb ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ False
have hi_mem : 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⟩⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ False
have hi_mem₁ : i < i ∧ i ≤ j
Tactic: rw [Finset.mem_Ioc] at hi_mem
Cleared hypotheses: hi_mem
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
i j : ι
hij : i < j
⊢ succFn i ≤ j
have h : IsGLB (Set.Ioi i) (succFn i)
Tactic: have h := succFn_spec i
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ succFn i ≤ j
have h₁ : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
Tactic: rw [IsGLB, IsGreatest, mem_lowerBounds] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i
have hij₁ : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
Tactic: rw [lt_isGLB_iff (succFn_spec i)] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
⊢ j ≤ i
have obtain : ∀ (k : ι) (hk_lb : k ∈ lowerBounds (Set.Ioi i)) (hk : j < k), j ≤ i
Tactic: obtain ⟨k, hk_lb, hk⟩ := hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ j ≤ i
have hk_lb₁ : ∀ x ∈ Set.Ioi i, k ≤ x
Tactic: rw [mem_lowerBounds] at hk_lb
Cleared hypotheses: hk_lb, hk
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i ≤ j
⊢ ∃ (n : ℕ), succ^[n] i = j
have hij₁ : i < j ∨ i = j
Tactic: rw [le_iff_lt_or_eq] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ (n : ℕ), succ^[n] i = j
have inl : ∀ (hij : i < j), ∃ (n : ℕ), succ^[n] i = j
Tactic: rcases hij with hij | hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ ∃ (n : ℕ), succ^[n] i = j
have inr : ∀ (hij : i = j), ∃ (n : ℕ), succ^[n] i = j
Tactic: rcases hij with hij | hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i = j
⊢ ∃ (n : ℕ), succ^[n] i = j
have inr : succ^[0] i = j
Tactic: refine ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
⊢ ∃ (n : ℕ), succ^[n] i = j
have inl : ∀ (h : ∀ (n : ℕ), succ^[n] i ≠ j), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have succ : succ^[n + 1] i ≤ j
Tactic: refine lt_of_le_of_ne ?_ (h _)
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have succ : succ (succ^[n] i) ≤ j
Tactic: rw [Function.iterate_succ', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have zero : succ^[0] 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
zero : succ^[0] i < j
⊢ succ^[n] i < j
have succ : ∀ (n : ℕ) (hn : succ^[n] i < j), succ^[n + 1] 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
⊢ False
have h_lt : ∀ (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
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ False
have h_mem : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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 ∧ succ^[n] i = succ^[m] i
have obtain : ∀ (n m : ℕ) (hnm_ne : n ≠ m) (hfnm : f n = f m), ∃ (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
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
have hnm_eq : 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
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
have inl : ∀ (h_le : n ≤ m), ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
Tactic: rcases le_total n m with h_le | h_le
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
have inr : ∀ (h_le : m ≤ n), ∃ (n : ℕ) (m : ℕ), n < m ∧ succ^[n] i = succ^[m] i
Tactic: rcases le_total n m with h_le | h_le
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ False
have inl : ∀ (n m : ℕ) (hnm : n < m) (h_eq : succ^[n] i = succ^[m] i), 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⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
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
⊢ False
have h_max : IsMax (succ^[n] i)
Tactic: have h_max : IsMax (succ^[n] i) := isMax_iterate_succ_of_eq_of_ne h_eq hnm.ne
-- 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 : ι
⊢ toZ i0 i0 = 0
have rw : Eq (α := ℤ) (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) sorry) : ℤ) 0
Tactic: rw [toZ_of_ge le_rfl]
-- 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 : ι
⊢ Eq (α := ℤ) (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯) : ℤ) 0
have norm_cast : Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) sorry = 0
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 : ι
⊢ Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯ = 0
have rw : Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) sorry ≤ 0
Tactic: rw [← nonpos_iff_eq_zero]
-- 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 : ι
⊢ Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i0) ⋯ ≤ 0
have hn : succ^[0] i0 = i0
Tactic: apply Nat.find_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 : ι
⊢ succ^[0] i0 = i0
have hn : id i0 = i0
Tactic: rw [Function.iterate_zero, id]
-- 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 : ι
hn : id i0 = i0
⊢ succ^[0] i0 = i0
have hn₁ : i0 = i0
Tactic: rw [Function.iterate_zero, id]
-- 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 i : ι
hi : i0 ≤ i
⊢ succ^[(toZ i0 i).toNat] i0 = i
have rw : succ^[Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) sorry] i0 = i
Tactic: rw [toZ_of_ge hi, Int.toNat_natCast]
-- 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 i : ι
hi : i < i0
⊢ pred^[(-toZ i0 i).toNat] i0 = i
have rw : pred^[Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) sorry] i0 = i
Tactic: rw [toZ_of_lt hi, neg_neg, Int.toNat_natCast]
-- 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 i : ι
hi : i0 ≤ i
⊢ 0 ≤ toZ i0 i
have rw : LE.le (α := ℤ) 0 (↑(Nat.find (p := fun (n : ℕ) ↦ succ^[n] i0 = i) sorry) : ℤ)
Tactic: rw [toZ_of_ge 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 i : ι
hi : i < i0
⊢ toZ i0 i < 0
have refine_1 : toZ i0 i ≤ 0
Tactic: refine lt_of_le_of_ne ?_ ?_
-- 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 i : ι
hi : i < i0
refine_1 : toZ i0 i ≤ 0
⊢ toZ i0 i < 0
have refine_2 : toZ i0 i ≠ 0
Tactic: refine lt_of_le_of_ne ?_ ?_
-- 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 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0
have refine_1 : LE.le (α := ℤ) (-(↑(Nat.find (p := fun (n : ℕ) ↦ pred^[n] i0 = i) sorry) : ℤ)) 0
Tactic: rw [toZ_of_lt hi]
-- 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
⊢ False
have h_eq : pred^[(-toZ i0 i).toNat] i0 = i
Tactic: have h_eq := iterate_pred_toZ i hi