case a
α : Type u_2
β : Type u_1
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
b x : β
⊢ x ∈ pimage f s ↔ x ∈ image (fun x => Part.get (f ↑x) (_ : (f ↑x).Dom)) (attach (filter (fun x => (f x).Dom) s))
α : Type u_2
β : Type u_1
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
b : β
⊢ pimage f s = image (fun x => Part.get (f ↑x) (_ : (f ↑x).Dom)) (attach (filter (fun x => (f x).Dom) s))
ext x
case a
α : Type u_2
β : Type u_1
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
b x : β
⊢ (∃ a, a ∈ s ∧ ∃ h, Part.get (f a) h = x) ↔
    ∃ a hp hq, Part.get (f a) (_ : (f ↑{ val := a, property := (_ : a ∈ filter (fun x => (f x).Dom) s) }).Dom) = x
case a
α : Type u_2
β : Type u_1
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
b x : β
⊢ x ∈ pimage f s ↔ x ∈ image (fun x => Part.get (f ↑x) (_ : (f ↑x).Dom)) (attach (filter (fun x => (f x).Dom) s))
simp [Part.mem_eq, And.exists]
no goals
case a
α : Type u_2
β : Type u_1
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
b x : β
⊢ (∃ a, a ∈ s ∧ ∃ h, Part.get (f a) h = x) ↔
    ∃ a hp hq, Part.get (f a) (_ : (f ↑{ val := a, property := (_ : a ∈ filter (fun x => (f x).Dom) s) }).Dom) = x
simp only [←exists_prop]