F : Type ?u.108630
α : Type u_2
β : Type u_1
γ : Type ?u.108639
ι : Type ?u.108642
κ : Type ?u.108645
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s s₁ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ inf s₁ f = inf s₁ g
F : Type ?u.108630
α : Type u_2
β : Type u_1
γ : Type ?u.108639
ι : Type ?u.108642
κ : Type ?u.108645
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ inf s₁ f = inf s₂ g
subst hs
no goals
F : Type ?u.108630
α : Type u_2
β : Type u_1
γ : Type ?u.108639
ι : Type ?u.108642
κ : Type ?u.108645
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s s₁ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ inf s₁ f = inf s₁ g
exact Finset.fold_congr hfg