α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ f a = b) ∧ p b ↔ ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (image f s) ↔ b ∈ image f (filter (p ∘ f) s)
simp only [mem_filter, mem_image, exists_prop]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ f a = b) ∧ p b ↔ ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b
exact
  ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩,
   by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = f x
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ f a = b) ∧ p b → ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b
rintro ⟨⟨x, h1, rfl⟩, h2⟩
no goals
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = f x
exact ⟨x, ⟨h1, h2⟩, rfl⟩
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : (p ∘ f) x
⊢ (∃ a, a ∈ s ∧ f a = f x) ∧ p (f x)
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b) → (∃ a, a ∈ s ∧ f a = b) ∧ p b
rintro ⟨x, ⟨h1, h2⟩, rfl⟩
no goals
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.84280
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : (p ∘ f) x
⊢ (∃ a, a ∈ s ∧ f a = f x) ∧ p (f x)
exact ⟨⟨x, h1, rfl⟩, h2⟩