α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n ↔ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ∈ powersetLen n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetLen n s)
simp only [card_map, mem_powersetLen, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t

case mpr
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n ↔ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
constructor
case mpr
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t

case mpr
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
. classical
  intro h
  have : map f (filter (fun x => (f x ∈ t)) s) = t := by
    ext x
    simp only [mem_map, mem_filter, decide_eq_true_eq]
    exact ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂,
      fun hx => let ⟨y, hy⟩ := mem_map.1 (h.1 hx); ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
  refine' ⟨_, _, this⟩
  rw [← card_map f, this, h.2]; simp
no goals
case mpr
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
. rintro ⟨a, ⟨has, rfl⟩, rfl⟩
  dsimp [RelEmbedding.coe_toEmbedding]
  rw [mapEmbedding_apply]
  simp [has]
no goals
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
classical
intro h
have : map f (filter (fun x => (f x ∈ t)) s) = t := by
  ext x
  simp only [mem_map, mem_filter, decide_eq_true_eq]
  exact ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂,
    fun hx => let ⟨y, hy⟩ := mem_map.1 (h.1 hx); ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
refine' ⟨_, _, this⟩
rw [← card_map f, this, h.2]; simp
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
intro h
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
have : map f (filter (fun x => (f x ∈ t)) s) = t := by
  ext x
  simp only [mem_map, mem_filter, decide_eq_true_eq]
  exact ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂,
    fun hx => let ⟨y, hy⟩ := mem_map.1 (h.1 hx); ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ card (filter (fun x => ↑f x ∈ t) s) = n
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
refine' ⟨_, _, this⟩
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ n = n
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ card (filter (fun x => ↑f x ∈ t) s) = n
rw [← card_map f, this, h.2]
no goals
case mp
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ n = n
simp
case a
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ x ∈ map f (filter (fun x => ↑f x ∈ t) s) ↔ x ∈ t
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ map f (filter (fun x => ↑f x ∈ t) s) = t
ext x
case a
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ (∃ a, (a ∈ s ∧ ↑f a ∈ t) ∧ ↑f a = x) ↔ x ∈ t
case a
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ x ∈ map f (filter (fun x => ↑f x ∈ t) s) ↔ x ∈ t
simp only [mem_map, mem_filter, decide_eq_true_eq]
no goals
case a
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ (∃ a, (a ∈ s ∧ ↑f a ∈ t) ∧ ↑f a = x) ↔ x ∈ t
exact ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂,
  fun hx => let ⟨y, hy⟩ := mem_map.1 (h.1 hx); ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
case mpr.intro.intro.intro
α : Type u_2
s✝ t : Finset α
β : Type u_1
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f).toEmbedding a ⊆ map f s ∧ card (↑(mapEmbedding f).toEmbedding a) = card a
case mpr
α : Type u_2
s✝ t✝ : Finset α
β : Type u_1
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
rintro ⟨a, ⟨has, rfl⟩, rfl⟩
case mpr.intro.intro.intro
α : Type u_2
s✝ t : Finset α
β : Type u_1
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f) a ⊆ map f s ∧ card (↑(mapEmbedding f) a) = card a
case mpr.intro.intro.intro
α : Type u_2
s✝ t : Finset α
β : Type u_1
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f).toEmbedding a ⊆ map f s ∧ card (↑(mapEmbedding f).toEmbedding a) = card a
dsimp [RelEmbedding.coe_toEmbedding]
case mpr.intro.intro.intro
α : Type u_2
s✝ t : Finset α
β : Type u_1
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ card (map f a) = card a
case mpr.intro.intro.intro
α : Type u_2
s✝ t : Finset α
β : Type u_1
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f) a ⊆ map f s ∧ card (↑(mapEmbedding f) a) = card a
rw [mapEmbedding_apply]
no goals
case mpr.intro.intro.intro
α : Type u_2
s✝ t : Finset α
β : Type u_1
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ card (map f a) = card a
simp [has]