-- Mathlib/Data/Fintype/Sum.lean
theorem image_subtype_univ_ssubset_image_univ [Fintype α] [DecidableEq β] (k : β) (b : α → β)
    (hk : k ∈ Finset.image b univ) (p : β → Prop) [DecidablePred p] (hp : ¬p k) :
    image (fun i : { a // p (b a) } => b ↑i) univ ⊂ image b univ

Proof state:
case left.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
y : { a // p (b a) }
left✝ : y ∈ univ
hy : b ↑y = x
⊢ x ∈ image b univ

Tactic:
exact hy ▸ mem_image_of_mem b (mem_univ (y : α))

Result:
no goals

Proof state:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : ∃ a ∈ univ, b ↑a = b k'
⊢ False

Tactic:
rcases this with ⟨j, _, hj'⟩

Result:
case right.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝¹ : k' ∈ univ
hp : ¬p (b k')
j : { a // p (b a) }
left✝ : j ∈ univ
hj' : b ↑j = b k'
⊢ False

Proof state:
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊆ image b univ

Tactic:
intro x hx

Result:
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
⊢ x ∈ image b univ

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊂ image b univ

Tactic:
constructor

Result:
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊆ image b univ

case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ ¬image b univ ⊆ image (fun i => b ↑i) univ

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ ¬image b univ ⊆ image (fun i => b ↑i) univ

Tactic:
intro h

Result:
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False

Proof state:
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
⊢ x ∈ image b univ

Tactic:
rcases mem_image.1 hx with ⟨y, _, hy⟩

Result:
case left.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
y : { a // p (b a) }
left✝ : y ∈ univ
hy : b ↑y = x
⊢ x ∈ image b univ

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : ∃ a ∈ univ, b a = k
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False

Tactic:
rcases hk with ⟨k', _, hk'⟩

Result:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hk' : b k' = k
⊢ False

Proof state:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
⊢ False

Tactic:
have := h (mem_image_of_mem b (mem_univ k'))

Result:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : b k' ∈ image (fun i => b ↑i) univ
⊢ False

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False

Tactic:
rw [mem_image] at hk

Result:
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : ∃ a ∈ univ, b a = k
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False

Proof state:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : b k' ∈ image (fun i => b ↑i) univ
⊢ False

Tactic:
rw [mem_image] at this

Result:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : ∃ a ∈ univ, b ↑a = b k'
⊢ False

Proof state:
case right.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝¹ : k' ∈ univ
hp : ¬p (b k')
j : { a // p (b a) }
left✝ : j ∈ univ
hj' : b ↑j = b k'
⊢ False

Tactic:
exact hp (hj' ▸ j.2)

Result:
no goals

Proof state:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hk' : b k' = k
⊢ False

Tactic:
subst hk'

Result:
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
⊢ False