-- Mathlib/Data/Finset/Image.lean
theorem subset_set_image_iff [DecidableEq β] {s : Set α} {t : Finset β} {f : α → β} :
    ↑t ⊆ f '' s ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ s'.image f = t

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(image f t) ⊆ f '' s

Tactic:
rw [coe_image]

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ f '' ↑t ⊆ f '' s

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x => x ∈ s) t) = image (f ∘ Subtype.val) t

Tactic:
ext y

Result:
case mp.intro.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x => x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s

Tactic:
rintro ⟨t, ht, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(image f t) ⊆ f '' s

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t

Tactic:
refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x => x ∈ s) t) = image (f ∘ Subtype.val) t

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
letI : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Proof state:
case mp.intro.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x => x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ f '' ↑t ⊆ f '' s

Tactic:
exact Set.image_subset f ht

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
lift t to Finset s using h

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t

case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s