case inl
F : Type ?u.47469
α : Type u_2
β : Type u_1
γ : Type ?u.47478
ι : Type ?u.47481
κ : Type ?u.47484
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ (sup ∅ fun x => ⊥) = ⊥

case inr
F : Type ?u.47469
α : Type u_2
β : Type u_1
γ : Type ?u.47478
ι : Type ?u.47481
κ : Type ?u.47484
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
s : Finset β
hs : Finset.Nonempty s
⊢ (sup s fun x => ⊥) = ⊥
F : Type ?u.47469
α : Type u_2
β : Type u_1
γ : Type ?u.47478
ι : Type ?u.47481
κ : Type ?u.47484
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
s : Finset β
⊢ (sup s fun x => ⊥) = ⊥
obtain rfl | hs := s.eq_empty_or_nonempty
no goals
case inl
F : Type ?u.47469
α : Type u_2
β : Type u_1
γ : Type ?u.47478
ι : Type ?u.47481
κ : Type ?u.47484
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ (sup ∅ fun x => ⊥) = ⊥
exact sup_empty
no goals
case inr
F : Type ?u.47469
α : Type u_2
β : Type u_1
γ : Type ?u.47478
ι : Type ?u.47481
κ : Type ?u.47484
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
s : Finset β
hs : Finset.Nonempty s
⊢ (sup s fun x => ⊥) = ⊥
exact sup_const hs _