awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
obtain : ∀ (y : α) (hy : sInf s ⋖ y), sInf s ∈ s
⊢ sInf s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Premises used: not_forall_not, Iff.mp
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
obtain : ∀ (i : α) (his : i ∈ s) (hi : i < y), sInf s ∈ s
⊢ sInf s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := exists_lt_of_csInf_lt hne hy.lt

Premises used: CovBy.lt, exists_lt_of_csInf_lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s

Tactic:
eq_of_le_of_not_lt (csInf_le hbdd his) (hy.2 · hi) ▸ his

Premises used: Set.Mem, Eq.rec, And.right, Eq.symm, csInf_le, eq_of_le_of_not_lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s

Tactic:
exact eq_of_le_of_not_lt (csInf_le hbdd his) (hy.2 · hi) ▸ his
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Nonempty ι
f : ι → α
hf : BddAbove (range f)
hf' : ¬IsSuccPrelimit.{u_2} (α := α) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
csSup_mem_of_not_isSuccPrelimit (range_nonempty f) hf hf'

Premises used: Set.Mem, iSup, setOf, Set.range_nonempty, Set.range, csSup_mem_of_not_isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Nonempty ι
f : ι → α
hf : BddBelow (range f)
hf' : ¬IsPredPrelimit.{u_2} (α := α) (⨅ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨅ (i : ι), f i

Tactic:
csInf_mem_of_not_isPredPrelimit (range_nonempty f) hf hf'

Premises used: iInf, Set.Mem, setOf, csInf_mem_of_not_isPredPrelimit, Set.range_nonempty, Set.range
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
x : α
hs : IsLUB s x
hne : s.Nonempty
hx : ¬IsSuccPrelimit x
⊢ x ∈ s

Tactic:
hs.csSup_eq hne ▸ csSup_mem_of_not_isSuccPrelimit hne hs.bddAbove (hs.csSup_eq hne ▸ hx)

Premises used: Eq.rec, IsLUB.csSup_eq, Eq.symm, IsLUB.bddAbove, csSup_mem_of_not_isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
x : α
hs : IsGLB s x
hne : s.Nonempty
hx : ¬IsPredPrelimit x
⊢ x ∈ s

Tactic:
hs.csInf_eq hne ▸ csInf_mem_of_not_isPredPrelimit hne hs.bddBelow (hs.csInf_eq hne ▸ hx)

Premises used: IsGLB.bddBelow, Eq.rec, csInf_mem_of_not_isPredPrelimit, IsGLB.csInf_eq, Eq.symm
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Nonempty ι
f : ι → α
x : α
hf : IsLUB (range f) x
hx : ¬IsSuccPrelimit x
⊢ ∃ (i : ι), f i = x

Tactic:
hf.mem_of_nonempty_of_not_isSuccPrelimit (range_nonempty f) hx

Premises used: IsLUB.mem_of_nonempty_of_not_isSuccPrelimit, Set.Mem, setOf, Set.range_nonempty, Set.range
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Nonempty ι
f : ι → α
x : α
hf : IsGLB (range f) x
hx : ¬IsPredPrelimit x
⊢ ∃ (i : ι), f i = x

Tactic:
hf.mem_of_nonempty_of_not_isPredPrelimit (range_nonempty f) hx

Premises used: Set.Mem, setOf, IsGLB.mem_of_nonempty_of_not_isPredPrelimit, Set.range_nonempty, Set.range
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
inl : ∀ (hlim : ¬IsSuccPrelimit.{u_2} (α := α) (sSup ∅)), Membership.mem (γ := Set α) ∅ (sSup ∅)
inr : ∀ (hs : s.Nonempty), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
hlim : ¬IsSuccPrelimit.{u_2} (α := α) (sSup ∅)
⊢ Membership.mem (γ := Set α) ∅ (sSup ∅)

Tactic:
simp [isSuccPrelimit_bot] at hlim

Premises used: Order.isSuccPrelimit_bot
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
apply : BddAbove s
⊢ sSup s ∈ s

Tactic:
apply csSup_mem_of_not_isSuccPrelimit hs _ hlim

Premises used: csSup_mem_of_not_isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
contrapose! : ∀ (hlim : ¬BddAbove s), IsSuccPrelimit (sSup s)
⊢ BddAbove s

Tactic:
contrapose! hlim
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
rw : IsSuccPrelimit.{u_2} (α := α) ⊥
⊢ IsSuccPrelimit (sSup s)

Tactic:
rw [csSup_of_not_bddAbove hlim, csSup_empty]

Premises used: csSup_empty, csSup_of_not_bddAbove
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit.{u_2} (α := α) ⊥

Tactic:
isSuccPrelimit_bot

Premises used: Order.isSuccPrelimit_bot
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit.{u_2} (α := α) ⊥

Tactic:
exact isSuccPrelimit_bot

Premises used: Order.isSuccPrelimit_bot
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf' : ¬IsSuccPrelimit.{u_2} (α := α) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
csSup_mem_of_not_isSuccPrelimit' hf'

Premises used: Set.Mem, iSup, setOf, csSup_mem_of_not_isSuccPrelimit', Set.range
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : ¬IsSuccLimit (sSup s)
⊢ sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)

Tactic:
rw [isSuccLimit_iff_of_orderBot, not_and_or, not_ne_iff] at hlim

Premises used: not_ne_iff, not_and_or, Order.isSuccLimit_iff_of_orderBot
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
hlim.elim (fun h ↦ ?_) csSup_mem_of_not_isSuccPrelimit'

Premises used: csSup_mem_of_not_isSuccPrelimit', Or.elim
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s = ⊥

Tactic:
refine hlim.elim (fun h ↦ ?_) csSup_mem_of_not_isSuccPrelimit'

Premises used: csSup_mem_of_not_isSuccPrelimit', Or.elim
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
obtain : ∀ (a : α) (ha : a ∈ s), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain ⟨a, ha⟩ := hne
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
a : α
ha : a ∈ s
inl : ∀ (ha : ⊥ ∈ s), sSup s ∈ s
inr : ∀ (ha' : ⊥ ≠ a), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain rfl | ha' := eq_or_ne ⊥ a

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
ha : ⊥ ∈ s
inl inl₁ inl₂ inl₃ : ⊥ ∈ s
⊢ sSup s ∈ s

Tactic:
rwa [h]
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
a : α
ha : a ∈ s
ha' : ⊥ ≠ a
⊢ sSup s ∈ s

Tactic:
exact (h ▸ ha'.bot_lt'.trans_le <| le_csSup hbbd ha).false.elim
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
inst_1 : Nonempty ι
hbbd : BddAbove (range f)
hf : ¬IsSuccLimit.{u_2} (α := α) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
csSup_mem_of_not_isSuccLimit (Set.range_nonempty _) hbbd hf

Premises used: Set.Mem, iSup, setOf, Set.range_nonempty, csSup_mem_of_not_isSuccLimit, Set.range
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
inl : ∀ (h : IsSuccPrelimit.{u_2} (α := α) ⊥), Eq.{u_2 + 1} (α := α) (sSup (Iio ⊥)) ⊥
inr : ∀ (hx : ⊥ < x), sSup (Iio x) = x
⊢ sSup (Iio x) = x

Tactic:
obtain rfl | hx := eq_bot_or_bot_lt x

Premises used: eq_bot_or_bot_lt, rfl
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit.{u_2} (α := α) ⊥
⊢ Eq.{u_2 + 1} (α := α) (sSup (Iio ⊥)) ⊥

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
h.isLUB_Iio.csSup_eq ⟨⊥, hx⟩

Premises used: Order.IsSuccPrelimit.isLUB_Iio, Bot.bot, IsLUB.csSup_eq, Exists.intro
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
exact h.isLUB_Iio.csSup_eq ⟨⊥, hx⟩

Premises used: Order.IsSuccPrelimit.isLUB_Iio, Bot.bot, IsLUB.csSup_eq, Exists.intro
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
rw : sSup (Iio x) = x
rw₁ rw₂ : x = x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x

Tactic:
rw [← sSup_eq_iSup', h.sSup_Iio]

Premises used: Order.IsSuccPrelimit.sSup_Iio, sSup_eq_iSup'
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccLimit x
⊢ sSup (Iio x) = x

Tactic:
h.isSuccPrelimit.sSup_Iio

Premises used: Order.IsSuccLimit.isSuccPrelimit, Order.IsSuccPrelimit.sSup_Iio
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccLimit x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x

Tactic:
h.isSuccPrelimit.iSup_Iio

Premises used: Order.IsSuccLimit.isSuccPrelimit, Order.IsSuccPrelimit.iSup_Iio
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩

Premises used: Iff.intro, Order.IsSuccPrelimit.sSup_Iio
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
refine : ∀ (h : sSup (Iio x) = x), IsSuccPrelimit x
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
by_contra : ∀ (hx : ¬IsSuccPrelimit x), False
⊢ IsSuccPrelimit x

Tactic:
by_contra hx
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit x
⊢ ¬IsSuccPrelimit (sSup (Iio x))

Tactic:
rw [← h] at hx
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False

Tactic:
simpa [h] using csSup_mem_of_not_isSuccPrelimit' hx

Premises used: csSup_mem_of_not_isSuccPrelimit'
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
rw : sSup (Iio x) = x ↔ IsSuccPrelimit x
rw₁ rw₂ : IsSuccPrelimit x ↔ IsSuccPrelimit x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x ↔ IsSuccPrelimit x

Tactic:
rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]

Premises used: sSup_Iio_eq_self_iff_isSuccPrelimit, sSup_eq_iSup'
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
⊢ Membership.mem (γ := Set α) (upperBounds (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))) (succ x)

Tactic:
simp +contextual [upperBounds, succ_le_succ, le_of_lt]

Premises used: le_of_lt, upperBounds, Order.succ_le_succ
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
⊢ BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))

Tactic:
have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
    ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
apply : ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) ≤ x
apply₁ : ∀ (y : α) (hy : y < x), y < ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α)
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) = x

Tactic:
apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)

Premises used: le_of_forall_lt, le_antisymm
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
rw : ∀ (i : (↑(Iio x) : Type u_2)), succ (↑i : α) ≤ x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) ≤ x

Tactic:
rw [ciSup_le_iff' H]

Premises used: ciSup_le_iff'
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
⊢ ∀ (i : (↑(Iio x) : Type u_2)), succ (↑i : α) ≤ x

Tactic:
fun a ↦ succ_le_of_lt a.2

Premises used: Order.succ_le_of_lt, Subtype.property
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
⊢ ∀ (i : (↑(Iio x) : Type u_2)), succ (↑i : α) ≤ x

Tactic:
exact fun a ↦ succ_le_of_lt a.2

Premises used: Order.succ_le_of_lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
y : α
hy : y < x
rw : ∃ (i : (↑(Iio x) : Type u_2)), y < succ (↑i : α)
⊢ y < ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α)

Tactic:
rw [lt_ciSup_iff' H]

Premises used: lt_ciSup_iff'
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
y : α
hy : y < x
⊢ ∃ (i : (↑(Iio x) : Type u_2)), y < succ (↑i : α)

Tactic:
⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩

Premises used: Order.lt_succ_of_not_isMax, Subtype.mk, Exists.intro, LT.lt.not_isMax
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
y : α
hy : y < x
⊢ ∃ (i : (↑(Iio x) : Type u_2)), y < succ (↑i : α)

Tactic:
exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
obtain : ∀ (y : α) (hy : y ⋖ sSup s), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Premises used: not_forall_not, Iff.mp
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
obtain : ∀ (i : α) (his : i ∈ s) (hi : y < i), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt

Premises used: Iff.mp, lt_sSup_iff, CovBy.lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his

Premises used: Set.Mem, Eq.rec, And.right, le_sSup, eq_of_le_of_not_lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
exact eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
obtain : ∀ (y : α) (hy : sInf s ⋖ y), sInf s ∈ s
⊢ sInf s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Premises used: not_forall_not, Iff.mp
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
obtain : ∀ (i : α) (his : i ∈ s) (hi : i < y), sInf s ∈ s
⊢ sInf s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt

Premises used: sInf_lt_iff, Iff.mp, CovBy.lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s

Tactic:
eq_of_le_of_not_lt (sInf_le his) (hy.2 · hi) ▸ his

Premises used: Set.Mem, Eq.rec, And.right, sInf_le, Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s

Tactic:
exact eq_of_le_of_not_lt (sInf_le his) (hy.2 · hi) ▸ his
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLinearOrder α
f : ι → α
hf : ¬IsSuccPrelimit.{u_2} (α := α) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
sSup_mem_of_not_isSuccPrelimit hf

Premises used: Set.Mem, iSup, setOf, sSup_mem_of_not_isSuccPrelimit, Set.range
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLinearOrder α
f : ι → α
hf : ¬IsPredPrelimit.{u_2} (α := α) (⨅ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨅ (i : ι), f i

Tactic:
sInf_mem_of_not_isPredPrelimit hf

Premises used: iInf, Set.Mem, setOf, sInf_mem_of_not_isPredPrelimit, Set.range
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a b : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ CovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a ⋖ b

Tactic:
(isLowerSet_range f).ordConnected.apply_covBy_apply_iff f.toOrderEmbedding

Premises used: IsLowerSet.ordConnected, InitialSeg.toOrderEmbedding, Set.OrdConnected.apply_covBy_apply_iff, InitialSeg.isLowerSet_range
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a b : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ WCovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a ⩿ b

Tactic:
simp [wcovBy_iff_eq_or_covBy]

Premises used: wcovBy_iff_eq_or_covBy
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)

Tactic:
(f.apply_covBy_apply_iff.2 (covBy_succ a)).succ_eq.symm

Premises used: Iff.mpr, CovBy.succ_eq, InitialSeg.apply_covBy_apply_iff, Order.covBy_succ, Eq.symm
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : PredOrder α
inst_3 : NoMinOrder α
inst_4 : PredOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (pred a) : β) (pred ((f : (a : α) → β) a) : β)

Tactic:
(f.apply_covBy_apply_iff.2 (pred_covBy a)).pred_eq.symm

Premises used: Iff.mpr, CovBy.pred_eq, Order.pred_covBy, InitialSeg.apply_covBy_apply_iff, Eq.symm
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
mp : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β) → IsSuccPrelimit a
mpr : IsSuccPrelimit a → IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β)
⊢ IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsSuccPrelimit a

Tactic:
constructor
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β)
b : α
hb : b ⋖ a
⊢ CovBy.{u_2} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a : β)

Tactic:
rw [← f.apply_covBy_apply_iff] at hb

Premises used: InitialSeg.apply_covBy_apply_iff
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β)
b : α
hb : CovBy.{u_2} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a : β)
⊢ False

Tactic:
h _ hb
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β)
b : α
hb : CovBy.{u_2} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a : β)
⊢ False

Tactic:
exact h _ hb
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit a
b : β
hb : b ⋖ (f : (a : α) → β) a
mpr : ∀ (c : α) (hb : CovBy.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)), False
⊢ False

Tactic:
obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt

Premises used: InitialSeg.mem_range_of_rel, CovBy.lt, rfl