case a
α : Type u_2
β : Type u_1
γ : Type ?u.522272
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b a : β
⊢ a ∈ erase (Finset.biUnion s f) b ↔ a ∈ Finset.biUnion s fun x => erase (f x) b
α : Type u_2
β : Type u_1
γ : Type ?u.522272
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b : β
⊢ erase (Finset.biUnion s f) b = Finset.biUnion s fun x => erase (f x) b
ext a
case a
α : Type u_2
β : Type u_1
γ : Type ?u.522272
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b a : β
⊢ (¬a = b ∧ ∃ a_1, a_1 ∈ s ∧ a ∈ f a_1) ↔ ∃ a_1, a_1 ∈ s ∧ ¬a = b ∧ a ∈ f a_1
case a
α : Type u_2
β : Type u_1
γ : Type ?u.522272
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b a : β
⊢ a ∈ erase (Finset.biUnion s f) b ↔ a ∈ Finset.biUnion s fun x => erase (f x) b
simp [Finset.mem_biUnion, iff_self_iff, exists_and_left, Finset.mem_erase]
no goals
case a
α : Type u_2
β : Type u_1
γ : Type ?u.522272
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b a : β
⊢ (¬a = b ∧ ∃ a_1, a_1 ∈ s ∧ a ∈ f a_1) ↔ ∃ a_1, a_1 ∈ s ∧ ¬a = b ∧ a ∈ f a_1
tauto