/-
Copyright (c) 2022 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module data.countable.basic
! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Equiv.Nat
import Mathlib.Logic.Equiv.Fin
import Mathlib.Data.Countable.Defs

/-!
# Countable types

In this file we provide basic instances of the `Countable` typeclass defined elsewhere.
-/


universe u v w

open Function

instance: Countable ℤ
instance : Countable: Sort ?u.2 → Prop
Countable ℤ: Type
ℤ :=
  Countable.of_equiv: ∀ {β : Sort ?u.4} (α : Sort ?u.5) [inst : Countable α], α ≃ β → Countable β
Countable.of_equiv ℕ: Type
ℕ Equiv.intEquivNat: ℤ ≃ ℕ
Equiv.intEquivNat.symm: {α : Sort ?u.10} → {β : Sort ?u.9} → α ≃ β → β ≃ α
symm

/-!
### Definition in terms of `Function.Embedding`
-/

section Embedding

variable {α: Sort u
α : Sort u: Type u
SortSort u: Type u
 u} {β: Sort v
β : Sort v: Type v
SortSort v: Type v
 v}

theorem countable_iff_nonempty_embedding: Countable α ↔ Nonempty (α ↪ ℕ)
countable_iff_nonempty_embedding : Countable: Sort ?u.32 → Prop
Countable α: Sort u
α ↔ Nonempty: Sort ?u.33 → Prop
Nonempty (α: Sort u
α ↪ ℕ: Type
ℕ) :=
  ⟨fun ⟨⟨f: α → ℕ
f, hf: Injective f
hf⟩⟩ => ⟨⟨f: α → ℕ
f, hf: Injective f
hf⟩⟩, fun ⟨f: α ↪ ℕ
f⟩ => ⟨⟨f: α ↪ ℕ
f, f: α ↪ ℕ
f.2: ∀ {α : Sort ?u.357} {β : Sort ?u.356} (self : α ↪ β), Injective self.toFun
2⟩⟩⟩
#align countable_iff_nonempty_embedding countable_iff_nonempty_embedding: ∀ {α : Sort u}, Countable α ↔ Nonempty (α ↪ ℕ)
countable_iff_nonempty_embedding

theorem nonempty_embedding_nat: ∀ (α : Sort u_1) [inst : Countable α], Nonempty (α ↪ ℕ)
nonempty_embedding_nat (α: Sort u_1
α) [Countable: Sort ?u.435 → Prop
Countable α: ?m.432
α] : Nonempty: Sort ?u.438 → Prop
Nonempty (α: ?m.432
α ↪ ℕ: Type
ℕ) :=
  countable_iff_nonempty_embedding: ∀ {α : Sort ?u.444}, Countable α ↔ Nonempty (α ↪ ℕ)
countable_iff_nonempty_embedding.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 ‹_›
#align nonempty_embedding_nat nonempty_embedding_nat: ∀ (α : Sort u_1) [inst : Countable α], Nonempty (α ↪ ℕ)
nonempty_embedding_nat

protected theorem Function.Embedding.countable: ∀ {α : Sort u} {β : Sort v} [inst : Countable β], (α ↪ β) → Countable α
Function.Embedding.countable [Countable: Sort ?u.464 → Prop
Countable β: Sort v
β] (f: α ↪ β
f : α: Sort u
α ↪ β: Sort v
β) : Countable: Sort ?u.471 → Prop
Countable α: Sort u
α :=
  f: α ↪ β
f.injective: ∀ {α : Sort ?u.475} {β : Sort ?u.476} (f : α ↪ β), Injective ↑f
injective.countable: ∀ {α : Sort ?u.482} {β : Sort ?u.481} [inst : Countable β] {f : α → β}, Injective f → Countable α
countable
#align function.embedding.countable Function.Embedding.countable: ∀ {α : Sort u} {β : Sort v} [inst : Countable β], (α ↪ β) → Countable α
Function.Embedding.countable

end Embedding

/-!
### Operations on `Type _`s
-/

section type

variable {α: Type u
α : Type u: Type (u+1)
Type u} {β: Type v
β : Type v: Type (v+1)
Type v} {π: α → Type w
π : α: Type u
α → Type w: Type (w+1)
Type w}

instance: ∀ {α : Type u} {β : Type v} [inst : Countable α] [inst : Countable β], Countable (α ⊕ β)
instance [Countable: Sort ?u.525 → Prop
Countable α: Type u
α] [Countable: Sort ?u.528 → Prop
Countable β: Type v
β] : Countable: Sort ?u.531 → Prop
Countable (Sum: Type ?u.533 → Type ?u.532 → Type (max?u.533?u.532)
Sum α: Type u
α β: Type v
β) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

Countable (α ⊕ β)rcases exists_injective_nat: ∀ (α : Sort ?u.539) [inst : Countable α], ∃ f, Injective f
exists_injective_nat α: Type u
α with ⟨f, hf⟩: ∃ f, Injective f
⟨f: α → ℕ
f⟨f, hf⟩: ∃ f, Injective f
, hf: Injective f
hf⟨f, hf⟩: ∃ f, Injective f
⟩α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

f: α → ℕ

hf: Injective f

introCountable (α ⊕ β)
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

Countable (α ⊕ β)rcases exists_injective_nat: ∀ (α : Sort ?u.578) [inst : Countable α], ∃ f, Injective f
exists_injective_nat β: Type v
β with ⟨g, hg⟩: ∃ f, Injective f
⟨g: β → ℕ
g⟨g, hg⟩: ∃ f, Injective f
, hg: Injective g
hg⟨g, hg⟩: ∃ f, Injective f
⟩α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

f: α → ℕ

hf: Injective f

g: β → ℕ

hg: Injective g

intro.introCountable (α ⊕ β)
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

Countable (α ⊕ β)exact (Equiv.natSumNatEquivNat: ℕ ⊕ ℕ ≃ ℕ
Equiv.natSumNatEquivNat.injective: ∀ {α : Sort ?u.612} {β : Sort ?u.611} (e : α ≃ β), Injective ↑e
injective.comp: ∀ {α : Sort ?u.619} {β : Sort ?u.618} {φ : Sort ?u.617} {g : β → φ} {f : α → β},
  Injective g → Injective f → Injective (g ∘ f)
comp <| hf: Injective f
hf.sum_map: ∀ {α : Type ?u.643} {α' : Type ?u.641} {β : Type ?u.642} {β' : Type ?u.640} {f : α → β} {g : α' → β'},
  Injective f → Injective g → Injective (Sum.map f g)
sum_map hg: Injective g
hg).countable: ∀ {α : Sort ?u.694} {β : Sort ?u.693} [inst : Countable β] {f : α → β}, Injective f → Countable α
countable
Goals accomplished! 🐙

instance: ∀ {α : Type u} [inst : Countable α], Countable (Option α)
instance [Countable: Sort ?u.759 → Prop
Countable α: Type u
α] : Countable: Sort ?u.762 → Prop
Countable (Option: Type ?u.763 → Type ?u.763
Option α: Type u
α) :=
  Countable.of_equiv: ∀ {β : Sort ?u.766} (α : Sort ?u.767) [inst : Countable α], α ≃ β → Countable β
Countable.of_equiv _: Sort ?u.767
_ (Equiv.optionEquivSumPUnit: (α : Type ?u.785) → Option α ≃ α ⊕ PUnit
Equiv.optionEquivSumPUnit.{_, 0} α: Type u
α).symm: {α : Sort ?u.787} → {β : Sort ?u.786} → α ≃ β → β ≃ α
symm

instance: ∀ {α : Type u} {β : Type v} [inst : Countable α] [inst : Countable β], Countable (α × β)
instance [Countable: Sort ?u.839 → Prop
Countable α: Type u
α] [Countable: Sort ?u.842 → Prop
Countable β: Type v
β] : Countable: Sort ?u.845 → Prop
Countable (α: Type u
α × β: Type v
β) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

Countable (α × β)rcases exists_injective_nat: ∀ (α : Sort ?u.853) [inst : Countable α], ∃ f, Injective f
exists_injective_nat α: Type u
α with ⟨f, hf⟩: ∃ f, Injective f
⟨f: α → ℕ
f⟨f, hf⟩: ∃ f, Injective f
, hf: Injective f
hf⟨f, hf⟩: ∃ f, Injective f
⟩α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

f: α → ℕ

hf: Injective f

introCountable (α × β)
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

Countable (α × β)rcases exists_injective_nat: ∀ (α : Sort ?u.892) [inst : Countable α], ∃ f, Injective f
exists_injective_nat β: Type v
β with ⟨g, hg⟩: ∃ f, Injective f
⟨g: β → ℕ
g⟨g, hg⟩: ∃ f, Injective f
, hg: Injective g
hg⟨g, hg⟩: ∃ f, Injective f
⟩α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

f: α → ℕ

hf: Injective f

g: β → ℕ

hg: Injective g

intro.introCountable (α × β)
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: Countable β

Countable (α × β)exact (Nat.pairEquiv: ℕ × ℕ ≃ ℕ
Nat.pairEquiv.injective: ∀ {α : Sort ?u.926} {β : Sort ?u.925} (e : α ≃ β), Injective ↑e
injective.comp: ∀ {α : Sort ?u.933} {β : Sort ?u.932} {φ : Sort ?u.931} {g : β → φ} {f : α → β},
  Injective g → Injective f → Injective (g ∘ f)
comp <| hf: Injective f
hf.Prod_map: ∀ {α : Type ?u.954} {β : Type ?u.956} {γ : Type ?u.955} {δ : Type ?u.957} {f : α → γ} {g : β → δ},
  Injective f → Injective g → Injective (Prod.map f g)
Prod_map hg: Injective g
hg).countable: ∀ {α : Sort ?u.1008} {β : Sort ?u.1007} [inst : Countable β] {f : α → β}, Injective f → Countable α
countable
Goals accomplished! 🐙

instance: ∀ {α : Type u} {π : α → Type w} [inst : Countable α] [inst : ∀ (a : α), Countable (π a)], Countable (Sigma π)
instance [Countable: Sort ?u.1073 → Prop
Countable α: Type u
α] [∀ a: ?m.1077
a, Countable: Sort ?u.1080 → Prop
Countable (π: α → Type w
π a: ?m.1077
a)] : Countable: Sort ?u.1084 → Prop
Countable (Sigma: {α : Type ?u.1086} → (α → Type ?u.1085) → Type (max?u.1086?u.1085)
Sigma π: α → Type w
π) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: ∀ (a : α), Countable (π a)

Countable (Sigma π)rcases exists_injective_nat: ∀ (α : Sort ?u.1096) [inst : Countable α], ∃ f, Injective f
exists_injective_nat α: Type u
α with ⟨f, hf⟩: ∃ f, Injective f
⟨f: α → ℕ
f⟨f, hf⟩: ∃ f, Injective f
, hf: Injective f
hf⟨f, hf⟩: ∃ f, Injective f
⟩α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: ∀ (a : α), Countable (π a)

f: α → ℕ

hf: Injective f

introCountable (Sigma π)
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: ∀ (a : α), Countable (π a)

Countable (Sigma π)choose g: (a : α) → π a → ℕ
g hg: ∀ (a : α), Injective (g a)
hg using fun a: ?m.1138
a => exists_injective_nat: ∀ (α : Sort ?u.1140) [inst : Countable α], ∃ f, Injective f
exists_injective_nat (π: α → Type w
π a: ?m.1138
a)α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: ∀ (a : α), Countable (π a)

f: α → ℕ

hf: Injective f

g: (a : α) → π a → ℕ

hg: ∀ (a : α), Injective (g a)

introCountable (Sigma π)
  α: Type u

β: Type v

π: α → Type w

inst✝¹: Countable α

inst✝: ∀ (a : α), Countable (π a)

Countable (Sigma π)exact ((Equiv.sigmaEquivProd: (α : Type ?u.1161) → (β : Type ?u.1160) → (_ : α) × β ≃ α × β
Equiv.sigmaEquivProd ℕ: Type
ℕ ℕ: Type
ℕ).injective: ∀ {α : Sort ?u.1163} {β : Sort ?u.1162} (e : α ≃ β), Injective ↑e
injective.comp: ∀ {α : Sort ?u.1170} {β : Sort ?u.1169} {φ : Sort ?u.1168} {g : β → φ} {f : α → β},
  Injective g → Injective f → Injective (g ∘ f)
comp <| hf: Injective f
hf.sigma_map: ∀ {α₁ : Type ?u.1191} {α₂ : Type ?u.1192} {β₁ : α₁ → Type ?u.1193} {β₂ : α₂ → Type ?u.1194} {f₁ : α₁ → α₂}
  {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)}, Injective f₁ → (∀ (a : α₁), Injective (f₂ a)) → Injective (Sigma.map f₁ f₂)
sigma_map hg: ∀ (a : α), Injective (g a)
hg).countable: ∀ {α : Sort ?u.1259} {β : Sort ?u.1258} [inst : Countable β] {f : α → β}, Injective f → Countable α
countable
Goals accomplished! 🐙

end type

section sort

variable {α: Sort u
α : Sort u: Type u
SortSort u: Type u
 u} {β: Sort v
β : Sort v: Type v
SortSort v: Type v
 v} {π: α → Sort w
π : α: Sort u
α → Sort w: Type w
SortSort w: Type w
 w}

/-!
### Operations on `Sort _`s
-/

instance (priority := 500) SetCoe.countable: ∀ {α : Type u_1} [inst : Countable α] (s : Set α), Countable ↑s
SetCoe.countable {α: ?m.1364
α} [Countable: Sort ?u.1367 → Prop
Countable α: ?m.1364
α] (s: Set α
s : Set: Type ?u.1370 → Type ?u.1370
Set α: ?m.1364
α) : Countable: Sort ?u.1373 → Prop
Countable s: Set α
s :=
  Subtype.countable: ∀ {α : Sort ?u.1528} [inst : Countable α] {p : α → Prop}, Countable { x // p x }
Subtype.countable
#align set_coe.countable SetCoe.countable: ∀ {α : Type u_1} [inst : Countable α] (s : Set α), Countable ↑s
SetCoe.countable

instance: ∀ {α : Sort u} {β : Sort v} [inst : Countable α] [inst : Countable β], Countable (α ⊕' β)
instance [Countable: Sort ?u.1591 → Prop
Countable α: Sort u
α] [Countable: Sort ?u.1594 → Prop
Countable β: Sort v
β] : Countable: Sort ?u.1597 → Prop
Countable (PSum: Sort ?u.1599 → Sort ?u.1598 → Sort (max(max1?u.1599)?u.1598)
PSum α: Sort u
α β: Sort v
β) :=
  Countable.of_equiv: ∀ {β : Sort ?u.1603} (α : Sort ?u.1604) [inst : Countable α], α ≃ β → Countable β
Countable.of_equiv (Sum: Type ?u.1608 → Type ?u.1607 → Type (max?u.1608?u.1607)
Sum (PLift: Sort ?u.1609 → Type ?u.1609
PLift α: Sort u
α) (PLift: Sort ?u.1610 → Type ?u.1610
PLift β: Sort v
β)) (Equiv.plift: {α : Sort ?u.1612} → PLift α ≃ α
Equiv.plift.sumPSum: {α₁ : Type ?u.1617} →
  {α₂ : Sort ?u.1616} → {β₁ : Type ?u.1615} → {β₂ : Sort ?u.1614} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕' β₂
sumPSum Equiv.plift: {α : Sort ?u.1637} → PLift α ≃ α
Equiv.plift)

instance: ∀ {α : Sort u} {β : Sort v} [inst : Countable α] [inst : Countable β], Countable (PProd α β)
instance [Countable: Sort ?u.1717 → Prop
Countable α: Sort u
α] [Countable: Sort ?u.1720 → Prop
Countable β: Sort v
β] : Countable: Sort ?u.1723 → Prop
Countable (PProd: Sort ?u.1725 → Sort ?u.1724 → Sort (max(max1?u.1725)?u.1724)
PProd α: Sort u
α β: Sort v
β) :=
  Countable.of_equiv: ∀ {β : Sort ?u.1729} (α : Sort ?u.1730) [inst : Countable α], α ≃ β → Countable β
Countable.of_equiv (PLift: Sort ?u.1735 → Type ?u.1735
PLift α: Sort u
α × PLift: Sort ?u.1736 → Type ?u.1736
PLift β: Sort v
β) (Equiv.plift: {α : Sort ?u.1738} → PLift α ≃ α
Equiv.plift.prodPProd: {α₁ : Type ?u.1743} →
  {α₂ : Sort ?u.1742} → {β₁ : Type ?u.1741} → {β₂ : Sort ?u.1740} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ PProd α₂ β₂
prodPProd Equiv.plift: {α : Sort ?u.1763} → PLift α ≃ α
Equiv.plift)

instance: ∀ {α : Sort u} {π : α → Sort w} [inst : Countable α] [inst : ∀ (a : α), Countable (π a)], Countable (PSigma π)
instance [Countable: Sort ?u.1843 → Prop
Countable α: Sort u
α] [∀ a: ?m.1847
a, Countable: Sort ?u.1850 → Prop
Countable (π: α → Sort w
π a: ?m.1847
a)] : Countable: Sort ?u.1854 → Prop
Countable (PSigma: {α : Sort ?u.1856} → (α → Sort ?u.1855) → Sort (max(max1?u.1856)?u.1855)
PSigma π: α → Sort w
π) :=
  Countable.of_equiv: ∀ {β : Sort ?u.1864} (α : Sort ?u.1865) [inst : Countable α], α ≃ β → Countable β
Countable.of_equiv (Σa: PLift α
a : PLift: Sort ?u.1872 → Type ?u.1872
PLift α: Sort u
α, PLift: Sort ?u.1874 → Type ?u.1874
PLift (π: α → Sort w
π a: PLift α
a.down: {α : Sort ?u.1875} → PLift α → α
down)) (Equiv.psigmaEquivSigmaPLift: {α : Sort ?u.1882} → (β : α → Sort ?u.1881) → (i : α) ×' β i ≃ (i : PLift α) × PLift (β i.down)
Equiv.psigmaEquivSigmaPLift π: α → Sort w
π).symm: {α : Sort ?u.1888} → {β : Sort ?u.1887} → α ≃ β → β ≃ α
symm

instance: ∀ {α : Sort u} {π : α → Sort w} [inst : Finite α] [inst : ∀ (a : α), Countable (π a)], Countable ((a : α) → π a)
instance [Finite: Sort ?u.2016 → Prop
Finite α: Sort u
α] [∀ a: ?m.2020
a, Countable: Sort ?u.2023 → Prop
Countable (π: α → Sort w
π a: ?m.2020
a)] : Countable: Sort ?u.2027 → Prop
Countable (∀ a: ?m.2029
a, π: α → Sort w
π a: ?m.2029
a) := by
Goals accomplished! 🐙
  α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

Countable ((a : α) → π a)have : ∀ n: ?m.2041
n, Countable: Sort ?u.2044 → Prop
Countable (Fin: ℕ → Type
Fin n: ?m.2041
n → ℕ: Type
ℕ) := α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

Countable ((a : α) → π a)by
Goals accomplished! 🐙
    α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

∀ (n : ℕ), Countable (Fin n → ℕ)intro n: ℕ
nα: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

Countable (Fin n → ℕ)
    α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

∀ (n : ℕ), Countable (Fin n → ℕ)induction' n: ℕ
n with n: ℕ
n ihn: ?m.2067 n
ihnα: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

zeroCountable (Fin Nat.zero → ℕ)
α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

ihn: Countable (Fin n → ℕ)

succCountable (Fin (Nat.succ n) → ℕ)
    α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

∀ (n : ℕ), Countable (Fin n → ℕ)·α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

zeroCountable (Fin Nat.zero → ℕ) α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

zeroCountable (Fin Nat.zero → ℕ)
α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

ihn: Countable (Fin n → ℕ)

succCountable (Fin (Nat.succ n) → ℕ)change Countable: Sort ?u.2079 → Prop
Countable (Fin: ℕ → Type
Fin 0: ?m.2082
0 → ℕ: Type
ℕ)α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

zeroCountable (Fin 0 → ℕ);α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

zeroCountable (Fin 0 → ℕ) α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

zeroCountable (Fin Nat.zero → ℕ)infer_instance
Goals accomplished! 🐙
    α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

∀ (n : ℕ), Countable (Fin n → ℕ)·α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

ihn: Countable (Fin n → ℕ)

succCountable (Fin (Nat.succ n) → ℕ) α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

ihn: Countable (Fin n → ℕ)

succCountable (Fin (Nat.succ n) → ℕ)haveI := ihn: ?m.2067 n
ihnα: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

ihn, this: Countable (Fin n → ℕ)

succCountable (Fin (Nat.succ n) → ℕ)
      α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

n: ℕ

ihn: Countable (Fin n → ℕ)

succCountable (Fin (Nat.succ n) → ℕ)exact Countable.of_equiv: ∀ {β : Sort ?u.2166} (α : Sort ?u.2167) [inst : Countable α], α ≃ β → Countable β
Countable.of_equiv (ℕ: Type
ℕ × (Fin: ℕ → Type
Fin n: ℕ
n → ℕ: Type
ℕ)) (Equiv.piFinSucc: (n : ℕ) → (β : Type ?u.2176) → (Fin (n + 1) → β) ≃ β × (Fin n → β)
Equiv.piFinSucc _: ℕ
_ _: Type ?u.2176
_).symm: {α : Sort ?u.2180} → {β : Sort ?u.2179} → α ≃ β → β ≃ α
symm
Goals accomplished! 🐙
  α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

Countable ((a : α) → π a)rcases Finite.exists_equiv_fin: ∀ (α : Sort ?u.2218) [h : Finite α], ∃ n, Nonempty (α ≃ Fin n)
Finite.exists_equiv_fin α: Sort u
α with ⟨n, ⟨e⟩⟩: ∃ n, Nonempty (α ≃ Fin n)
⟨n: ℕ
n⟨n, ⟨e⟩⟩: ∃ n, Nonempty (α ≃ Fin n)
, ⟨e⟩: Nonempty (α ≃ Fin n)
⟨e: α ≃ Fin n
e⟨e⟩: Nonempty (α ≃ Fin n)
⟩⟨n, ⟨e⟩⟩: ∃ n, Nonempty (α ≃ Fin n)
⟩α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

this: ∀ (n : ℕ), Countable (Fin n → ℕ)

n: ℕ

e: α ≃ Fin n

intro.introCountable ((a : α) → π a)
  α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

Countable ((a : α) → π a)have f: ?m.2271
f := fun a: ?m.2273
a => (nonempty_embedding_nat: ∀ (α : Sort ?u.2275) [inst : Countable α], Nonempty (α ↪ ℕ)
nonempty_embedding_nat (π: α → Sort w
π a: ?m.2273
a)).some: {α : Sort ?u.2287} → Nonempty α → α
someα: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

this: ∀ (n : ℕ), Countable (Fin n → ℕ)

n: ℕ

e: α ≃ Fin n

f: (a : α) → π a ↪ ℕ

intro.introCountable ((a : α) → π a)
  α: Sort u

β: Sort v

π: α → Sort w

inst✝¹: Finite α

inst✝: ∀ (a : α), Countable (π a)

Countable ((a : α) → π a)exact ((Embedding.piCongrRight: {α : Sort ?u.2300} →
  {β : α → Sort ?u.2299} → {γ : α → Sort ?u.2298} → ((a : α) → β a ↪ γ a) → ((a : α) → β a) ↪ (a : α) → γ a
Embedding.piCongrRight f: ?m.2271
f).trans: {α : Sort ?u.2317} → {β : Sort ?u.2316} → {γ : Sort ?u.2315} → (α ↪ β) → (β ↪ γ) → α ↪ γ
trans (Equiv.piCongrLeft': {α : Sort ?u.2331} →
  {β : Sort ?u.2330} → (P : α → Sort ?u.2329) → (e : α ≃ β) → ((a : α) → P a) ≃ ((b : β) → P (↑e.symm b))
Equiv.piCongrLeft' _: ?m.2332 → Sort ?u.2329
_ e: α ≃ Fin n
e).toEmbedding: {α : Sort ?u.2340} → {β : Sort ?u.2339} → α ≃ β → α ↪ β
toEmbedding).countable: ∀ {α : Sort ?u.2358} {β : Sort ?u.2357} [inst : Countable β], (α ↪ β) → Countable α
countable
Goals accomplished! 🐙

end sort