case a
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ a✝ ∈ Finset.biUnion (Finset.biUnion s f) g ↔ a✝ ∈ Finset.biUnion s fun a => Finset.biUnion (f a) g
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ Finset.biUnion (Finset.biUnion s f) g = Finset.biUnion s fun a => Finset.biUnion (f a) g
ext
case a
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, (∃ a_1, a_1 ∈ s ∧ a ∈ f a_1) ∧ a✝ ∈ g a) ↔ ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ f a ∧ a✝ ∈ g a_1
case a
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ a✝ ∈ Finset.biUnion (Finset.biUnion s f) g ↔ a✝ ∈ Finset.biUnion s fun a => Finset.biUnion (f a) g
simp only [Finset.mem_biUnion, exists_prop]
case a
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a x, x ∈ s ∧ a ∈ f x ∧ a✝ ∈ g a) ↔ ∃ a x, a ∈ s ∧ x ∈ f a ∧ a✝ ∈ g x
case a
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, (∃ a_1, a_1 ∈ s ∧ a ∈ f a_1) ∧ a✝ ∈ g a) ↔ ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ f a ∧ a✝ ∈ g a_1
simp_rw [← exists_and_right, ← exists_and_left, and_assoc]
no goals
case a
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a x, x ∈ s ∧ a ∈ f x ∧ a✝ ∈ g a) ↔ ∃ a x, a ∈ s ∧ x ∈ f a ∧ a✝ ∈ g x
rw [exists_comm]