case a
𝕜 : Type ?u.8631
ι : Type u_1
κ : Type ?u.8637
α : Type u_3
β : Type u_2
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 α
a✝ : α × β
⊢ a✝ ∈ interedges r (Finset.biUnion s f) t ↔ a✝ ∈ Finset.biUnion s fun a => interedges r (f a) t
𝕜 : Type ?u.8631
ι : Type u_1
κ : Type ?u.8637
α : Type u_3
β : Type u_2
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 α
⊢ interedges r (Finset.biUnion s f) t = Finset.biUnion s fun a => interedges r (f a) t
ext
no goals
case a
𝕜 : Type ?u.8631
ι : Type u_1
κ : Type ?u.8637
α : Type u_3
β : Type u_2
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 α
a✝ : α × β
⊢ a✝ ∈ interedges r (Finset.biUnion s f) t ↔ a✝ ∈ Finset.biUnion s fun a => interedges r (f a) t
simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]