F : Type ?u.17780
α : Type u_2
β : Type u_1
γ : Type ?u.17789
ι : Type ?u.17792
κ : Type ?u.17795
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ sup s₁ f = sup s₁ g
F : Type ?u.17780
α : Type u_2
β : Type u_1
γ : Type ?u.17789
ι : Type ?u.17792
κ : Type ?u.17795
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ sup s₁ f = sup s₂ g
subst hs
no goals
F : Type ?u.17780
α : Type u_2
β : Type u_1
γ : Type ?u.17789
ι : Type ?u.17792
κ : Type ?u.17795
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ sup s₁ f = sup s₁ g
exact Finset.fold_congr hfg