α : Type u_1
β : Type u_2
γ : Type ?u.90806
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ ∀ ⦃x : β⦄, x ≠ f a → ∀ (x_1 : α), x_1 ∈ s → f x_1 = x → ∃ a_4, (a_4 ≠ a ∧ a_4 ∈ s) ∧ f a_4 = x
α : Type u_1
β : Type u_2
γ : Type ?u.90806
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ erase (image f s) (f a) ⊆ image f (erase s a)
simp only [subset_iff, and_imp, exists_prop, mem_image, exists_imp, mem_erase]
α : Type u_1
β : Type u_2
γ : Type ?u.90806
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a x : α
hx : x ∈ s
hb : f x ≠ f a
⊢ ∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = f x
α : Type u_1
β : Type u_2
γ : Type ?u.90806
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ ∀ ⦃x : β⦄, x ≠ f a → ∀ (x_1 : α), x_1 ∈ s → f x_1 = x → ∃ a_4, (a_4 ≠ a ∧ a_4 ∈ s) ∧ f a_4 = x
rintro b hb x hx rfl
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.90806
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a x : α
hx : x ∈ s
hb : f x ≠ f a
⊢ ∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = f x
exact ⟨_, ⟨ne_of_apply_ne f hb, hx⟩, rfl⟩