case a
α : Type u_1
β : Type u_2
γ : Type ?u.68613
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s
α : Type u_1
β : Type u_2
γ : Type ?u.68613
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
⊢ image f s = image g s
ext
case a
α : Type u_1
β : Type u_2
γ : Type ?u.68613
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ x x_1, f x = a✝) ↔ ∃ x x_1, g x = a✝
case a
α : Type u_1
β : Type u_2
γ : Type ?u.68613
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s
simp_rw [mem_image, ← bex_def]
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.68613
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ x x_1, f x = a✝) ↔ ∃ x x_1, g x = a✝
exact bex_congr fun x hx => by rw [h hx]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.68613
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
x : α
hx : x ∈ s
⊢ f x = a✝ ↔ g x = a✝
rw [h hx]