awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
refine : ∀ (i : ι) (hi : p i), f ⋯ ≤ ⨆ (ih : Exists p), f ih
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
refine le_antisymm ciSup_exists_le <| ciSup_le' fun i ↦ ciSup_le' fun hi ↦ ?_

Premises used: ciSup_le', le_antisymm, ciSup_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
i : ι
hi : p i
⊢ f ⋯ ≤ ⨆ (ih : Exists p), f ih

Tactic:
simp [show Exists p from ⟨i, hi⟩]

Premises used: Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
pos : ∀ (hp : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
neg : ∀ (hp : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
by_cases hp : p
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
by_cases hq : q
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
by_cases hq : q
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
simp [hp, hq]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : ¬q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
simp [hp, hq]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
simp [hp, hq]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : ¬q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))

Tactic:
simp [hp, hq]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = ⨆ (x : (↑s : Type u_1)), l (↑x : α)

Tactic:
Eq.symm <| IsLUB.ciSup_set_eq (gc.isLUB_l_image <| isLUB_csSup hne hbdd) hne

Premises used: GaloisConnection.isLUB_l_image, IsLUB.ciSup_set_eq, isLUB_csSup, Eq.symm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
rw : ⨆ (x : (↑s : Type u_1)), l (↑x : α) = sSup (l '' s)
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑s : Type u_1)), l (↑x : α)) (⨆ (a : (↑s : Type u_1)), l (↑a : α))
⊢ l (sSup s) = sSup (l '' s)

Tactic:
rw [gc.l_csSup hne hbdd, sSup_image']

Premises used: GaloisConnection.l_csSup, sSup_image'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑(range f) : Type u_1)), l (↑x : α)) (⨆ (i : ι), l (f i))
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (⨆ (i : ι), l (f i)) (⨆ (i : ι), l (f i))
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)

Tactic:
rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']

Premises used: iSup, iSup_range', Set.range_nonempty, GaloisConnection.l_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
haveI := hne.to_subtype
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))

Tactic:
rw [image_eq_range] at hf

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
hf₁ : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
⊢ s.Nonempty

Tactic:
rw [image_eq_range] at hf

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
hf₁ : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne₁ : s.Nonempty
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
rw [image_eq_range] at hf

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))

Tactic:
gc.l_ciSup hf

Premises used: GaloisConnection.l_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))

Tactic:
exact gc.l_ciSup hf

Premises used: GaloisConnection.l_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set β
hne : s.Nonempty
hbdd : BddBelow s
⊢ u (sInf s) = ⨅ (x : (↑s : Type u_2)), u (↑x : β)

Tactic:
gc.dual.l_csSup hne hbdd

Premises used: iInf, GaloisConnection.dual, GaloisConnection.l_csSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set β
hne : s.Nonempty
hbdd : BddBelow s
⊢ u (sInf s) = sInf (u '' s)

Tactic:
gc.dual.l_csSup' hne hbdd

Premises used: GaloisConnection.l_csSup', GaloisConnection.dual, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → β
hf : BddBelow (range f)
⊢ u (⨅ (i : ι), f i) = ⨅ (i : ι), u (f i)

Tactic:
gc.dual.l_ciSup hf

Premises used: iInf, iSup, GaloisConnection.dual, GaloisConnection.l_ciSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → β
hf : BddBelow (f '' s)
hne : s.Nonempty
⊢ u (⨅ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨅ (i : (↑s : Type u_3)), u (f (↑i : γ))

Tactic:
gc.dual.l_ciSup_set hf hne

Premises used: iInf, iSup, GaloisConnection.dual, GaloisConnection.l_ciSup_set, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
e : α ≃o β
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ (x : (↑s : Type u_1)), (e : (a : α) → β) (↑x : α) : β)

Tactic:
e.to_galoisConnection.l_csSup hne hbdd

Premises used: OrderIso.to_galoisConnection, GaloisConnection.l_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
e : α ≃o β
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (sSup ((⇑e : (a : α) → β) '' s) : β)

Tactic:
e.to_galoisConnection.l_csSup' hne hbdd

Premises used: GaloisConnection.l_csSup', OrderIso.to_galoisConnection
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
e : α ≃o β
f : ι → α
hf : BddAbove (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
e.to_galoisConnection.l_ciSup hf

Premises used: OrderIso.to_galoisConnection, GaloisConnection.l_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
e : α ≃o β
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) : β)
    (⨆ (i : (↑s : Type u_3)), (e : (a : α) → β) (f (↑i : γ)) : β)

Tactic:
e.to_galoisConnection.l_ciSup_set hf hne

Premises used: OrderIso.to_galoisConnection, GaloisConnection.l_ciSup_set
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
e : α ≃o β
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ (x : (↑s : Type u_1)), (e : (a : α) → β) (↑x : α) : β)

Tactic:
e.dual.map_csSup hne hbdd

Premises used: iInf, OrderIso.dual, OrderIso.map_csSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
e : α ≃o β
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (sInf ((⇑e : (a : α) → β) '' s) : β)

Tactic:
e.dual.map_csSup' hne hbdd

Premises used: OrderIso.map_csSup', OrderIso.dual, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
e : α ≃o β
f : ι → α
hf : BddBelow (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨅ (i : ι), f i) : β) (⨅ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
e.dual.map_ciSup hf

Premises used: iInf, OrderIso.map_ciSup, OrderIso.dual, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
e : α ≃o β
s : Set γ
f : γ → α
hf : BddBelow (f '' s)
hne : s.Nonempty
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨅ (i : (↑s : Type u_3)), f (↑i : γ)) : β)
    (⨅ (i : (↑s : Type u_3)), (e : (a : α) → β) (f (↑i : γ)) : β)

Tactic:
e.dual.map_ciSup_set hf hne

Premises used: iInf, OrderIso.dual, OrderIso.map_ciSup_set, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
inl :
  IsEmpty ι → Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
inr :
  Nonempty ι → Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : IsEmpty ι
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
simp [map_bot]

Premises used: OrderIso.map_bot
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
pos :
  ∀ (hf : BddAbove (range f)),
    Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
neg :
  ∀ (hf : ¬BddAbove (range f)),
    Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
by_cases hf : BddAbove (range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
hf : BddAbove (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
e.map_ciSup hf

Premises used: OrderIso.map_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
hf : BddAbove (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
exact e.map_ciSup hf

Premises used: OrderIso.map_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
hf : ¬BddAbove (range f)
⊢ ¬BddAbove.{u_2} (α := β) (range fun (i : ι) ↦ (e : (a : α) → β) (f i))

Tactic:
simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf

Premises used: Function.Surjective.forall, upperBounds, OrderIso.surjective, BddAbove, Set.Nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
hf : ¬BddAbove (range f)
⊢ ¬BddAbove.{u_2} (α := β) (range fun (i : ι) ↦ (e : (a : α) → β) (f i))

Tactic:
have hfe : ¬ BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
hf : ¬BddAbove (range f)
hfe : ¬BddAbove.{u_2} (α := β) (range fun (i : ι) ↦ (e : (a : α) → β) (f i))
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
simp [map_bot, hf, hfe]

Premises used: OrderIso.map_bot
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
rw : (∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨆ (x : ι), (↑(f x) : WithTop α)) ⊤ ↔ ¬BddAbove (range f)

Tactic:
rw [iSup_eq_top, not_bddAbove_iff]

Premises used: iSup_eq_top, not_bddAbove_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y

Tactic:
⟨fun hf r => ?_, fun hf a ha => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
refine_1 : ∀ (hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) (r : α), ∃ y ∈ range f, r < y
refine_2 : ∀ (hf : ∀ (x : α), ∃ y ∈ range f, x < y) (a : WithTop α) (ha : a < ⊤), ∃ (i : ι), a < (↑(f i) : WithTop α)
⊢ (∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y

Tactic:
refine ⟨fun hf r => ?_, fun hf a ha => ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)
r : α
refine_1 : ∀ (i : ι) (hi : (↑r : WithTop α) < (↑(f i) : WithTop α)), ∃ y ∈ range f, r < y
⊢ ∃ y ∈ range f, r < y

Tactic:
rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩

Premises used: WithTop.coe_lt_top, WithTop.some
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)
r : α
i : ι
hi : (↑r : WithTop α) < (↑(f i) : WithTop α)
⊢ ∃ y ∈ range f, r < y

Tactic:
⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩

Premises used: WithTop.coe_lt_coe, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)
r : α
i : ι
hi : (↑r : WithTop α) < (↑(f i) : WithTop α)
⊢ ∃ y ∈ range f, r < y

Tactic:
exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
refine_2 : ∀ (i : ι) (hi : a.untop ⋯ < f i), ∃ (i : ι), a < (↑(f i) : WithTop α)
⊢ ∃ (i : ι), a < (↑(f i) : WithTop α)

Tactic:
rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩

Premises used: WithTop.untop, rfl, LT.lt.ne
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < (↑(f i) : WithTop α)

Tactic:
simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi

Premises used: Iff.mpr, WithTop.coe_untop, WithTop.coe_lt_coe, LT.lt.ne
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ ∃ (i : ι), a < (↑(f i) : WithTop α)

Tactic:
exact ⟨i, by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ LT.lt.{u_1} (α := WithTop α) (⨆ (x : ι), (↑(f x) : WithTop α)) ⊤ ↔ BddAbove (range f)

Tactic:
lt_top_iff_ne_top.trans iSup_coe_eq_top.not_left

Premises used: lt_top_iff_ne_top, Iff.not_left, WithTop.iSup_coe_eq_top, Iff.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨅ (x : ι), (↑(f x) : WithTop α)) ⊤ ↔ IsEmpty ι

Tactic:
simp [isEmpty_iff]

Premises used: isEmpty_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
rw : Ne.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
rw₁ : ¬Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
rw₂ : ¬IsEmpty ι ↔ Nonempty ι
rw₃ rw₄ : Nonempty ι ↔ Nonempty ι
⊢ LT.lt.{u_1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι

Tactic:
rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]

Premises used: WithTop.iInf_coe_eq_top, Ne, lt_top_iff_ne_top, not_isEmpty_iff
-- 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
hb : b ∈ s
h : a ≤ b
⊢ a ≤ sSup s

Tactic:
le_trans h (hd.le_csSup hs hb)

Premises used: DirectedOn.le_csSup, le_trans
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s t : Set α
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hdt : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
ht : BddAbove t
hs : s.Nonempty
h : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
hds.csSup_le hs fun _ ha => hdt.le_csSup ht (h ha)

Premises used: DirectedOn.csSup_le, DirectedOn.le_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : BddAbove s
hs : s.Nonempty
⊢ a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

Tactic:
⟨fun h _ hb => le_trans h (hd.csSup_le hs hb), fun hb => hb _ fun _ => hd.le_csSup h⟩

Premises used: DirectedOn.csSup_le, DirectedOn.le_csSup, Iff.intro, SupSet.sSup, le_trans
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
H : IsGreatest s a
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
fun _ h₁ _ h₂ ↦ ⟨a, H.1, H.2 h₁, H.2 h₂⟩

Premises used: DirectedOn, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
s : Set α
a : α
H : IsGreatest s a
⊢ sSup s = a

Tactic:
H.directedOn.isLUB_csSup H.nonempty ⟨a, H.2⟩ |>.unique H.isLUB

Premises used: IsGreatest.directedOn, IsGreatest.isLUB, IsLUB.unique, And.right, Exists.intro, IsGreatest.nonempty, DirectedOn.isLUB_csSup