case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ ⊆ erase (image b univ) k

case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ erase (image b univ) k ⊆ image (fun i => b ↑i) univ
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ = erase (image b univ) k
apply subset_antisymm
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ (x : { a // b a ≠ k }), x ∈ univ → b ↑x ∈ erase (image b univ) k
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ ⊆ erase (image b univ) k
rw [image_subset_iff]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : { a // b a ≠ k }
a✝ : i ∈ univ
⊢ b ↑i ∈ erase (image b univ) k
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ (x : { a // b a ≠ k }), x ∈ univ → b ↑x ∈ erase (image b univ) k
intro i _
no goals
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : { a // b a ≠ k }
a✝ : i ∈ univ
⊢ b ↑i ∈ erase (image b univ) k
apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ i ∈ image (fun i => b ↑i) univ
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ erase (image b univ) k ⊆ image (fun i => b ↑i) univ
intro i hi
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ i ∈ image (fun i => b ↑i) univ
rw [mem_image]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ erase (image b univ) k
⊢ ∃ a_1, a_1 ∈ univ ∧ b ↑a_1 = b a
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
subst ha
no goals
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ erase (image b univ) k
⊢ ∃ a_1, a_1 ∈ univ ∧ b ↑a_1 = b a
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩