no goals
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ card s' ≤ card (Finset.biUnion s' fun a' => t ↑a')
classical
  rw [← card_image_of_injective s' Subtype.coe_injective]
  convert ht (s'.image fun z => z.1) using 1
  apply congr_arg
  ext y
  simp
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ card (image (fun a => ↑a) s') ≤ card (Finset.biUnion s' fun a' => t ↑a')
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ card s' ≤ card (Finset.biUnion s' fun a' => t ↑a')
rw [← card_image_of_injective s' Subtype.coe_injective]
case h.e'_4
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ card (Finset.biUnion s' fun a' => t ↑a') = card (Finset.biUnion (image (fun z => ↑z) s') t)
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ card (image (fun a => ↑a) s') ≤ card (Finset.biUnion s' fun a' => t ↑a')
convert ht (s'.image fun z => z.1) using 1
case h.e'_4.h
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ (Finset.biUnion s' fun a' => t ↑a') = Finset.biUnion (image (fun z => ↑z) s') t
case h.e'_4
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ card (Finset.biUnion s' fun a' => t ↑a') = card (Finset.biUnion (image (fun z => ↑z) s') t)
apply congr_arg
case h.e'_4.h.a
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
y : α
⊢ (y ∈ Finset.biUnion s' fun a' => t ↑a') ↔ y ∈ Finset.biUnion (image (fun z => ↑z) s') t
case h.e'_4.h
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
⊢ (Finset.biUnion s' fun a' => t ↑a') = Finset.biUnion (image (fun z => ↑z) s') t
ext y
no goals
case h.e'_4.h.a
ι✝ : Type u
α : Type v
inst✝¹ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝ : Fintype ι✝
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
s' : Finset ↑↑s
y : α
⊢ (y ∈ Finset.biUnion s' fun a' => t ↑a') ↔ y ∈ Finset.biUnion (image (fun z => ↑z) s') t
simp