awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : Ioo a b = ∅
refine_1 : ∀ (h : succ a < b), (Ioo a b).Nonempty
⊢ b ≤ succ a

Tactic:
contrapose! h
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : succ a < b
⊢ (Ioo a b).Nonempty

Tactic:
⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩

Premises used: Iff.mpr, Order.succ, not_isMax, Order.lt_succ_iff_not_isMax, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : succ a < b
⊢ (Ioo a b).Nonempty

Tactic:
exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
refine_2 : ∀ (x : α), x ∈ Ioo a b ↔ Membership.mem (γ := Set α) ∅ x
⊢ Ioo a b = ∅

Tactic:
ext x
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
x : α
this : a < x → b ≤ x
⊢ x ∈ Ioo a b ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simpa
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
x : α
refine_2 : a < x → b ≤ x
⊢ x ∈ Ioo a b ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
suffices a < x → b ≤ x by simpa
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
x : α
⊢ a < x → b ≤ x

Tactic:
fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

Premises used: lt_of_le_of_lt, Order.succ_strictMono, Order.le_of_lt_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
x : α
⊢ a < x → b ≤ x

Tactic:
exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

Premises used: lt_of_le_of_lt, Order.succ_strictMono, Order.le_of_lt_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
inst_3 : NoMaxOrder α
rw : a ≤ ⊥ ↔ a = ⊥
rw₁ rw₂ : a = ⊥ ↔ a = ⊥
⊢ a < succ ⊥ ↔ a = ⊥

Tactic:
rw [lt_succ_iff, le_bot_iff]

Premises used: le_bot_iff, Order.lt_succ_iff
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
rw : a = succ ⊥ ∨ a ≤ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
rw₁ : a = succ ⊥ ∨ a = ⊥ ↔ a = ⊥ ∨ a = succ ⊥
rw₂ rw₃ : a = ⊥ ∨ a = succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Tactic:
rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]

Premises used: le_bot_iff, or_comm, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
succ : ∀ (a : α), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
⊢ h₀ = h₁

Tactic:
ext a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
pos : ∀ (ha : IsMax a), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
neg : ∀ (ha : ¬IsMax a), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a

Tactic:
by_cases ha : IsMax a

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : IsMax a
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a

Tactic:
(@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm

Premises used: Order.succ, Eq.symm, IsMax.succ_eq, Eq.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : IsMax a
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a

Tactic:
exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm

Premises used: Eq.symm, IsMax.succ_eq, Eq.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a

Tactic:
@CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)

Premises used: Order.succ, CovBy.succ_eq, Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a

Tactic:
exact @CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)

Premises used: CovBy.succ_eq, Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
apply : sInf (Ioi a) ≤ succ a
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_sInf fun b => succ_le_of_lt).antisymm

Premises used: LE.le.antisymm, le_sInf
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
inl : LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) (succ ⊤)
inr : ∀ (ha : a ≠ ⊤), sInf (Ioi a) ≤ succ a
⊢ sInf (Ioi a) ≤ succ a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
inl : LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) ⊤
⊢ LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) (succ ⊤)

Tactic:
rw [succ_top]

Premises used: Order.succ_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
⊢ LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
⊢ LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ sInf (Ioi a) ≤ succ a

Tactic:
sInf_le (lt_succ_iff_ne_top.2 ha)

Premises used: Iff.mpr, sInf_le, Order.lt_succ_iff_ne_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ sInf (Ioi a) ≤ succ a

Tactic:
exact sInf_le (lt_succ_iff_ne_top.2 ha)

Premises used: Iff.mpr, sInf_le, Order.lt_succ_iff_ne_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
rw : sInf (Ioi a) = ⨅ (b : α), ⨅ (_ : b > a), b
rw₁ : sInf (Ioi a) = ⨅ (x : { b : α // b > a }), (↑x : α)
rw₂ : sInf (Ioi a) = sInf (range fun (x : { b : α // b > a }) ↦ (↑x : α))
rw₃ : sInf (Ioi a) = sInf {x : α | x > a}
rw₄ rw₅ : Eq.{u_1 + 1} (α := α) (sInf {x : α | a < x}) (sInf {x : α | x > a})
⊢ succ a = ⨅ (b : α), ⨅ (_ : b > a), b

Tactic:
rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]

Premises used: Set.Ioi, iInf, iInf_subtype', Subtype.range_coe_subtype, Order.succ_eq_sInf
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
apply : sInf (Ioi a) ≤ succ a
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm

Premises used: le_csInf, LE.le.antisymm, Order.succ_le_of_lt, Set.nonempty_Ioi
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a

Tactic:
csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

Premises used: le_of_lt, Order.lt_succ, Exists.intro, csInf_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a

Tactic:
exact csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

Premises used: le_of_lt, Order.lt_succ, Exists.intro, csInf_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : PredOrder α
a b : α
ha : ¬IsMin a
⊢ a ≤ b → pred a < b

Tactic:
(pred_lt_of_not_isMin ha).trans_le

Premises used: LT.lt.trans_le, Order.pred_lt_of_not_isMin
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : PredOrder α
a : α
n m : ℕ
h_eq : pred^[n] a = pred^[m] a
h_lt : n < m
⊢ IsMin (pred^[n] a)

Tactic:
@isMax_iterate_succ_of_eq_of_lt αᵒᵈ _ _ _ _ _ h_eq h_lt

Premises used: Order.isMax_iterate_succ_of_eq_of_lt, Order.pred, OrderDual, IsMin
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : PredOrder α
a : α
n m : ℕ
h_eq : pred^[n] a = pred^[m] a
h_ne : n ≠ m
⊢ IsMin (pred^[n] a)

Tactic:
@isMax_iterate_succ_of_eq_of_ne αᵒᵈ _ _ _ _ _ h_eq h_ne

Premises used: Order.isMax_iterate_succ_of_eq_of_ne, Order.pred, OrderDual, IsMin
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
a : α
⊢ a ≤ succ (pred a)

Tactic:
(pred_wcovBy _).le_succ

Premises used: WCovBy.le_succ, Order.pred_wcovBy
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
⊢ GaloisConnection.{u_1, u_1} (α := α) pred succ

Tactic:
fun _ _ ↦ pred_le_iff_le_succ

Premises used: Order.pred_le_iff_le_succ, GaloisConnection
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
a : α
h : ¬IsMin a
⊢ succ (pred a) = a

Tactic:
CovBy.succ_eq (pred_covBy_of_not_isMin h)

Premises used: Order.pred_covBy_of_not_isMin, CovBy.succ_eq
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a : α
⊢ succ (pred a) = a

Tactic:
CovBy.succ_eq (pred_covBy _)

Premises used: CovBy.succ_eq, Order.pred_covBy
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
hin : ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)
⊢ pred^[0] (succ^[0] i) = i

Tactic:
simp only [Function.iterate_zero, id]

Premises used: Function.iterate_zero, id
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n + 1 - 1] i)
⊢ ¬IsMax (succ^[n] i)

Tactic:
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin

Premises used: Nat.sub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (Order.succ^[n - 1] i)), pred^[n] (Order.succ^[n] i) = i
hin : ¬IsMax (Order.succ^[n] i)
zero :
  ∀ (hn : ∀ (hin : ¬IsMax (Order.succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (Order.succ^[0] i) = i)
    (hin : ¬IsMax (Order.succ^[0] i)), ¬IsMax (Order.succ^[HSub.hSub (α := ℕ) 0 1] i)
succ :
  ∀ (n : ℕ) (hn : ∀ (hin : ¬IsMax (Order.succ^[n + 1 - 1] i)), pred^[n + 1] (Order.succ^[n + 1] i) = i)
    (hin : ¬IsMax (Order.succ^[n + 1] i)), ¬IsMax (Order.succ^[n + 1 - 1] i)
⊢ ¬IsMax (Order.succ^[n - 1] i)

Tactic:
rcases n with - | n
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
hn : ∀ (hin : ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (succ^[0] i) = i
hin : ¬IsMax (succ^[0] i)
⊢ ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)

Tactic:
simpa using hin
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (Order.succ^[n + 1 - 1] i)), pred^[n + 1] (Order.succ^[n + 1] i) = i
hin : ¬IsMax (Order.succ^[n + 1] i)
succ :
  ∀ (hn : ∀ (hin : ¬IsMax (Order.succ^[n] i)), pred^[n + 1] (Order.succ^[n + 1] i) = i)
    (hin : ¬IsMax (Order.succ^[n + 1] i)), ¬IsMax (Order.succ^[n] i)
⊢ ¬IsMax (Order.succ^[n + 1 - 1] i)

Tactic:
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢

Premises used: Nat.sub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
rw : succ^[n] i ≤ (succ ∘ succ^[n]) i
⊢ succ^[n] i ≤ succ^[n.succ] i

Tactic:
rw [Function.iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ (succ ∘ succ^[n]) i

Tactic:
le_succ _

Premises used: Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ (succ ∘ succ^[n]) i

Tactic:
exact le_succ _

Premises used: Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ succ^[n.succ] i

Tactic:
have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
⊢ ¬IsMax (succ^[n] i)

Tactic:
fun h_max => hin fun j hj => ?_

Premises used: Not
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (Order.succ^[n] i)), pred^[n + 1] (Order.succ^[n + 1] i) = i
hin : ¬IsMax (Order.succ^[n + 1] i)
h_sub_le : Order.succ^[n] i ≤ Order.succ^[n.succ] i
succ : ∀ (h_max : IsMax (Order.succ^[n] i)) (j : α) (hj : Order.succ^[n + 1] i ≤ j), j ≤ Order.succ^[n + 1] i
⊢ ¬IsMax (Order.succ^[n] i)

Tactic:
refine fun h_max => hin fun j hj => ?_
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
⊢ j ≤ succ^[n] i

Tactic:
have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
hj_le : j ≤ succ^[n] i
⊢ j ≤ succ^[n + 1] i

Tactic:
hj_le.trans h_sub_le

Premises used: LE.le.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
hj_le : j ≤ succ^[n] i
⊢ j ≤ succ^[n + 1] i

Tactic:
exact hj_le.trans h_sub_le

Premises used: LE.le.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ ¬IsMax (succ^[n - 1] i)

Tactic:
have h_not_max : ¬IsMax (succ^[n - 1] i) := by
      rcases n with - | n
      · simpa using hin
      rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
      have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
      refine fun h_max => hin fun j hj => ?_
      have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
      exact hj_le.trans h_sub_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (Order.succ^[n - 1] i)), pred^[n] (Order.succ^[n] i) = i
hin : ¬IsMax (Order.succ^[n] i)
h_not_max : ¬IsMax (Order.succ^[n - 1] i)
succ : (pred^[n] ∘ pred) ((Order.succ ∘ Order.succ^[n]) i) = i
⊢ pred^[n + 1] (Order.succ^[n + 1] i) = i

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

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (Order.succ^[n - 1] i)), pred^[n] (Order.succ^[n] i) = i
hin : ¬IsMax (Order.succ^[n] i)
h_not_max : ¬IsMax (Order.succ^[n - 1] i)
succ : pred^[n] (pred (Order.succ (Order.succ^[n] i))) = i
⊢ (pred^[n] ∘ pred) ((Order.succ ∘ Order.succ^[n]) i) = i

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (Order.succ^[n - 1] i)), pred^[n] (Order.succ^[n] i) = i
hin : ¬IsMax (Order.succ^[n] i)
h_not_max : ¬IsMax (Order.succ^[n - 1] i)
succ : pred^[n] (Order.succ^[n] i) = i
⊢ pred^[n] (pred (Order.succ (Order.succ^[n] i))) = i

Tactic:
rw [pred_succ_of_not_isMax hin]

Premises used: Order.pred_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i

Tactic:
hn h_not_max
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i

Tactic:
exact hn h_not_max
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hin : ¬IsMax (Order.succ^[n - 1] i)
zero : ∀ (hin : ¬IsMax (Order.succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (Order.succ^[0] i) = i
succ :
  ∀ (n : ℕ) (hn : ∀ (hin : ¬IsMax (Order.succ^[n - 1] i)), pred^[n] (Order.succ^[n] i) = i)
    (hin : ¬IsMax (Order.succ^[n + 1 - 1] i)), pred^[n + 1] (Order.succ^[n + 1] i) = i
⊢ pred^[n] (Order.succ^[n] i) = i

Tactic:
induction n with
  | zero => simp only [Function.iterate_zero, id]
  | succ n hn =>
    rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
    have h_not_max : ¬IsMax (succ^[n - 1] i) := by
      rcases n with - | n
      · simpa using hin
      rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
      have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
      refine fun h_max => hin fun j hj => ?_
      have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
      exact hj_le.trans h_sub_le
    rw [Function.iterate_succ, Function.iterate_succ']
    simp only [Function.comp_apply]
    rw [pred_succ_of_not_isMax hin]
    exact hn h_not_max

Premises used: Order.succ, Function.iterate_succ, Function.iterate_zero, Function.iterate_succ', Order.pred_succ_of_not_isMax, id, Nat.sub_zero, Function.comp_apply, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
none :
  LE.le.{u_1} (α := WithTop α) Option.none
    (match (motive := WithTop α → WithTop α) Option.none with
    | Option.none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α))
some :
  ∀ (a : α),
    Option.some a ≤
      match (motive := WithTop α → WithTop α) Option.some a with
      | Option.none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)
⊢ a ≤
    match (motive := WithTop α → WithTop α) a with
    | Option.none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)

Tactic:
obtain - | a := a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
⊢ LE.le.{u_1} (α := WithTop α) none
    (match (motive := WithTop α → WithTop α) none with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α))

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
⊢ LE.le.{u_1} (α := WithTop α) none
    (match (motive := WithTop α → WithTop α) none with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α))

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
pos : succ a = a → Option.some a ≤ ⊤
neg : ¬succ a = a → Option.some a ≤ (↑(succ a) : WithTop α)
⊢ Option.some a ≤ if succ a = a then ⊤ else (↑(succ a) : WithTop α)

Tactic:
split_ifs
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : succ a = a
⊢ Option.some a ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : succ a = a
⊢ Option.some a ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : ¬succ a = a
⊢ Option.some a ≤ (↑(succ a) : WithTop α)

Tactic:
coe_le_coe.2 (le_succ a)

Premises used: Iff.mpr, WithTop.some, Order.le_succ, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : ¬succ a = a
⊢ Option.some a ≤ (↑(succ a) : WithTop α)

Tactic:
exact coe_le_coe.2 (le_succ a)

Premises used: Iff.mpr, Order.le_succ, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
ha :
  (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    a
top :
  ∀
    (ha :
      LE.le.{u_1} (α := WithTop α)
        (match (motive := WithTop α → WithTop α) ⊤ with
          | none => ⊤
          | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α) :
          WithTop α)
        (⊤ : WithTop α)),
    IsMax.{u_1} (α := WithTop α) ⊤
coe :
  ∀ (a : α)
    (ha :
      (match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
        | none => ⊤
        | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
        (↑a : WithTop α)),
    IsMax (↑a : WithTop α)
⊢ IsMax a

Tactic:
cases a