ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
choose s h1s h2s using hC
case intro
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
val✝ : Encodable (ι → ℕ)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
cases nonempty_encodable (ι → ℕ)
case intro
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
case intro
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
val✝ : Encodable (ι → ℕ)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
case intro
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ (⋃ (n : ℕ), (fun n => Set.pi univ fun i => s i (e n i)) n) = univ
case intro
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
refine' ⟨fun n => Set.pi univ fun i => s i (e n i), fun n =>
  mem_image_of_mem _ fun i _ => h1s i _, _⟩
no goals
case intro
ι : Type u_2
ι' : Type ?u.427415
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), (⋃ (n : ℕ), s i n) = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ (⋃ (n : ℕ), (fun n => Set.pi univ fun i => s i (e n i)) n) = univ
simp_rw [(surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
  iUnion_univ_pi s, h2s, pi_univ]