α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
haveI := hs.to_subtype
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ {t | Set.Finite t ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
refine' Countable.mono _ (countable_range fun t : Finset s => Subtype.val '' (t : Set s))
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set α
ht : Set.Finite t
hts : t ⊆ s
⊢ t ∈ range fun t => Subtype.val '' ↑t
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ {t | Set.Finite t ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t
rintro t ⟨ht, hts⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val t)
⊢ (fun x x_1 => x '' x_1) Subtype.val t ∈ range fun t => Subtype.val '' ↑t
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set α
ht : Set.Finite t
hts : t ⊆ s
⊢ t ∈ range fun t => Subtype.val '' ↑t
lift t to Set s using hts
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Finset ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val ↑t)
⊢ (fun x x_1 => x '' x_1) Subtype.val ↑t ∈ range fun t => Subtype.val '' ↑t
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val t)
⊢ (fun x x_1 => x '' x_1) Subtype.val t ∈ range fun t => Subtype.val '' ↑t
lift t to Finset s using ht.of_finite_image (Subtype.val_injective.injOn _)
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Finset ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val ↑t)
⊢ (fun x x_1 => x '' x_1) Subtype.val ↑t ∈ range fun t => Subtype.val '' ↑t
exact mem_range_self _