α : Type u_2
β : Type u_1
γ : Type ?u.2249
f : α ↪ β
s : Finset α
b : β
⊢ (∃ a, a ∈ s.val ∧ ↑f a = b) ↔ ∃ a, a ∈ s ∧ ↑f a = b
α : Type u_2
β : Type u_1
γ : Type ?u.2249
f : α ↪ β
s : Finset α
b : β
⊢ (∃ a, a ∈ s.val ∧ ↑f a = b) ↔ ∃ a, a ∈ s ∧ ↑f a = b
simp only [exists_prop]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.2249
f : α ↪ β
s : Finset α
b : β
⊢ (∃ a, a ∈ s.val ∧ ↑f a = b) ↔ ∃ a, a ∈ s ∧ ↑f a = b
rfl