Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module data.countable.basic
! 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 → PropCountable ℤ: 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 uSortSort u: Type u u} {β: Sort vβ : Sort v: Type vSortSort v: Type v v}

theorem countable_iff_nonempty_embedding: Countable α ↔ Nonempty (α ↪ ℕ)countable_iff_nonempty_embedding : Countable: Sort ?u.32 → PropCountable α: Sort uα ↔ Nonempty: Sort ?u.33 → PropNonempty (α: Sort uα ↪ ℕ: Typeℕ) :=
⟨fun ⟨⟨f: α → ℕf, hf: Injective fhf⟩⟩ => ⟨⟨f: α → ℕf, hf: Injective fhf⟩⟩, fun ⟨f: α ↪ ℕf⟩ => ⟨⟨f: α ↪ ℕf, f: α ↪ ℕf.2: ∀ {α : Sort ?u.357} {β : Sort ?u.356} (self : α ↪ β), Injective self.toFun2⟩⟩⟩
#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 → PropCountable α: ?m.432α] : Nonempty: Sort ?u.438 → PropNonempty (α: ?m.432α ↪ ℕ: Typeℕ) :=
countable_iff_nonempty_embedding: ∀ {α : Sort ?u.444}, Countable α ↔ Nonempty (α ↪ ℕ)countable_iff_nonempty_embedding.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 ‹_›
#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 → PropCountable β: Sort vβ] (f: α ↪ βf : α: Sort uα ↪ β: Sort vβ) : Countable: Sort ?u.471 → PropCountable α: Sort uα :=
f: α ↪ βf.injective: ∀ {α : Sort ?u.475} {β : Sort ?u.476} (f : α ↪ β), Injective ↑finjective.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 → PropCountable α: Type uα] [Countable: Sort ?u.528 → PropCountable β: Type vβ] : Countable: Sort ?u.531 → PropCountable (Sum: Type ?u.533 → Type ?u.532 → Type (max?u.533?u.532)Sum α: Type uα β: Type vβ) := byGoals accomplished! 🐙
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βCountable (α ⊕ β)rcases exists_injective_nat: ∀ (α : Sort ?u.539) [inst : Countable α], ∃ f, Injective fexists_injective_nat α: Type uα with ⟨f, hf⟩: ∃ f, Injective f⟨f: α → ℕf⟨f, hf⟩: ∃ f, Injective f, hf: Injective fhf⟨f, hf⟩: ∃ f, Injective f⟩α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βf: α → ℕhf: Injective fintroCountable (α ⊕ β)
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βCountable (α ⊕ β)rcases exists_injective_nat: ∀ (α : Sort ?u.578) [inst : Countable α], ∃ f, Injective fexists_injective_nat β: Type vβ with ⟨g, hg⟩: ∃ f, Injective f⟨g: β → ℕg⟨g, hg⟩: ∃ f, Injective f, hg: Injective ghg⟨g, hg⟩: ∃ f, Injective f⟩α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βf: α → ℕhf: Injective fg: β → ℕhg: Injective gintro.introCountable (α ⊕ β)
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βCountable (α ⊕ β)exact (Equiv.natSumNatEquivNat: ℕ ⊕ ℕ ≃ ℕEquiv.natSumNatEquivNat.injective: ∀ {α : Sort ?u.612} {β : Sort ?u.611} (e : α ≃ β), Injective ↑einjective.comp: ∀ {α : Sort ?u.619} {β : Sort ?u.618} {φ : Sort ?u.617} {g : β → φ} {f : α → β},
Injective g → Injective f → Injective (g ∘ f)comp <| hf: Injective fhf.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 ghg).countable: ∀ {α : Sort ?u.694} {β : Sort ?u.693} [inst : Countable β] {f : α → β}, Injective f → Countable αcountableGoals accomplished! 🐙

instance: ∀ {α : Type u} [inst : Countable α], Countable (Option α)instance [Countable: Sort ?u.759 → PropCountable α: Type uα] : Countable: Sort ?u.762 → PropCountable (Option: Type ?u.763 → Type ?u.763Option α: 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 α ≃ α ⊕ PUnitEquiv.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 → PropCountable α: Type uα] [Countable: Sort ?u.842 → PropCountable β: Type vβ] : Countable: Sort ?u.845 → PropCountable (α: Type uα × β: Type vβ) := byGoals accomplished! 🐙
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βCountable (α × β)rcases exists_injective_nat: ∀ (α : Sort ?u.853) [inst : Countable α], ∃ f, Injective fexists_injective_nat α: Type uα with ⟨f, hf⟩: ∃ f, Injective f⟨f: α → ℕf⟨f, hf⟩: ∃ f, Injective f, hf: Injective fhf⟨f, hf⟩: ∃ f, Injective f⟩α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βf: α → ℕhf: Injective fintroCountable (α × β)
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βCountable (α × β)rcases exists_injective_nat: ∀ (α : Sort ?u.892) [inst : Countable α], ∃ f, Injective fexists_injective_nat β: Type vβ with ⟨g, hg⟩: ∃ f, Injective f⟨g: β → ℕg⟨g, hg⟩: ∃ f, Injective f, hg: Injective ghg⟨g, hg⟩: ∃ f, Injective f⟩α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βf: α → ℕhf: Injective fg: β → ℕhg: Injective gintro.introCountable (α × β)
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: Countable βCountable (α × β)exact (Nat.pairEquiv: ℕ × ℕ ≃ ℕNat.pairEquiv.injective: ∀ {α : Sort ?u.926} {β : Sort ?u.925} (e : α ≃ β), Injective ↑einjective.comp: ∀ {α : Sort ?u.933} {β : Sort ?u.932} {φ : Sort ?u.931} {g : β → φ} {f : α → β},
Injective g → Injective f → Injective (g ∘ f)comp <| hf: Injective fhf.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 ghg).countable: ∀ {α : Sort ?u.1008} {β : Sort ?u.1007} [inst : Countable β] {f : α → β}, Injective f → Countable αcountableGoals accomplished! 🐙

instance: ∀ {α : Type u} {π : α → Type w} [inst : Countable α] [inst : ∀ (a : α), Countable (π a)], Countable (Sigma π)instance [Countable: Sort ?u.1073 → PropCountable α: Type uα] [∀ a: ?m.1077a, Countable: Sort ?u.1080 → PropCountable (π: α → Type wπ a: ?m.1077a)] : Countable: Sort ?u.1084 → PropCountable (Sigma: {α : Type ?u.1086} → (α → Type ?u.1085) → Type (max?u.1086?u.1085)Sigma π: α → Type wπ) := byGoals accomplished! 🐙
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: ∀ (a : α), Countable (π a)Countable (Sigma π)rcases exists_injective_nat: ∀ (α : Sort ?u.1096) [inst : Countable α], ∃ f, Injective fexists_injective_nat α: Type uα with ⟨f, hf⟩: ∃ f, Injective f⟨f: α → ℕf⟨f, hf⟩: ∃ f, Injective f, hf: Injective fhf⟨f, hf⟩: ∃ f, Injective f⟩α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: ∀ (a : α), Countable (π a)f: α → ℕhf: Injective fintroCountable (Sigma π)
α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: ∀ (a : α), Countable (π a)Countable (Sigma π)choose g: (a : α) → π a → ℕg hg: ∀ (a : α), Injective (g a)hg using fun a: ?m.1138a => exists_injective_nat: ∀ (α : Sort ?u.1140) [inst : Countable α], ∃ f, Injective fexists_injective_nat (π: α → Type wπ a: ?m.1138a)α: Type uβ: Type vπ: α → Type winst✝¹: Countable αinst✝: ∀ (a : α), Countable (π a)f: α → ℕhf: Injective fg: (a : α) → π a → ℕhg: ∀ (a : α), Injective (g a)introCountable (Sigma π)
α: Type uβ: Type vπ: α → Type winst✝¹: 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 ↑einjective.comp: ∀ {α : Sort ?u.1170} {β : Sort ?u.1169} {φ : Sort ?u.1168} {g : β → φ} {f : α → β},
Injective g → Injective f → Injective (g ∘ f)comp <| hf: Injective fhf.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 αcountableGoals accomplished! 🐙

end type

section sort

variable {α: Sort uα : Sort u: Type uSortSort u: Type u u} {β: Sort vβ : Sort v: Type vSortSort v: Type v v} {π: α → Sort wπ : α: Sort uα → Sort w: Type wSortSort w: Type w w}

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

instance (priority := 500) SetCoe.countable: ∀ {α : Type u_1} [inst : Countable α] (s : Set α), Countable ↑sSetCoe.countable {α: ?m.1364α} [Countable: Sort ?u.1367 → PropCountable α: ?m.1364α] (s: Set αs : Set: Type ?u.1370 → Type ?u.1370Set α: ?m.1364α) : Countable: Sort ?u.1373 → PropCountable 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 ↑sSetCoe.countable

instance: ∀ {α : Sort u} {β : Sort v} [inst : Countable α] [inst : Countable β], Countable (α ⊕' β)instance [Countable: Sort ?u.1591 → PropCountable α: Sort uα] [Countable: Sort ?u.1594 → PropCountable β: Sort vβ] : Countable: Sort ?u.1597 → PropCountable (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.1609PLift α: Sort uα) (PLift: Sort ?u.1610 → Type ?u.1610PLift β: 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 → PropCountable α: Sort uα] [Countable: Sort ?u.1720 → PropCountable β: Sort vβ] : Countable: Sort ?u.1723 → PropCountable (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.1735PLift α: Sort uα × PLift: Sort ?u.1736 → Type ?u.1736PLift β: 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 → PropCountable α: Sort uα] [∀ a: ?m.1847a, Countable: Sort ?u.1850 → PropCountable (π: α → Sort wπ a: ?m.1847a)] : Countable: Sort ?u.1854 → PropCountable (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.1872PLift α: Sort uα, PLift: Sort ?u.1874 → Type ?u.1874PLift (π: α → 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 → PropFinite α: Sort uα] [∀ a: ?m.2020a, Countable: Sort ?u.2023 → PropCountable (π: α → Sort wπ a: ?m.2020a)] : Countable: Sort ?u.2027 → PropCountable (∀ a: ?m.2029a, π: α → Sort wπ a: ?m.2029a) := byGoals accomplished! 🐙
α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)Countable ((a : α) → π a)have : ∀ n: ?m.2041n, Countable: Sort ?u.2044 → PropCountable (Fin: ℕ → TypeFin n: ?m.2041n → ℕ: Typeℕ) := α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)Countable ((a : α) → π a)byGoals accomplished! 🐙
α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)∀ (n : ℕ), Countable (Fin n → ℕ)intro n: ℕnα: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)n: ℕCountable (Fin n → ℕ)
α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)∀ (n : ℕ), Countable (Fin n → ℕ)induction' n: ℕn with n: ℕn ihn: ?m.2067 nihnα: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)zeroCountable (Fin Nat.zero → ℕ)α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)n: ℕihn: Countable (Fin n → ℕ)succCountable (Fin (Nat.succ n) → ℕ)
α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)∀ (n : ℕ), Countable (Fin n → ℕ)·α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)zeroCountable (Fin Nat.zero → ℕ) α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)zeroCountable (Fin Nat.zero → ℕ)α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)n: ℕihn: Countable (Fin n → ℕ)succCountable (Fin (Nat.succ n) → ℕ)change Countable: Sort ?u.2079 → PropCountable (Fin: ℕ → TypeFin 0: ?m.20820 → ℕ: Typeℕ)α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)zeroCountable (Fin 0 → ℕ);α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)zeroCountable (Fin 0 → ℕ) α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)zeroCountable (Fin Nat.zero → ℕ)infer_instanceGoals accomplished! 🐙
α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)∀ (n : ℕ), Countable (Fin n → ℕ)·α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)n: ℕihn: Countable (Fin n → ℕ)succCountable (Fin (Nat.succ n) → ℕ) α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)n: ℕihn: Countable (Fin n → ℕ)succCountable (Fin (Nat.succ n) → ℕ)haveI := ihn: ?m.2067 nihnα: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)n: ℕihn, this: Countable (Fin n → ℕ)succCountable (Fin (Nat.succ n) → ℕ)
α: Sort uβ: Sort vπ: α → Sort winst✝¹: 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: ℕ → TypeFin 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} → α ≃ β → β ≃ αsymmGoals accomplished! 🐙
α: Sort uβ: Sort vπ: α → Sort winst✝¹: 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 ne⟨e⟩: Nonempty (α ≃ Fin n)⟩⟨n, ⟨e⟩⟩: ∃ n, Nonempty (α ≃ Fin n)⟩α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)this: ∀ (n : ℕ), Countable (Fin n → ℕ)n: ℕe: α ≃ Fin nintro.introCountable ((a : α) → π a)
α: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)Countable ((a : α) → π a)have f: ?m.2271f := fun a: ?m.2273a => (nonempty_embedding_nat: ∀ (α : Sort ?u.2275) [inst : Countable α], Nonempty (α ↪ ℕ)nonempty_embedding_nat (π: α → Sort wπ a: ?m.2273a)).some: {α : Sort ?u.2287} → Nonempty α → αsomeα: Sort uβ: Sort vπ: α → Sort winst✝¹: Finite αinst✝: ∀ (a : α), Countable (π a)this: ∀ (n : ℕ), Countable (Fin n → ℕ)n: ℕe: α ≃ Fin nf: (a : α) → π a ↪ ℕintro.introCountable ((a : α) → π a)
α: Sort uβ: Sort vπ: α → Sort winst✝¹: 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 : α) → γ aEmbedding.piCongrRight f: ?m.2271f).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 ne).toEmbedding: {α : Sort ?u.2340} → {β : Sort ?u.2339} → α ≃ β → α ↪ βtoEmbedding).countable: ∀ {α : Sort ?u.2358} {β : Sort ?u.2357} [inst : Countable β], (α ↪ β) → Countable αcountableGoals accomplished! 🐙

end sort
```