awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
⊢ Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a

Tactic:
have := mem_range_succ_or_isSuccPrelimit a
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₃ inl₄ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₅ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ¬IsMin a
inl₆ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
inr₃ inr₄ :
  ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₅ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → ¬IsMin a
inr₆ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
inl₇ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ∀ (b : α), ¬b ⋖ a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a

Tactic:
tauto
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
inst : PartialOrder α
inst_1 : SuccOrder α
H : ∀ a < b, succ a < b
⊢ IsSuccPrelimit b

Tactic:
fun a hab ↦ (H a hab.lt).ne hab.succ_eq

Premises used: Order.IsSuccPrelimit, CovBy.succ_eq, CovBy.lt, Not, LT.lt.ne
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
pos : ∀ (h : IsMax a), succ a < b
neg : ∀ (h : ¬IsMax a), succ a < b
⊢ succ a < b

Tactic:
by_cases h : IsMax a

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : IsMax a
pos pos₁ pos₂ pos₃ : a < b
⊢ succ a < b

Tactic:
rwa [h.succ_eq]

Premises used: IsMax.succ_eq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
neg : a < b ∧ succ a ≠ b
⊢ succ a < b

Tactic:
rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]

Premises used: lt_iff_le_and_ne, Order.succ_le_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b

Tactic:
⟨ha, fun hab => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
neg : ∀ (hab : succ a = b), False
⊢ a < b ∧ succ a ≠ b

Tactic:
refine ⟨ha, fun hab => ?_⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ IsSuccPrelimit (succ a)

Tactic:
subst hab
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
hb₁ : IsSuccPrelimit (succ a)
⊢ a < succ a

Tactic:
subst hab
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ¬IsMax a
hb : IsSuccPrelimit (succ a)
ha : a < succ a
⊢ False

Tactic:
(h hb.isMax).elim

Premises used: False.elim, Order.IsSuccPrelimit.isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ¬IsMax a
hb : IsSuccPrelimit (succ a)
ha : a < succ a
⊢ False

Tactic:
exact (h hb.isMax).elim

Premises used: False.elim, Order.IsSuccPrelimit.isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccLimit b
ha : a < b
⊢ succ a < b

Tactic:
hb.isSuccPrelimit.succ_lt ha

Premises used: Order.IsSuccPrelimit.succ_lt, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
⊢ succ a < b ↔ a < b

Tactic:
⟨fun h => (le_succ a).trans_lt h, hb.succ_lt⟩

Premises used: Iff.intro, Order.IsSuccPrelimit.succ_lt, Order.le_succ, LE.le.trans_lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccLimit b
⊢ succ a < b ↔ a < b

Tactic:
hb.isSuccPrelimit.succ_lt_iff

Premises used: Order.IsSuccPrelimit.succ_lt_iff, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
inst : PartialOrder α
inst_1 : SuccOrder α
⊢ IsSuccPrelimit b ↔ ∀ a < b, succ a < b

Tactic:
⟨fun hb _ => hb.succ_lt, isSuccPrelimit_of_succ_lt⟩

Premises used: Iff.intro, Order.IsSuccPrelimit.succ_lt, Order.isSuccPrelimit_of_succ_lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
⊢ IsSuccPrelimit a ↔ ∀ (b : α), succ b ≠ a

Tactic:
⟨IsSuccPrelimit.succ_ne, isSuccPrelimit_of_succ_ne⟩

Premises used: Order.IsSuccPrelimit.succ_ne, Order.isSuccPrelimit_of_succ_ne, Iff.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
simp_rw : (¬∀ (b : α), succ b ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
simp_rw₁ : (∃ (x : α), ¬succ x ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
simp_rw₂ : (∃ (x : α), succ x = a) ↔ Membership.mem (γ := Set α) (range succ) a
⊢ ¬IsSuccPrelimit a ↔ Membership.mem (γ := Set α) (range succ) a

Tactic:
simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]

Premises used: Set.mem_range, not_ne_iff, Order.isSuccPrelimit_iff_succ_ne, Classical.not_forall
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
revert : ∀ (h : IsSuccPrelimit a), a ≤ b
⊢ a ≤ b

Tactic:
revert h
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ ∀ (h : IsSuccPrelimit a), a ≤ b

Tactic:
Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb

Premises used: Succ.rec
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
refine : ∀ (c : α), b ≤ c → ∀ (H : ∀ (h : IsSuccPrelimit c), c ≤ b) (hc : IsSuccPrelimit (succ c)), succ c ≤ b
⊢ ∀ (h : IsSuccPrelimit a), a ≤ b

Tactic:
refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
h : b ≤ c
H : ∀ (h : IsSuccPrelimit c), c ≤ b
hc : IsSuccPrelimit (succ c)
⊢ succ c = c

Tactic:
have := hc.isMax.succ_eq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
h : b ≤ c
H : ∀ (h : IsSuccPrelimit c), c ≤ b
hc : IsSuccPrelimit (succ c)
this : succ c = c
rw : ∀ (hc : IsSuccPrelimit c) (this : succ c = c), c ≤ b
⊢ succ c ≤ b

Tactic:
rw [this] at hc ⊢
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
h : b ≤ c
H : ∀ (h : IsSuccPrelimit c), c ≤ b
hc : IsSuccPrelimit c
this : succ c = c
⊢ c ≤ b

Tactic:
H hc
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
h : b ≤ c
H : ∀ (h : IsSuccPrelimit c), c ≤ b
hc : IsSuccPrelimit c
this : succ c = c
⊢ c ≤ b

Tactic:
exact H hc
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
⊢ IsSuccPrelimit a ↔ IsMin a

Tactic:
⟨IsSuccPrelimit.isMin, IsMin.isSuccPrelimit⟩

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

Tactic:
fun h ↦ h.not_isMin <| h.isSuccPrelimit.isMin

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

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit a
mpr : (∀ c < a, c ≤ b) → a ≤ b
⊢ a ≤ b ↔ ∀ c < a, c ≤ b

Tactic:
use fun ha c hc ↦ hc.le.trans ha
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
mpr : ∀ (ha : b < a), False
⊢ a ≤ b

Tactic:
by_contra! ha
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
ha : b < a
⊢ False

Tactic:
h b ⟨ha, fun c hb hc ↦ (H c hc).not_gt hb⟩

Premises used: LE.le.not_gt, And.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
ha : b < a
⊢ False

Tactic:
exact h b ⟨ha, fun c hb hc ↦ (H c hc).not_gt hb⟩

Premises used: LE.le.not_gt, And.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccLimit a
⊢ a ≤ b ↔ ∀ c < a, c ≤ b

Tactic:
h.isSuccPrelimit.le_iff_forall_le

Premises used: Order.IsSuccPrelimit.le_iff_forall_le, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit b
rw : ¬a < b ↔ ¬∃ c < b, a < c
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit b
⊢ ¬a < b ↔ ¬∃ c < b, a < c

Tactic:
simp [h.le_iff_forall_le]

Premises used: Order.IsSuccPrelimit.le_iff_forall_le
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccLimit b
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
h.isSuccPrelimit.lt_iff_exists_lt

Premises used: Order.IsSuccPrelimit.lt_iff_exists_lt, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
obtain : ∀ (c : α) (hc : c ∈ s) (hbc : b < c) (hca : c ≤ a), False
⊢ False

Tactic:
obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt

Premises used: IsLUB.exists_between, CovBy.lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
⊢ a ∈ s

Tactic:
obtain rfl := (hb.ge_of_gt hbc).antisymm hca

Premises used: LE.le.antisymm, CovBy.ge_of_gt, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
hc₁ : a ∈ s
⊢ b < a

Tactic:
obtain rfl := (hb.ge_of_gt hbc).antisymm hca

Premises used: LE.le.antisymm, CovBy.ge_of_gt, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
hc₁ : a ∈ s
hbc₁ : b < a
⊢ a ≤ a

Tactic:
obtain rfl := (hb.ge_of_gt hbc).antisymm hca

Premises used: LE.le.antisymm, CovBy.ge_of_gt, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
hc : a ∈ s
hbc : b < a
hca : a ≤ a
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : ¬IsSuccPrelimit a
⊢ a ∈ s

Tactic:
ha.imp_symm hs.isSuccPrelimit_of_notMem

Premises used: Not.imp_symm, IsLUB.isSuccPrelimit_of_notMem
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ IsSuccLimit a

Tactic:
⟨?_, hs.isSuccPrelimit_of_notMem ha⟩

Premises used: Order.IsSuccLimit, IsLUB.isSuccPrelimit_of_notMem, And.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
refine : ¬IsMin a
⊢ IsSuccLimit a

Tactic:
refine ⟨?_, hs.isSuccPrelimit_of_notMem ha⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
obtain : ∀ (b : α) (hb : b ∈ s), ¬IsMin a
⊢ ¬IsMin a

Tactic:
obtain ⟨b, hb⟩ := hs'
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
inl : ∀ (hs : IsLUB s b) (ha : b ∉ s), ¬IsMin b
inr : ∀ (hb : b < a), ¬IsMin a
⊢ ¬IsMin a

Tactic:
obtain rfl | hb := (hs.1 hb).eq_or_lt

Premises used: LE.le.eq_or_lt, And.left, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
b : α
hb : b ∈ s
hs : IsLUB s b
ha : b ∉ s
⊢ ¬IsMin b

Tactic:
contradiction
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb_1 : b ∈ s
hb : b < a
⊢ ¬IsMin a

Tactic:
hb.not_isMin

Premises used: LT.lt.not_isMin
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb_1 : b ∈ s
hb : b < a
⊢ ¬IsMin a

Tactic:
exact hb.not_isMin

Premises used: LT.lt.not_isMin
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : ¬IsSuccLimit a
⊢ a ∈ s

Tactic:
ha.imp_symm <| hs.isSuccLimit_of_notMem hs'

Premises used: Not.imp_symm, IsLUB.isSuccLimit_of_notMem
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
⊢ IsLUB (Iio a) a

Tactic:
⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩

Premises used: le_of_lt, IsLeast, le_of_forall_lt, And.intro, IsLUB
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
refine : ∀ (b : α) (hb : b ∈ upperBounds (Iio a)) (c : α) (hc : c < a), c < b
⊢ IsLUB (Iio a) a

Tactic:
refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
obtain : ∀ (d : α) (hd : d < a) (hd' : c < d), c < b
⊢ c < b

Tactic:
obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc

Premises used: Order.IsSuccPrelimit.lt_iff_exists_lt, Iff.mp
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
d : α
hd : d < a
hd' : c < d
⊢ c < b

Tactic:
hd'.trans_le (hb hd)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
d : α
hd : d < a
hd' : c < d
⊢ c < b

Tactic:
exact hd'.trans_le (hb hd)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccLimit a
⊢ IsLUB (Iio a) a

Tactic:
ha.isSuccPrelimit.isLUB_Iio

Premises used: Order.IsSuccPrelimit.isLUB_Iio, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a

Tactic:
⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩

Premises used: Order.IsSuccPrelimit.isLUB_Iio, Iff.intro
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
refine : ∀ (ha : IsLUB (Iio a) a) (b : α) (hb : b ⋖ a), False
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a

Tactic:
refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsLUB (Iio a) a
b : α
hb : b ⋖ a
⊢ IsLUB (Iic b) a

Tactic:
rw [hb.Iio_eq] at ha

Premises used: CovBy.Iio_eq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsLUB (Iio a) a
b : α
hb : b ⋖ a
ha₁ : IsLUB (Iic b) a
⊢ b ⋖ a

Tactic:
rw [hb.Iio_eq] at ha

Premises used: CovBy.Iio_eq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
⊢ IsLUB (Iic b) b

Tactic:
obtain rfl := isLUB_Iic.unique ha

Premises used: IsLUB.unique, isLUB_Iic, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
ha₁ : IsLUB (Iic b) b
⊢ b ⋖ b

Tactic:
obtain rfl := isLUB_Iic.unique ha

Premises used: IsLUB.unique, isLUB_Iic, rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : LinearOrder α
b : α
ha : IsLUB (Iic b) b
hb : b ⋖ b
⊢ False

Tactic:
cases hb.lt.false

Premises used: LT.lt.false, CovBy.lt
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
⊢ b ≤ succ a ↔ b ≤ a

Tactic:
le_iff_le_iff_lt_iff_lt.2 hb.succ_lt_iff

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Order.IsSuccPrelimit.succ_lt_iff
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
inst_1 : SuccOrder α
hb : IsSuccLimit b
⊢ b ≤ succ a ↔ b ≤ a

Tactic:
hb.isSuccPrelimit.le_succ_iff

Premises used: Order.IsSuccPrelimit.le_succ_iff, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : IsSuccPrelimit b
⊢ isSuccPrelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit = isSuccPrelimit b hb

Tactic:
dif_pos hb

Premises used: dif_pos, Order.isSuccPrelimitRecOn
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
⊢ ¬IsSuccPrelimit (Order.succ b)

Tactic:
have hb' := mt IsSuccPrelimit.isMax hb
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
⊢ ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b

Tactic:
have H := Classical.choose_spec (not_isSuccPrelimit_iff_succ_eq.1 hb')
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
rw :
  HEq (α := motive (Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯)))
    (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯) (succ b hb)
⊢ isSuccPrelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit = succ b hb

Tactic:
rw [isSuccPrelimitRecOn, dif_neg hb', cast_eq_iff_heq]

Premises used: dif_neg, cast_eq_iff_heq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
e'_1 : Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯ = b
⊢ HEq (α := motive (Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯)))
    (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯) (succ b hb)

Tactic:
congr!
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
⊢ Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯ = b

Tactic:
(succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2

Premises used: And.right, And.left, Iff.mp, Order.succ_eq_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
⊢ Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯ = b

Tactic:
exact (succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2

Premises used: And.right, And.left, Iff.mp, Order.succ_eq_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
inst_2 : NoMaxOrder α
b : α
⊢ isSuccPrelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit = succ b ⋯

Tactic:
isSuccPrelimitRecOn_succ_of_not_isMax ..

Premises used: Order.isSuccPrelimitRecOn_succ_of_not_isMax