case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
⊢ ∃ f, s = range f
rcases hc.exists_surjective hs with ⟨f, hf⟩
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f
refine' ⟨(↑) ∘ f, _⟩
no goals
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)
rw [hf.range_comp, Subtype.range_coe]