[GOAL]
α : Type u_1
β : Type u_2
o : Part α
inst✝ : Decidable o.Dom
x : α
⊢ x ∈ toFinset o ↔ x ∈ o
[PROOFSTEP]
simp [toFinset]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Decidable none.Dom
⊢ toFinset none = ∅
[PROOFSTEP]
simp [toFinset]
[GOAL]
α : Type u_1
β : Type u_2
a : α
inst✝ : Decidable (some a).Dom
⊢ toFinset (some a) = {a}
[PROOFSTEP]
simp [toFinset]
[GOAL]
α : 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 : β
⊢ b ∈ pimage f s ↔ ∃ a, a ∈ s ∧ b ∈ f a
[PROOFSTEP]
simp [pimage]
[GOAL]
α : 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
[PROOFSTEP]
ext
[GOAL]
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
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : 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 : β
h₁ : s = t
h₂ : ∀ (x : α), x ∈ t → f x = g x
⊢ pimage f s = pimage g t
[PROOFSTEP]
subst s
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
t : Finset α
b : β
h₂ : ∀ (x : α), x ∈ t → f x = g x
⊢ pimage f t = pimage g t
[PROOFSTEP]
ext y
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
t : Finset α
b : β
h₂ : ∀ (x : α), x ∈ t → f x = g x
y : β
⊢ y ∈ pimage f t ↔ y ∈ pimage g t
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_pimage, ← exists_prop, h₂]
[GOAL]
α : 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 : β
⊢ pimage f s = image (fun x => Part.get (f ↑x) (_ : (f ↑x).Dom)) (attach (filter (fun x => (f x).Dom) s))
[PROOFSTEP]
ext x
[GOAL]
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 x : β
⊢ x ∈ pimage f s ↔ x ∈ image (fun x => Part.get (f ↑x) (_ : (f ↑x).Dom)) (attach (filter (fun x => (f x).Dom) s))
[PROOFSTEP]
simp [Part.mem_eq, And.exists]
  -- Porting note: `←exists_prop` required because `∃ x ∈ s, p x` is defined differently
[GOAL]
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 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
[PROOFSTEP]
simp only [← exists_prop]
[GOAL]
α : 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 : β
inst✝ : DecidableEq α
⊢ ↑(pimage f (s ∪ t)) = ↑(pimage f s ∪ pimage f t)
[PROOFSTEP]
simp only [coe_pimage, coe_union, ← PFun.image_union]
[GOAL]
α : 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 : β
⊢ pimage f ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
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 a✝ : β
⊢ a✝ ∈ pimage f ∅ ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : 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 : β
t : Finset β
⊢ pimage f s ⊆ t ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ f x → y ∈ t
[PROOFSTEP]
simp [subset_iff, @forall_swap _ β]
[GOAL]
α : 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 : β
inst✝ : DecidableEq α
⊢ pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t
[PROOFSTEP]
simp only [← coe_subset, coe_pimage, coe_inter, PFun.image_inter]
