awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
H : IsGreatest s a
⊢ sSup s ∈ s

Tactic:
H.csSup_eq.symm ▸ H.1

Premises used: Eq.rec, And.left, Eq.symm, IsGreatest.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hb : BddAbove s
hs : s.Nonempty
⊢ sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

Tactic:
isLUB_le_iff (hd.isLUB_csSup hs hb)

Premises used: Set.Mem, setOf, upperBounds, isLUB_le_iff, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
x : α
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : sSup s < x
hs : BddAbove s
⊢ x ∉ s

Tactic:
fun hx ↦ lt_irrefl _ <| (hd.le_csSup hs hx).trans_lt h

Premises used: lt_irrefl, DirectedOn.le_csSup, LE.le.trans_lt, Not
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
b : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
H : ∀ a ∈ s, a ≤ b
H' : ∀ w < b, ∃ a ∈ s, w < a
⊢ sSup s = b

Tactic:
(eq_of_le_of_not_lt (hd.csSup_le hs H)) fun hb =>
    let ⟨_, ha, ha'⟩ := H' _ hb
    lt_irrefl _ <| ha'.trans_le <| hd.le_csSup ⟨b, H⟩ ha

Premises used: False, lt_irrefl, DirectedOn.csSup_le, LT.lt.trans_le, DirectedOn.le_csSup, _private.0.DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt.match_1, Exists.intro, eq_of_le_of_not_lt, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a b : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : BddAbove s
ha : a ∈ s
h : b < a
⊢ b < sSup s

Tactic:
lt_of_lt_of_le h (hd.le_csSup hs ha)

Premises used: DirectedOn.le_csSup, lt_of_lt_of_le
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
a : α
⊢ sSup {a} = a

Tactic:
isGreatest_singleton.csSup_eq

Premises used: IsGreatest.csSup_eq, isGreatest_singleton
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_5
inst : ConditionallyCompletePartialOrderInf α
a : α
⊢ sInf (Ici a) = a

Tactic:
isLeast_Ici.csInf_eq

Premises used: isLeast_Ici, IsLeast.csInf_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_5
inst : ConditionallyCompletePartialOrderInf α
a b : α
h : a < b
⊢ sInf (Ico a b) = a

Tactic:
(isLeast_Ico h).csInf_eq

Premises used: IsLeast.csInf_eq, isLeast_Ico
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_5
inst : ConditionallyCompletePartialOrderInf α
a b : α
h : a ≤ b
⊢ sInf (Icc a b) = a

Tactic:
(isLeast_Icc h).csInf_eq

Premises used: isLeast_Icc, IsLeast.csInf_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
a : α
⊢ sSup (Iic a) = a

Tactic:
isGreatest_Iic.csSup_eq

Premises used: isGreatest_Iic, IsGreatest.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
a b : α
h : a < b
⊢ sSup (Ioc a b) = b

Tactic:
(isGreatest_Ioc h).csSup_eq

Premises used: isGreatest_Ioc, IsGreatest.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
a b : α
h : a ≤ b
⊢ sSup (Icc a b) = b

Tactic:
(isGreatest_Icc h).csSup_eq

Premises used: isGreatest_Icc, IsGreatest.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
inst_1 : OrderTop α
h : ⊤ ∈ s
⊢ sSup s = ⊤

Tactic:
IsGreatest.csSup_eq ⟨h, fun _ _ ↦ le_top⟩

Premises used: le_top, And.intro, IsGreatest.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrder α
s : Set α
hdb : DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) s
hda : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hb : BddBelow s
ha : BddAbove s
⊢ s ⊆ Icc (sInf s) (sSup s)

Tactic:
fun _ hx => ⟨hdb.csInf_le hb hx, hda.le_csSup ha hx⟩

Premises used: Set.Mem, setOf, Set.Subset, Set.Icc, And.intro, DirectedOn.le_csSup, DirectedOn.csInf_le
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrder α
s : Set α
hdb : DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) s
hda : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hb : BddBelow s
ha : BddAbove s
ne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
isGLB_le_isLUB (hdb.isGLB_csInf ne hb) (hda.isLUB_csSup ne ha) ne

Premises used: isGLB_le_isLUB, DirectedOn.isLUB_csSup, DirectedOn.isGLB_csInf
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Goal:
α : Type u_2
inst : ConditionallyCompletePartialOrderSup α
s : Set α
h_dir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h_non : s.Nonempty
h_bdd : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed s h_dir h_non h_bdd

Premises used: ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Goal:
α : Type u_2
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h_bdd : BddAbove s
ha : a ∈ s
⊢ a ≤ sSup s

Tactic:
(hs.isLUB_csSup ⟨a, ha⟩ h_bdd).1 ha

Premises used: And.left, Exists.intro, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Goal:
α : Type u_2
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h_non : s.Nonempty
ha : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a

Tactic:
(hd.isLUB_csSup h_non ⟨a, ha⟩).2 ha

Premises used: And.right, Exists.intro, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf_bdd : BddAbove (Set.range f)
i : ι
⊢ f i ≤ ⨆ (j : ι), f j

Tactic:
hf.directedOn_range.le_csSup hf_bdd <| Set.mem_range_self _

Premises used: Set.mem_range_self, iSup, Directed.directedOn_range, DirectedOn.le_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : ι → α
a : α
inst_1 : Nonempty ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
ha : ∀ (i : ι), f i ≤ a
⊢ ⨆ (i : ι), f i ≤ a

Tactic:
hf.directedOn_range.csSup_le (Set.range_nonempty _) <| Set.forall_mem_range.2 ha

Premises used: Iff.mpr, Set.forall_mem_range, DirectedOn.csSup_le, iSup, Directed.directedOn_range, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Nonempty ι
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
H : BddAbove (range f)
⊢ IsLUB (range f) (⨆ (i : ι), f i)

Tactic:
hd.directedOn_range.isLUB_csSup (range_nonempty f) H

Premises used: iSup, Directed.directedOn_range, Set.range_nonempty, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
rw : IsLUB (f '' s) (sSup (f '' s))
⊢ IsLUB (f '' s) (⨆ (i : (↑s : Type u_2)), f (↑i : β))

Tactic:
rw [← sSup_image']

Premises used: sSup_image'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))

Tactic:
hd.isLUB_csSup (Hne.image _) H

Premises used: Set.Nonempty.image, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))

Tactic:
exact hd.isLUB_csSup (Hne.image _) H

Premises used: Set.Nonempty.image, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Nonempty ι
f : ι → α
a : α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a

Tactic:
(isLUB_le_iff <| hd.isLUB_ciSup hf).trans forall_mem_range

Premises used: Set.forall_mem_range, isLUB_le_iff, Iff.trans, Directed.isLUB_ciSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
ι : Type u_5
s : Set ι
f : ι → α
a : α
hs : s.Nonempty
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
⊢ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) ≤ a ↔ ∀ i ∈ s, f i ≤ a

Tactic:
(isLUB_le_iff <| hd.isLUB_ciSup_set hf hs).trans forall_mem_image

Premises used: DirectedOn.isLUB_ciSup_set, isLUB_le_iff, Iff.trans, Set.forall_mem_image
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
a : α
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
H : BddAbove (range f)
c : ι
h : a ≤ f c
⊢ a ≤ iSup f

Tactic:
le_trans h (hd.le_ciSup H c)

Premises used: Directed.le_ciSup, le_trans
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
inl : IsEmpty ι → iSup f ≤ iSup g
inr : Nonempty ι → iSup f ≤ iSup g
⊢ iSup f ≤ iSup g

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : IsEmpty ι
inl : sSup ∅ ≤ iSup g
inl₁ inl₂ : LE.le.{u_1} (α := α) (sSup ∅) (sSup ∅)
⊢ iSup f ≤ iSup g

Tactic:
rw [iSup_of_empty', iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
hdf.ciSup_le fun x ↦ hdg.le_ciSup_of_le B x (H x)

Premises used: Directed.ciSup_le, Directed.le_ciSup_of_le
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
exact hdf.ciSup_le fun x ↦ hdg.le_ciSup_of_le B x (H x)

Premises used: Directed.ciSup_le, Directed.le_ciSup_of_le
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
c : β
hc : c ∈ s
⊢ f c ≤ ⨆ (i : (↑s : Type u_2)), f (↑i : β)

Tactic:
(hd.le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image'

Premises used: LE.le.trans_eq, Set.mem_image_of_mem, DirectedOn.le_csSup, sSup_image'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
rw : sSup (range fun (x : ι) ↦ a) = a
rw₁ : sSup {a} = a
rw₂ rw₃ : a = a
⊢ ⨆ (x : ι), a = a

Tactic:
rw [iSup, range_const, csSup_singleton]

Premises used: iSup, csSup_singleton, Set.range_const
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Unique ι
s : ι → α
⊢ ∀ (i : ι), s i = s default

Tactic:
have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Unique ι
s : ι → α
this : ∀ (i : ι), s i = s default
⊢ ⨆ (i : ι), s i = s default

Tactic:
simp only [this, ciSup_const]

Premises used: ciSup_const
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Subsingleton ι
i : ι
s : ι → α
⊢ ⨆ (i : ι), s i = s i

Tactic:
@ciSup_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _

Premises used: ciSup_unique
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : p
⊢ ⨆ (h : p), f h = f hp

Tactic:
simp [hp]
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (h : p) ↦ f h)) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (sSup ∅)

Tactic:
rw [iSup]

Premises used: iSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
e_a : Eq.{u_1 + 1} (α := Set α) (range fun (h : p) ↦ f h) ∅
⊢ Eq.{u_1 + 1} (α := α) (sSup (range fun (h : p) ↦ f h)) (sSup ∅)

Tactic:
congr
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
e_a : IsEmpty p
e_a₁ e_a₂ e_a₃ e_a₄ : ¬p
⊢ Eq.{u_1 + 1} (α := Set α) (range fun (h : p) ↦ f h) ∅

Tactic:
rwa [range_eq_empty_iff, isEmpty_Prop]

Premises used: Set.range_eq_empty_iff, isEmpty_Prop
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
inst_1 : Decidable p
f : p → α
pos : ∀ (H : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
neg : ∀ (H : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)

Tactic:
by_cases H : p
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
inst_1 : Decidable p
f : p → α
H : p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)

Tactic:
simp [ciSup_neg, H]

Premises used: ciSup_neg
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
inst_1 : Decidable p
f : p → α
H : ¬p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)

Tactic:
simp [ciSup_neg, H]

Premises used: ciSup_neg
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
simp : ⨆ (i : ι), f (Subtype.mk (p := p) i ⋯) = iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f

Tactic:
simp only [hp, ciSup_unique]

Premises used: ciSup_unique
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
simp : sSup (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = sSup (range.{u_1, max 1 u_4} f)
⊢ ⨆ (i : ι), f (Subtype.mk (p := p) i ⋯) = iSup.{u_1, max 1 u_4} f

Tactic:
simp only [iSup]

Premises used: iSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
e_a : (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = range.{u_1, max 1 u_4} f
⊢ sSup (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = sSup (range.{u_1, max 1 u_4} f)

Tactic:
congr
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
e_a : (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) ⊆ range.{u_1, max 1 u_4} f
e_a₁ : range.{u_1, max 1 u_4} f ⊆ range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)
⊢ (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = range.{u_1, max 1 u_4} f

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : ι
⊢ (fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) i ∈ range.{u_1, max 1 u_4} f

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : Subtype p
⊢ Membership.mem (γ := Set α) (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) (f i)

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
inl : IsEmpty ι → Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
inr : Nonempty ι → Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h : IsEmpty ι
inl inl₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)

Tactic:
rw [iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h : Nonempty ι
⊢ ∀ (i : ι), IsEmpty (p i)

Tactic:
have (i : ι) : IsEmpty (p i) := ⟨hp i⟩
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h : Nonempty ι
this : ∀ (i : ι), IsEmpty (p i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)

Tactic:
simp only [iSup_of_empty', ciSup_const]

Premises used: ciSup_const, iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (_ : Membership.mem (γ := Set β) ∅ i), f i) (sSup ∅)

Tactic:
cbiSup_eq_of_forall_not Set.notMem_empty

Premises used: cbiSup_eq_of_forall_not, Set.notMem_empty
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
b : α
inst_1 : Nonempty ι
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
h₁ : ∀ (i : ι), f i ≤ b
h₂ : ∀ w < b, ∃ (i : ι), w < f i
⊢ ⨆ (i : ι), f i = b

Tactic:
hd.directedOn_range.csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f)
    (forall_mem_range.mpr h₁) fun w hw => exists_range_iff.mpr <| h₂ w hw

Premises used: Iff.mpr, DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt, Set.forall_mem_range, iSup, Directed.directedOn_range, Set.range_nonempty, Set.exists_range_iff
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
⊢ Membership.mem (γ := Set α) (⋂ (n : β), Icc (f n) (g n)) (⨆ (n : β), f n)

Tactic:
mem_iInter.2 fun n => ?_

Premises used: Iff.mpr, Set.mem_iInter
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
refine : ∀ (n : β), ⨆ (n : β), f n ∈ Icc (f n) (g n)
⊢ Membership.mem (γ := Set α) (⋂ (n : β), Icc (f n) (g n)) (⨆ (n : β), f n)

Tactic:
refine mem_iInter.2 fun n => ?_

Premises used: Iff.mpr, Set.mem_iInter
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ Nonempty β

Tactic:
haveI : Nonempty β := ⟨n⟩
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ ∀ (m : β), f m ≤ g n

Tactic:
have h₁ : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
h₁ : ∀ (m : β), f m ≤ g n
⊢ Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
have h₂ : Directed (· ≤ ·) f := hf.directed_le
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
h₁ : ∀ (m : β), f m ≤ g n
h₂ : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ ⨆ (n : β), f n ∈ Icc (f n) (g n)

Tactic:
⟨h₂.le_ciSup ⟨g <| n, forall_mem_range.2 h₁⟩ _, h₂.ciSup_le h₁⟩

Premises used: Iff.mpr, Set.forall_mem_range, Set.Mem, setOf, Set.Icc, Directed.ciSup_le, And.intro, Exists.intro, Directed.le_ciSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
h₁ : ∀ (m : β), f m ≤ g n
h₂ : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ ⨆ (n : β), f n ∈ Icc (f n) (g n)

Tactic:
exact ⟨h₂.le_ciSup ⟨g <| n, forall_mem_range.2 h₁⟩ _, h₂.ciSup_le h₁⟩
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
h : Antitone.{u_2, u_1} (β := Set α) fun (n : β) ↦ Icc (f n) (g n)
h' : ∀ (n : β), f n ≤ g n
⊢ Membership.mem (γ := Set α) (⋂ (n : β), Icc (f n) (g n)) (⨆ (n : β), f n)

Tactic:
Monotone.ciSup_mem_iInter_Icc_of_antitone
    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'

Premises used: Set.Icc_subset_Icc_iff, Monotone.ciSup_mem_iInter_Icc_of_antitone, And.right, And.left, Iff.mp