α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
k : ℕ
this : Infinite ↑s
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = k
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
k : ℕ
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = k
have := hs.to_subtype
case intro.intro
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = Finset.card t'
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
k : ℕ
this : Infinite ↑s
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = k
obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k
case intro.intro
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.ncard (Subtype.val '' ↑t') = Finset.card t'
case intro.intro
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = Finset.card t'
refine' ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), _⟩
case intro.intro
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.ncard ↑t' = Finset.card t'
case intro.intro
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.ncard (Subtype.val '' ↑t') = Finset.card t'
rw [ncard_image_ofInjective _ Subtype.coe_injective]
no goals
case intro.intro
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.ncard ↑t' = Finset.card t'
simp
no goals
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Subtype.val '' ↑t' ⊆ s
simp
no goals
α : Type u_1
β : Type ?u.133509
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.Finite ↑t'
simp