α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b✝ c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
b : β
⊢ b ∈ image f (erase s a) → b ∈ erase (image f s) (f a)
α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ image f (erase s a) = erase (image f s) (f a)
refine' (erase_image_subset_image_erase _ _ _).antisymm' fun b => _
α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b✝ c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
b : β
⊢ (∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = b) → b ≠ f a ∧ ∃ a, a ∈ s ∧ f a = b
α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b✝ c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
b : β
⊢ b ∈ image f (erase s a) → b ∈ erase (image f s) (f a)
simp only [mem_image, exists_prop, mem_erase]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a a' : α
haa' : a' ≠ a
ha' : a' ∈ s
⊢ f a' ≠ f a ∧ ∃ a, a ∈ s ∧ f a = f a'
α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b✝ c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
b : β
⊢ (∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = b) → b ≠ f a ∧ ∃ a, a ∈ s ∧ f a = b
rintro ⟨a', ⟨haa', ha'⟩, rfl⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.92014
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a a' : α
haa' : a' ≠ a
ha' : a' ∈ s
⊢ f a' ≠ f a ∧ ∃ a, a ∈ s ∧ f a = f a'
exact ⟨hf.ne haa', a', ha', rfl⟩