no goals
F : Type ?u.182498
α : Type u_3
β : Type ?u.182504
γ : Type ?u.182507
ι : Type u_1
κ : Type u_2
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t✝ : Finset κ
f✝ : ι → α
g✝ : κ → α
a : α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
⊢ sup s f ⊓ sup t g = sup (s ×ˢ t) fun i => f i.fst ⊓ g i.snd
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]