case a
𝕜 : Type ?u.10244
ι : Type u_2
κ : Type ?u.10250
α : Type u_1
β : Type u_3
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 s (Finset.biUnion t f) ↔ a ∈ Finset.biUnion t fun b => interedges r s (f b)
𝕜 : Type ?u.10244
ι : Type u_2
κ : Type ?u.10250
α : Type u_1
β : Type u_3
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 s (Finset.biUnion t f) = Finset.biUnion t fun b => interedges r s (f b)
ext a
case a
𝕜 : Type ?u.10244
ι : Type u_2
κ : Type ?u.10250
α : Type u_1
β : Type u_3
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.fst ∈ s ∧ (∃ a_1, a_1 ∈ t ∧ a.snd ∈ f a_1) ∧ r a.fst a.snd ↔
    ∃ a_1, a_1 ∈ t ∧ a.fst ∈ s ∧ a.snd ∈ f a_1 ∧ r a.fst a.snd
case a
𝕜 : Type ?u.10244
ι : Type u_2
κ : Type ?u.10250
α : Type u_1
β : Type u_3
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 s (Finset.biUnion t f) ↔ a ∈ Finset.biUnion t fun b => interedges r s (f b)
simp only [mem_interedges_iff, mem_biUnion]
no goals
case a
𝕜 : Type ?u.10244
ι : Type u_2
κ : Type ?u.10250
α : Type u_1
β : Type u_3
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.fst ∈ s ∧ (∃ a_1, a_1 ∈ t ∧ a.snd ∈ f a_1) ∧ r a.fst a.snd ↔
    ∃ a_1, a_1 ∈ t ∧ a.fst ∈ s ∧ a.snd ∈ f a_1 ∧ r a.fst a.snd
exact ⟨fun ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩ ↦ ⟨x₂, x₃, x₁, x₄, x₅⟩,
  fun ⟨x₂, x₃, x₁, x₄, x₅⟩ ↦ ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩⟩