[GOAL]
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α ⊕ β)
[PROOFSTEP]
rcases exists_injective_nat α with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α ⊕ β)
[PROOFSTEP]
rcases exists_injective_nat β with ⟨g, hg⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α ⊕ β)
[PROOFSTEP]
exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sum_map hg).countable
[GOAL]
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α × β)
[PROOFSTEP]
rcases exists_injective_nat α with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α × β)
[PROOFSTEP]
rcases exists_injective_nat β with ⟨g, hg⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α × β)
[PROOFSTEP]
exact (Nat.pairEquiv.injective.comp <| hf.Prod_map hg).countable
[GOAL]
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Sigma π)
[PROOFSTEP]
rcases exists_injective_nat α with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
⊢ Countable (Sigma π)
[PROOFSTEP]
choose g hg using fun a => exists_injective_nat (π a)
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
g : (a : α) → π a → ℕ
hg : ∀ (a : α), Injective (g a)
⊢ Countable (Sigma π)
[PROOFSTEP]
exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
have : ∀ n, Countable (Fin n → ℕ) := by
  intro n
  induction' n with n ihn
  · change Countable (Fin 0 → ℕ); infer_instance
  · haveI := ihn
    exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Equiv.piFinSucc _ _).symm
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ ∀ (n : ℕ), Countable (Fin n → ℕ)
[PROOFSTEP]
intro n
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
⊢ Countable (Fin n → ℕ)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Fin Nat.zero → ℕ)
[PROOFSTEP]
change Countable (Fin 0 → ℕ)
[GOAL]
case zero
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Fin 0 → ℕ)
[PROOFSTEP]
infer_instance
[GOAL]
case succ
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
ihn : Countable (Fin n → ℕ)
⊢ Countable (Fin (Nat.succ n) → ℕ)
[PROOFSTEP]
haveI := ihn
[GOAL]
case succ
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
ihn this : Countable (Fin n → ℕ)
⊢ Countable (Fin (Nat.succ n) → ℕ)
[PROOFSTEP]
exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Equiv.piFinSucc _ _).symm
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
[GOAL]
case intro.intro
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
have f := fun a => (nonempty_embedding_nat (π a)).some
[GOAL]
case intro.intro
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
f : (a : α) → π a ↪ ℕ
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
exact ((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable
