no goals
𝕜 : Type ?u.12270
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
⊢ interedges r (Finset.biUnion s f) (Finset.biUnion t g) =
    Finset.biUnion (s ×ˢ t) fun ab => interedges r (f ab.fst) (g ab.snd)
simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]