case a
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
f✝ g : α →. β
inst✝² : (x : α) → Decidable (f✝ x).Dom
inst✝¹ : (x : α) → Decidable (g x).Dom
s✝ t : Finset α
b : β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
a✝ : β
⊢ a✝ ∈ pimage (fun x => Part.some (f x)) s ↔ a✝ ∈ image f s
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
f✝ g : α →. β
inst✝² : (x : α) → Decidable (f✝ x).Dom
inst✝¹ : (x : α) → Decidable (g x).Dom
s✝ t : Finset α
b : β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
⊢ pimage (fun x => Part.some (f x)) s = image f s
ext
no goals
case a
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
f✝ g : α →. β
inst✝² : (x : α) → Decidable (f✝ x).Dom
inst✝¹ : (x : α) → Decidable (g x).Dom
s✝ t : Finset α
b : β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
a✝ : β
⊢ a✝ ∈ pimage (fun x => Part.some (f x)) s ↔ a✝ ∈ image f s
simp [eq_comm]