case a
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (Finset.biUnion s f) ↔ b ∈ Finset.biUnion s fun a => filter p (f a)
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (Finset.biUnion s f) = Finset.biUnion s fun a => filter p (f a)
ext b
case a
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b ↔ ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
case a
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (Finset.biUnion s f) ↔ b ∈ Finset.biUnion s fun a => filter p (f a)
simp only [mem_biUnion, exists_prop, mem_filter]
case a.mp
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b → ∃ a, a ∈ s ∧ b ∈ f a ∧ p b

case a.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a ∧ p b) → (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b
case a
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b ↔ ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
constructor
case a.mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
hb : p b
a : α
ha : a ∈ s
hba : b ∈ f a
⊢ ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
case a.mp
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b → ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
rintro ⟨⟨a, ha, hba⟩, hb⟩
no goals
case a.mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
hb : p b
a : α
ha : a ∈ s
hba : b ∈ f a
⊢ ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
exact ⟨a, ha, hba, hb⟩
case a.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
a : α
ha : a ∈ s
hba : b ∈ f a
hb : p b
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b
case a.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a ∧ p b) → (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b
rintro ⟨a, ha, hba, hb⟩
no goals
case a.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.520534
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
a : α
ha : a ∈ s
hba : b ∈ f a
hb : p b
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b
exact ⟨⟨a, ha, hba⟩, hb⟩