F : Type ?u.263099
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.263111
κ : Type ?u.263114
inst✝ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f✝ : β → α
s : Finset γ
f : γ ↪ β
g : β → α
hs : Finset.Nonempty (map f s)
hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)
⊢ sup s ((WithBot.some ∘ g) ∘ ↑f) = sup s (WithBot.some ∘ g ∘ ↑f)
F : Type ?u.263099
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.263111
κ : Type ?u.263114
inst✝ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f✝ : β → α
s : Finset γ
f : γ ↪ β
g : β → α
hs : Finset.Nonempty (map f s)
hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)
⊢ sup' (map f s) hs g = sup' s hs' (g ∘ ↑f)
rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']
no goals
F : Type ?u.263099
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.263111
κ : Type ?u.263114
inst✝ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f✝ : β → α
s : Finset γ
f : γ ↪ β
g : β → α
hs : Finset.Nonempty (map f s)
hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)
⊢ sup s ((WithBot.some ∘ g) ∘ ↑f) = sup s (WithBot.some ∘ g ∘ ↑f)
rfl