awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ ¬IsPredPrelimit a → ¬IsPredLimit a

Tactic:
mt IsPredLimit.isPredPrelimit

Premises used: Order.IsPredLimit.isPredPrelimit, mt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
ha : ¬IsMin a
⊢ IsSuccLimit a

Tactic:
⟨ha, h⟩

Premises used: Order.IsSuccLimit, And.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : NoMinOrder α
h : IsSuccPrelimit a
⊢ IsSuccLimit a

Tactic:
h.isSuccLimit_of_not_isMin (not_isMin a)

Premises used: not_isMin, Order.IsSuccPrelimit.isSuccLimit_of_not_isMin
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : ¬IsMin a
⊢ IsSuccPrelimit a ↔ IsSuccLimit a

Tactic:
⟨fun ha ↦ ha.isSuccLimit_of_not_isMin h, IsSuccLimit.isSuccPrelimit⟩

Premises used: Order.IsSuccPrelimit.isSuccLimit_of_not_isMin, Iff.intro, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : NoMinOrder α
⊢ IsSuccPrelimit a ↔ IsSuccLimit a

Tactic:
isSuccPrelimit_iff_isSuccLimit_of_not_isMin (not_isMin a)

Premises used: not_isMin, Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsMin a
⊢ ¬IsSuccLimit a

Tactic:
fun ha ↦ ha.not_isMin h

Premises used: Order.IsSuccLimit.not_isMin, Not
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ IsMin a → IsSuccPrelimit a

Tactic:
fun h _ hab =>
  not_isMin_of_lt hab.lt h

Premises used: Order.IsSuccPrelimit, not_isMin_of_lt, CovBy.lt, Not
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccLimit a
⊢ (Iio a).Nonempty

Tactic:
not_isMin_iff.1 h.1

Premises used: not_isMin_iff, Set.Mem, setOf, Set.Nonempty, And.left, Iff.mp, Set.Iio
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
⊢ NoMaxOrder.{u_1} (↑(Iio a) : Type u_1)

Tactic:
⟨fun ⟨b, hb⟩ ↦ ?_⟩

Premises used: Exists, NoMaxOrder.mk, _private.0.Order.IsSuccPrelimit.noMaxOrder_Iio.match_1, LT.lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
refine :
  ∀ (x : (↑(Iio a) : Type u_1)) (b : α) (hb : b ∈ Iio a),
    ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1
⊢ NoMaxOrder.{u_1} (↑(Iio a) : Type u_1)

Tactic:
refine ⟨fun ⟨b, hb⟩ ↦ ?_⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
x : (↑(Iio a) : Type u_1)
b : α
hb : b ∈ Iio a
obtain :
  ∀ (c : α) (hbc : b < c) (hca : c < a),
    ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1
⊢ ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1

Tactic:
obtain ⟨c, hbc, hca⟩ := (not_covBy_iff hb).1 (h b)

Premises used: Iff.mp, not_covBy_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
x : (↑(Iio a) : Type u_1)
b : α
hb : b ∈ Iio a
c : α
hbc : b < c
hca : c < a
⊢ ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1

Tactic:
⟨⟨c, hca⟩, hbc⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
x : (↑(Iio a) : Type u_1)
b : α
hb : b ∈ Iio a
c : α
hbc : b < c
hca : c < a
⊢ ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1

Tactic:
exact ⟨⟨c, hca⟩, hbc⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ IsSuccPrelimit.{u_1} (α := α) ⊥

Tactic:
isMin_bot.isSuccPrelimit

Premises used: IsMin.isSuccPrelimit, isMin_bot
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ ¬IsSuccLimit.{u_1} (α := α) ⊥

Tactic:
isMin_bot.not_isSuccLimit

Premises used: IsMin.not_isSuccLimit, isMin_bot
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : OrderBot α
h : IsSuccLimit a
⊢ ⊥ < a

Tactic:
not_isMin_iff_bot_lt.1 h.not_isMin

Premises used: Order.IsSuccLimit.not_isMin, not_isMin_iff_bot_lt, Iff.mp
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : OrderBot α
h : IsSuccLimit a
⊢ a ≠ ⊥

Tactic:
h.bot_lt.ne'

Premises used: LT.lt.ne', Order.IsSuccLimit.bot_lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : Zero α
inst_2 : IsBotZeroClass α
h : IsSuccLimit a
⊢ 0 < a

Tactic:
let := IsBotZeroClass.toOrderBot α
  h.bot_lt

Premises used: IsBotZeroClass.toOrderBot, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : Zero α
inst_2 : IsBotZeroClass α
h : IsSuccLimit a
⊢ a ≠ 0

Tactic:
h.pos.ne'

Premises used: LT.lt.ne', Order.IsSuccLimit.pos
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
rw : ¬(¬IsMin a ∧ IsSuccPrelimit a) ↔ IsMin a ∨ ¬IsSuccPrelimit a
rw₁ : ¬¬IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
rw₂ rw₃ : IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
rw [IsSuccLimit, not_and_or, not_not]

Premises used: Classical.not_not, Order.IsSuccLimit, not_and_or
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
⊢ ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ ⋖ a

Tactic:
have := ha ⟨b, hs hb.le a.2⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ ⋖ a
rw : ∀ (this : ∃ (c : (↑s : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c ∧ c < a), False
rw₁ : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < a
⊢ False

Tactic:
rw [not_covBy_iff] at this

Premises used: not_covBy_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ∃ (c : (↑s : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c ∧ c < a
obtain : ∀ (c : (↑s : Type u_1)) (hc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c) (hc' : c < a), False
⊢ False

Tactic:
obtain ⟨c, hc, hc'⟩ := this
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
c : (↑s : Type u_1)
hc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c
hc' : c < a
⊢ False

Tactic:
hb.2 hc hc'

Premises used: And.right
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
c : (↑s : Type u_1)
hc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c
hc' : c < a
⊢ False

Tactic:
exact hb.2 hc hc'

Premises used: And.right
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ ⋖ a
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < a

Tactic:
hb.lt

Premises used: CovBy.lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ ⋖ a
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < a

Tactic:
exact hb.lt

Premises used: CovBy.lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
⊢ IsSuccLimit (↑a : α)

Tactic:
⟨?_, ha.isSuccPrelimit.subtypeVal hs⟩

Premises used: Order.IsSuccLimit, Order.IsSuccPrelimit.subtypeVal, And.intro, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
refine : ¬IsMin (↑a : α)
⊢ IsSuccLimit (↑a : α)

Tactic:
refine ⟨?_, ha.isSuccPrelimit.subtypeVal hs⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
⊢ ¬IsMin a

Tactic:
have := ha.1
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
this : ¬IsMin a
rw : ∀ (this : ∃ (b : (↑s : Type u_1)), b < a), ∃ (b : α), b < (↑a : α)
⊢ ¬IsMin (↑a : α)

Tactic:
rw [not_isMin_iff] at ⊢ this

Premises used: not_isMin_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
this : ∃ (b : (↑s : Type u_1)), b < a
obtain : ∀ (b : (↑s : Type u_1)) (hb : b < a), ∃ (b : α), b < (↑a : α)
⊢ ∃ (b : α), b < (↑a : α)

Tactic:
obtain ⟨b, hb⟩ := this
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
b : (↑s : Type u_1)
hb : b < a
⊢ ∃ (b : α), b < (↑a : α)

Tactic:
⟨b, hb⟩

Premises used: Exists.intro, Subtype.val
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
b : (↑s : Type u_1)
hb : b < a
⊢ ∃ (b : α), b < (↑a : α)

Tactic:
exact ⟨b, hb⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
x : α
⊢ IsSuccPrelimit (↑x : WithTop α) ↔
    (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccPrelimit y

Tactic:
simp [IsSuccPrelimit, WithTop.forall]

Premises used: Order.IsSuccPrelimit, WithTop.forall
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
⊢ IsSuccPrelimit.{u_1} (α := WithTop α) ⊤ ↔
    Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsSuccPrelimit y

Tactic:
simp [IsSuccPrelimit]

Premises used: Order.IsSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
x : WithTop α
coe :
  ∀ (x : α),
    IsSuccPrelimit (↑x : WithTop α) ↔
      (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccPrelimit y
top :
  IsSuccPrelimit.{u_1} (α := WithTop α) ⊤ ↔
    Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsSuccPrelimit y
⊢ IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsSuccPrelimit y

Tactic:
cases x with
  | coe x => simp [IsSuccPrelimit, WithTop.forall]
  | top => simp [IsSuccPrelimit]

Premises used: Order.IsSuccPrelimit, WithTop.forall
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
x : α
h : IsSuccPrelimit x
⊢ IsSuccPrelimit (↑x : WithTop α)

Tactic:
simpa [IsSuccPrelimit, WithTop.forall]

Premises used: Order.IsSuccPrelimit, WithTop.forall
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
⊢ IsSuccPrelimit.{u_1} (α := WithTop α) ⊤

Tactic:
simp [WithTop.isSuccPrelimit_iff]

Premises used: WithTop.isSuccPrelimit_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
x : α
⊢ IsSuccLimit (↑x : WithTop α) ↔ (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccLimit y

Tactic:
simp [IsSuccLimit, WithTop.isSuccPrelimit_iff, WithTop.exists]

Premises used: Order.IsSuccLimit, WithTop.isSuccPrelimit_iff, WithTop.exists
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
⊢ IsSuccLimit.{u_1} (α := WithTop α) ⊤ ↔
    Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsSuccLimit y

Tactic:
simp [IsSuccLimit, WithTop.exists]

Premises used: Order.IsSuccLimit, WithTop.exists
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
x : WithTop α
coe :
  ∀ (x : α),
    IsSuccLimit (↑x : WithTop α) ↔ (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccLimit y
top :
  IsSuccLimit.{u_1} (α := WithTop α) ⊤ ↔
    Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsSuccLimit y
⊢ IsSuccLimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsSuccLimit y

Tactic:
cases x with
  | coe x => simp [IsSuccLimit, WithTop.isSuccPrelimit_iff, WithTop.exists]
  | top => simp [IsSuccLimit, WithTop.exists]

Premises used: Order.IsSuccLimit, WithTop.isSuccPrelimit_iff, WithTop.exists
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
x : α
h : IsSuccLimit x
⊢ IsSuccLimit (↑x : WithTop α)

Tactic:
simpa [IsSuccLimit, WithTop.exists, h.isSuccPrelimit.withTopCoe] using h.not_isMin

Premises used: Order.IsSuccLimit, Order.IsSuccPrelimit.withTopCoe, Order.IsSuccLimit.not_isMin, Order.IsSuccLimit.isSuccPrelimit, WithTop.exists
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
⊢ IsSuccLimit.{u_1} (α := WithTop α) ⊤

Tactic:
simp [WithTop.isSuccLimit_iff]

Premises used: WithTop.isSuccLimit_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ IsPredPrelimit (↑x : WithTop α) ↔
    (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsPredLimit y

Tactic:
simp [IsPredPrelimit, IsPredLimit, WithTop.forall]

Premises used: WithTop.forall, Order.IsPredPrelimit, Order.IsPredLimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
⊢ IsPredPrelimit.{u_1} (α := WithTop α) ⊤ ↔
    Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsPredLimit y

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
x : WithTop α
coe :
  ∀ (x : α),
    IsPredPrelimit (↑x : WithTop α) ↔
      (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsPredLimit y
top :
  IsPredPrelimit.{u_1} (α := WithTop α) ⊤ ↔
    Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsPredLimit y
⊢ IsPredPrelimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsPredLimit y

Tactic:
cases x with
  | coe x => simp [IsPredPrelimit, IsPredLimit, WithTop.forall]
  | top => simp

Premises used: WithTop.forall, Order.IsPredPrelimit, Order.IsPredLimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
x : α
h : IsPredLimit x
⊢ IsPredLimit (↑x : WithTop α)

Tactic:
simpa [WithTop.isPredPrelimit_iff, IsPredLimit, WithTop.exists] using h

Premises used: WithTop.isPredPrelimit_iff, WithTop.exists, Order.IsPredLimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
h : IsSuccPrelimit (succ a)
by_contra : ∀ (H : ¬IsMax a), False
⊢ IsMax a

Tactic:
by_contra H
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
h : IsSuccPrelimit (succ a)
H : ¬IsMax a
⊢ False

Tactic:
h a (covBy_succ_of_not_isMax H)

Premises used: Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
h : IsSuccPrelimit (succ a)
H : ¬IsMax a
⊢ False

Tactic:
exact h a (covBy_succ_of_not_isMax H)

Premises used: Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
h : IsSuccLimit (succ a)
⊢ IsMax a

Tactic:
h.isSuccPrelimit.isMax

Premises used: Order.IsSuccPrelimit.isMax, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
ha : ¬IsMax a
⊢ ¬IsSuccPrelimit (succ a)

Tactic:
mt IsSuccPrelimit.isMax ha

Premises used: mt, Order.IsSuccPrelimit.isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
ha : ¬IsMax a
⊢ ¬IsSuccLimit (succ a)

Tactic:
mt IsSuccLimit.isMax ha

Premises used: Order.IsSuccLimit.isMax, mt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ b)
⊢ False

Tactic:
not_isMax _ h.isMax

Premises used: not_isMax, Order.IsSuccPrelimit.isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ b)
⊢ False

Tactic:
exact not_isMax _ h.isMax

Premises used: not_isMax, Order.IsSuccPrelimit.isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
h : IsSuccLimit a
b : α
⊢ succ b ≠ a

Tactic:
h.isSuccPrelimit.succ_ne b

Premises used: Order.IsSuccPrelimit.succ_ne, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ ¬IsSuccPrelimit (succ a)

Tactic:
fun h => h.succ_ne _ rfl

Premises used: Order.IsSuccPrelimit.succ_ne, Not, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ ¬IsSuccLimit (succ a)

Tactic:
fun h => h.succ_ne _ rfl

Premises used: Order.IsSuccLimit.succ_ne, Not, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
zero : ∀ (h : IsSuccPrelimit (Order.succ^[0] b)) (hb : b ≤ Order.succ^[0] b), Order.succ^[0] b ≤ b
succ : ∀ (n : ℕ) (h : IsSuccPrelimit (Order.succ^[n + 1] b)) (hb : b ≤ Order.succ^[n + 1] b), Order.succ^[n + 1] b ≤ b
⊢ a ≤ b

Tactic:
rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩

Premises used: LE.le.exists_succ_iterate, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ^[0] b)
hb : b ≤ succ^[0] b
⊢ succ^[0] b ≤ b

Tactic:
le_rfl

Premises used: le_rfl, Nat.iterate
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ^[0] b)
hb : b ≤ succ^[0] b
⊢ succ^[0] b ≤ b

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
⊢ IsSuccPrelimit (succ (succ^[n] b))

Tactic:
rw [iterate_succ_apply'] at h

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
h₁ : IsSuccPrelimit (succ (succ^[n] b))
⊢ b ≤ succ^[n + 1] b

Tactic:
rw [iterate_succ_apply'] at h

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ (succ^[n] b))
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
(not_isSuccPrelimit_succ _ h).elim

Premises used: False.elim, Order.not_isSuccPrelimit_succ
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ (succ^[n] b))
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
exact (not_isSuccPrelimit_succ _ h).elim

Premises used: False.elim, Order.not_isSuccPrelimit_succ
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
⊢ IsSuccPrelimit a ↔ IsMin a

Tactic:
⟨IsSuccPrelimit.isMin_of_noMax, IsMin.isSuccPrelimit⟩

Premises used: IsMin.isSuccPrelimit, Order.IsSuccPrelimit.isMin_of_noMax, Iff.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
⊢ ¬IsSuccLimit a

Tactic:
fun h ↦ h.not_isMin h.isSuccPrelimit.isMin_of_noMax

Premises used: Order.IsSuccPrelimit.isMin_of_noMax, Order.IsSuccLimit.not_isMin, Order.IsSuccLimit.isSuccPrelimit, Not
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
inst_4 : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : OrderBot α
rw : ¬IsMin a ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
rw₁ rw₂ : ¬a = ⊥ ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Tactic:
rw [IsSuccLimit, isMin_iff_eq_bot]

Premises used: Order.IsSuccLimit, isMin_iff_eq_bot
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ∀ (b : α), succ b ≠ a
⊢ IsSuccPrelimit a

Tactic:
fun b hba =>
  h b (CovBy.succ_eq hba)

Premises used: Order.IsSuccPrelimit, CovBy.succ_eq, Not
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
rw : (∃ (b : α), b ⋖ a) ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a
⊢ ¬IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a

Tactic:
rw [not_isSuccPrelimit_iff]

Premises used: Order.not_isSuccPrelimit_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
⊢ (∃ (b : α), b ⋖ a) ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a

Tactic:
exists_congr fun b ↦ ⟨fun hba ↦ ⟨hba.lt.not_isMax, hba.succ_eq⟩, ?_⟩

Premises used: CovBy.succ_eq, exists_congr, And.intro, Iff.intro, CovBy.lt, LT.lt.not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
refine : ∀ (b : α), ¬IsMax b ∧ succ b = a → b ⋖ a
⊢ (∃ (b : α), b ⋖ a) ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a

Tactic:
refine exists_congr fun b ↦ ⟨fun hba ↦ ⟨hba.lt.not_isMax, hba.succ_eq⟩, ?_⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
b : α
h : ¬IsMax b
⊢ b ⋖ succ b

Tactic:
covBy_succ_of_not_isMax h

Premises used: Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
b : α
h : ¬IsMax b
⊢ b ⋖ succ b

Tactic:
exact covBy_succ_of_not_isMax h

Premises used: Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ¬IsSuccPrelimit a
obtain : ∀ (b : α) (hb : ¬IsMax b ∧ succ b = a), Membership.mem (γ := Set α) (range succ) a
⊢ Membership.mem (γ := Set α) (range succ) a

Tactic:
obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff_succ_eq.1 h

Premises used: Order.not_isSuccPrelimit_iff_succ_eq, Iff.mp
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ¬IsSuccPrelimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ Membership.mem (γ := Set α) (range succ) a

Tactic:
⟨b, hb.2⟩

Premises used: Set.Mem, setOf, And.right, Exists.intro, Set.range
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ¬IsSuccPrelimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ Membership.mem (γ := Set α) (range succ) a

Tactic:
exact ⟨b, hb.2⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
⊢ Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a

Tactic:
or_iff_not_imp_right.2 <| mem_range_succ_of_not_isSuccPrelimit

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Order.mem_range_succ_of_not_isSuccPrelimit