F : Type ?u.239145
α : Type u_2
β : Type u_1
γ : Type ?u.239154
ι : Type ?u.239157
κ : Type ?u.239160
inst✝¹ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
inst✝ : DecidableEq β
b : β
h : Finset.Nonempty (insert b s)
⊢ ↑(sup' (insert b s) h f) = ↑(f b ⊔ sup' s H f)
F : Type ?u.239145
α : Type u_2
β : Type u_1
γ : Type ?u.239154
ι : Type ?u.239157
κ : Type ?u.239160
inst✝¹ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
inst✝ : DecidableEq β
b : β
h : Finset.Nonempty (insert b s)
⊢ sup' (insert b s) h f = f b ⊔ sup' s H f
rw [← WithBot.coe_eq_coe]
no goals
F : Type ?u.239145
α : Type u_2
β : Type u_1
γ : Type ?u.239154
ι : Type ?u.239157
κ : Type ?u.239160
inst✝¹ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
inst✝ : DecidableEq β
b : β
h : Finset.Nonempty (insert b s)
⊢ ↑(sup' (insert b s) h f) = ↑(f b ⊔ sup' s H f)
simp [WithBot.coe_sup]