F : Type ?u.231366
α : Type u_2
β : Type u_1
γ : Type ?u.231375
ι : Type ?u.231378
κ : Type ?u.231381
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
hb : ¬b ∈ s
h : Finset.Nonempty (cons b s hb)
⊢ ↑(sup' (cons b s hb) h f) = ↑(f b ⊔ sup' s H f)
F : Type ?u.231366
α : Type u_2
β : Type u_1
γ : Type ?u.231375
ι : Type ?u.231378
κ : Type ?u.231381
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
hb : ¬b ∈ s
h : Finset.Nonempty (cons b s hb)
⊢ sup' (cons b s hb) h f = f b ⊔ sup' s H f
rw [← WithBot.coe_eq_coe]
no goals
F : Type ?u.231366
α : Type u_2
β : Type u_1
γ : Type ?u.231375
ι : Type ?u.231378
κ : Type ?u.231381
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
hb : ¬b ∈ s
h : Finset.Nonempty (cons b s hb)
⊢ ↑(sup' (cons b s hb) h f) = ↑(f b ⊔ sup' s H f)
simp [WithBot.coe_sup]