no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.142048
γ : Type ?u.142051
ι : Sort ?u.142054
ι' : Sort ?u.142057
κ : ι → Sort ?u.142062
κ' : ι' → Sort ?u.142067
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b✝ : α
f : β → α
a b : β
⊢ (⨅ (x : β) (_ : x ∈ {a, b}), f x) = f a ⊓ f b
rw [iInf_insert, iInf_singleton]