-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
    powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding :=
  ext fun t => by
    simp only [card_map, mem_powersetCard, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]
    constructor
    · classical
      intro h
      have : map f (filter (fun x => (f x ∈ t)) s) = t

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f (filter (fun x => f x ∈ t) s) = t
⊢ filter (fun x => f x ∈ t) s ⊆ s ∧ n = n

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
x : β
⊢ (∃ a, (a ∈ s ∧ f a ∈ t) ∧ f a = x) ↔ x ∈ t

Tactic:
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⟩⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ #t = n

Tactic:
rintro ⟨a, ⟨has, rfl⟩, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ (mapEmbedding f).toEmbedding a ⊆ map f s ∧ #((mapEmbedding f).toEmbedding a) = #a

Proof state:
case h
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
x : β
⊢ x ∈ map f (filter (fun x => f x ∈ t) s) ↔ x ∈ t

Tactic:
simp only [mem_map, mem_filter, decide_eq_true_eq]

Result:
case h
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
x : β
⊢ (∃ a, (a ∈ s ∧ f a ∈ t) ∧ f a = x) ↔ x ∈ t

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f (filter (fun x => f x ∈ t) s) = t
⊢ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
refine ⟨_, ?_, this⟩

Result:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f (filter (fun x => f x ∈ t) s) = t
⊢ filter (fun x => f x ∈ t) s ⊆ s ∧ #(filter (fun x => f x ∈ t) s) = n

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
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

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ #(map f a) = #a

Tactic:
simp [has]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ∈ powersetCard n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetCard n s)

Tactic:
simp only [card_map, mem_powersetCard, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]

Result:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

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

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f (filter (fun x => f x ∈ t) s) = t
⊢ filter (fun x => f x ∈ t) s ⊆ s ∧ #(filter (fun x => f x ∈ t) s) = n

Tactic:
rw [← card_map f, this, h.2]

Result:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f (filter (fun x => f x ∈ t) s) = t
⊢ filter (fun x => f x ∈ t) s ⊆ s ∧ n = n

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ (mapEmbedding f) a ⊆ map f s ∧ #((mapEmbedding f) a) = #a

Tactic:
rw [mapEmbedding_apply]

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ #(map f a) = #a

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ (mapEmbedding f).toEmbedding a ⊆ map f s ∧ #((mapEmbedding f).toEmbedding a) = #a

Tactic:
dsimp [RelEmbedding.coe_toEmbedding]

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ (mapEmbedding f) a ⊆ map f s ∧ #((mapEmbedding f) a) = #a

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
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⟩⟩

Result:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f (filter (fun x => f x ∈ t) s) = t
⊢ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ map f (filter (fun x => f x ∈ t) s) = t

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
x : β
⊢ x ∈ map f (filter (fun x => f x ∈ t) s) ↔ x ∈ t