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

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

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

case mpr
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s
swap
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t
intro h
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
letI : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
case mp.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
lift t to Finset s using h
case mp.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x => x ∈ s) t) = image (f ∘ Subtype.val) t
case mp.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t
refine' ⟨t.map (Embedding.subtype _), map_subtype_subset _, _⟩
case mp.intro.a
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x => x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t
case mp.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x => x ∈ s) t) = image (f ∘ Subtype.val) t
ext y
no goals
case mp.intro.a
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  { prf := (_ : ∀ (y : β), y ∈ f '' s → ∃ y_1, (f ∘ Subtype.val) y_1 = y) }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x => x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t
simp
case mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(image f t) ⊆ f '' s
case mpr
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s
rintro ⟨t, ht, rfl⟩
case mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ f '' ↑t ⊆ f '' s
case mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(image f t) ⊆ f '' s
rw [coe_image]
no goals
case mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.140906
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ f '' ↑t ⊆ f '' s
exact Set.image_subset f ht