α : 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
α : 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
subst s
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
α : 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
ext y
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
t : Finset α
b : β
h₂ : ∀ (x : α), x ∈ t → f x = g x
y : β
⊢ y ∈ pimage f t ↔ y ∈ pimage g t
simp (config := { contextual := true }) only [mem_pimage, ←exists_prop, h₂]