-- Mathlib/Data/Fintype/Sum.lean
theorem image_subtype_ne_univ_eq_image_erase [Fintype α] [DecidableEq β] (k : β) (b : α → β) :
    image (fun i : { a // b a ≠ k } => b ↑i) univ = (image b univ).erase k

Proof state:
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ (image b univ).erase k
⊢ ∃ a_1 ∈ univ, b ↑a_1 = b a

Tactic:
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩

Result:
no goals

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

Tactic:
intro i hi

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

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

Tactic:
rw [mem_image]

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ ∃ a ∈ univ, b ↑a = i

Proof state:
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a ∈ univ, b ↑a = i

Tactic:
subst ha

Result:
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ (image b univ).erase k
⊢ ∃ a_1 ∈ univ, b ↑a_1 = b a

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : { a // b a ≠ k }
a✝ : i ∈ univ
⊢ b ↑i ∈ (image b univ).erase k

Tactic:
apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ x ∈ univ, b ↑x ∈ (image b univ).erase k

Tactic:
intro i _

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : { a // b a ≠ k }
a✝ : i ∈ univ
⊢ b ↑i ∈ (image b univ).erase k

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ ∃ a ∈ univ, b ↑a = i

Tactic:
rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩

Result:
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a ∈ univ, b ↑a = i

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

Tactic:
apply subset_antisymm

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

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

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

Tactic:
rw [image_subset_iff]

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ x ∈ univ, b ↑x ∈ (image b univ).erase k