case a
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ (sup' s H fun x => a) ≤ a

case a
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ a ≤ sup' s H fun x => a
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ (sup' s H fun x => a) = a
apply le_antisymm
case a.hs
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ ∀ (b : β), b ∈ s → a ≤ a
case a
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ (sup' s H fun x => a) ≤ a
apply sup'_le
case a.hs
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
b✝ : β
a✝ : b✝ ∈ s
⊢ a ≤ a
case a.hs
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ ∀ (b : β), b ∈ s → a ≤ a
intros
no goals
case a.hs
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
b✝ : β
a✝ : b✝ ∈ s
⊢ a ≤ a
exact le_rfl
no goals
case a
F : Type ?u.250689
α : Type u_1
β : Type u_2
γ : Type ?u.250698
ι : Type ?u.250701
κ : Type ?u.250704
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ a ≤ sup' s H fun x => a
apply le_sup' (fun _ => a) H.choose_spec