awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u_1
inst : Countable α
⊢ Nonempty.{max 1 u_1} (α ↪ ℕ)

Tactic:
countable_iff_nonempty_embedding.1 ‹_›

Premises used: Iff.mp, countable_iff_nonempty_embedding
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
inst : Countable β
f : α ↪ β
⊢ Countable α

Tactic:
f.injective.countable

Premises used: Function.Injective.countable, Function.Embedding.injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
inst : Uncountable α
f : α ↪ β
⊢ Uncountable β

Tactic:
f.injective.uncountable

Premises used: Function.Injective.uncountable, Function.Embedding.injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
rcases : ∀ (f : α → ℕ) (hf : Injective f), Countable (α ⊕ β)
⊢ Countable (α ⊕ β)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
rcases : ∀ (g : β → ℕ) (hg : Injective g), Countable (α ⊕ β)
⊢ Countable (α ⊕ β)

Tactic:
rcases exists_injective_nat β with ⟨g, hg⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α ⊕ β)

Tactic:
(Equiv.natSumNatEquivNat.injective.comp <| hf.sumMap hg).countable

Premises used: Function.Injective.countable, Function.Injective.sumMap, Equiv.natSumNatEquivNat, Function.Injective.comp, Equiv.injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α ⊕ β)

Tactic:
exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sumMap hg).countable

Premises used: Function.Injective.countable, Function.Injective.sumMap, Equiv.natSumNatEquivNat, Function.Injective.comp, Equiv.injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
⊢ Uncountable (α ⊕ β)

Tactic:
inl_injective.uncountable

Premises used: Function.Injective.uncountable, Sum.inl_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable β
⊢ Uncountable (α ⊕ β)

Tactic:
inr_injective.uncountable

Premises used: Function.Injective.uncountable, Sum.inr_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
⊢ Countable.{u + 1} (Option α)

Tactic:
Countable.of_equiv _ (Equiv.optionEquivSumPUnit.{0, _} α).symm

Premises used: Countable.of_equiv, Equiv.optionEquivSumPUnit, Equiv.symm
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
⊢ Countable.{u + 1} (WithTop α)

Tactic:
Option.instCountable

Premises used: Option.instCountable, WithTop
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
⊢ Countable.{u + 1} (WithBot α)

Tactic:
Option.instCountable

Premises used: WithBot, Option.instCountable
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
⊢ Countable ℕ∞

Tactic:
Option.instCountable

Premises used: Option.instCountable, ENat, WithTop
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
⊢ Uncountable.{u + 1} (Option α)

Tactic:
Injective.uncountable fun _ _ ↦ Option.some_inj.1

Premises used: Function.Injective.uncountable, Iff.mp, Option.some_inj
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
⊢ Uncountable.{u + 1} (WithTop α)

Tactic:
Option.instUncountable

Premises used: Option.instUncountable, WithTop
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
⊢ Uncountable.{u + 1} (WithBot α)

Tactic:
Option.instUncountable

Premises used: WithBot, Option.instUncountable
-- Module: Mathlib.Data.Countable.Basic
Goal:
d n : ℕ
⊢ WithTop.untopD d (↑n : ℕ∞) = n

Tactic:
rfl

Premises used: WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
rcases : ∀ (f : α → ℕ) (hf : Injective f), Countable (α × β)
⊢ Countable (α × β)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
rcases : ∀ (g : β → ℕ) (hg : Injective g), Countable (α × β)
⊢ Countable (α × β)

Tactic:
rcases exists_injective_nat β with ⟨g, hg⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α × β)

Tactic:
(Nat.pairEquiv.injective.comp <| hf.prodMap hg).countable

Premises used: Function.Injective.prodMap, Function.Injective.countable, Function.Injective.comp, Equiv.injective, Nat.pairEquiv
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α × β)

Tactic:
exact (Nat.pairEquiv.injective.comp <| hf.prodMap hg).countable

Premises used: Function.Injective.prodMap, Function.Injective.countable, Function.Injective.comp, Equiv.injective, Nat.pairEquiv
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
inst_1 : Nonempty β
inhabit : ∀ (inhabited_h : Inhabited β), Uncountable (α × β)
⊢ Uncountable (α × β)

Tactic:
inhabit β
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
inst_1 : Nonempty β
inhabited_h : Inhabited β
⊢ Uncountable (α × β)

Tactic:
(Prod.mk_left_injective default).uncountable

Premises used: Inhabited.default, Function.Injective.uncountable, Prod.mk_left_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
inst_1 : Nonempty β
inhabited_h : Inhabited β
⊢ Uncountable (α × β)

Tactic:
exact (Prod.mk_left_injective default).uncountable

Premises used: Inhabited.default, Function.Injective.uncountable, Prod.mk_left_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : Uncountable β
inhabit : ∀ (inhabited_h : Inhabited α), Uncountable (α × β)
⊢ Uncountable (α × β)

Tactic:
inhabit α
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : Uncountable β
inhabited_h : Inhabited α
⊢ Uncountable (α × β)

Tactic:
(Prod.mk_right_injective default).uncountable

Premises used: Inhabited.default, Function.Injective.uncountable, Prod.mk_right_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : Uncountable β
inhabited_h : Inhabited α
⊢ Uncountable (α × β)

Tactic:
exact (Prod.mk_right_injective default).uncountable

Premises used: Inhabited.default, Function.Injective.uncountable, Prod.mk_right_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
inst : Nonempty β
h : Countable (α × β)
contrapose! : ∀ (h : Uncountable α), Uncountable (α × β)
⊢ Countable α

Tactic:
contrapose! h
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
inst : Nonempty β
h : Uncountable α
⊢ Uncountable (α × β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
inst : Nonempty α
h : Countable (α × β)
contrapose! : ∀ (h : Uncountable β), Uncountable (α × β)
⊢ Countable β

Tactic:
contrapose! h
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
inst : Nonempty α
h : Uncountable β
⊢ Uncountable (α × β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
inst : Countable (α × β)
⊢ Countable (β × α)

Tactic:
Countable.of_equiv _ (Equiv.prodComm α β)

Premises used: Countable.of_equiv, Equiv.prodComm
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w + 1} (π a)
rcases : ∀ (f : α → ℕ) (hf : Injective f), Countable (Sigma π)
⊢ Countable (Sigma π)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w + 1} (π a)
f : α → ℕ
hf : Injective f
choose : ∀ (g : (a : α) → π a → ℕ) (hg : ∀ (a : α), Injective (g a)), Countable (Sigma π)
⊢ Countable (Sigma π)

Tactic:
choose g hg using fun a => exists_injective_nat (π a)

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w + 1} (π a)
f : α → ℕ
hf : Injective f
g : (a : α) → π a → ℕ
hg : ∀ (a : α), Injective (g a)
⊢ Countable (Sigma π)

Tactic:
((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable

Premises used: Function.Injective.countable, Function.Injective.sigma_map, Function.Injective.comp, Nat, Equiv.injective, Equiv.sigmaEquivProd
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w + 1} (π a)
f : α → ℕ
hf : Injective f
g : (a : α) → π a → ℕ
hg : ∀ (a : α), Injective (g a)
⊢ Countable (Sigma π)

Tactic:
exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable

Premises used: Function.Injective.countable, Function.Injective.sigma_map, Function.Injective.comp, Nat, Equiv.injective, Equiv.sigmaEquivProd
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
π : α → Type w
a : α
inst : Uncountable.{w + 1} (π a)
⊢ Uncountable (Sigma π)

Tactic:
(sigma_mk_injective (i := a)).uncountable

Premises used: Function.Injective.uncountable, sigma_mk_injective
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : ∀ (a : α), Uncountable.{w + 1} (π a)
inhabit : ∀ (inhabited_h : Inhabited α), Uncountable (Sigma π)
⊢ Uncountable (Sigma π)

Tactic:
inhabit α
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : ∀ (a : α), Uncountable.{w + 1} (π a)
inhabited_h : Inhabited α
⊢ Uncountable (Sigma π)

Tactic:
Sigma.uncountable default

Premises used: Inhabited.default, Sigma.uncountable
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : ∀ (a : α), Uncountable.{w + 1} (π a)
inhabited_h : Inhabited α
⊢ Uncountable (Sigma π)

Tactic:
exact Sigma.uncountable default

Premises used: Inhabited.default, Sigma.uncountable
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
s : Set α
⊢ Countable.{u + 1} (↑s : Type u)

Tactic:
Subtype.countable

Premises used: Subtype.countable
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Countable α
inst_1 : Countable β
⊢ Countable (α ⊕' β)

Tactic:
Countable.of_equiv (PLift α ⊕ PLift β) (Equiv.plift.sumPSum Equiv.plift)

Premises used: Countable.of_equiv, Sum, PLift, Equiv.plift, Equiv.sumPSum
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Countable α
inst_1 : Countable β
⊢ Countable (α ×' β)

Tactic:
Countable.of_equiv (PLift α × PLift β) (Equiv.plift.prodPProd Equiv.plift)

Premises used: Countable.of_equiv, PLift, Equiv.plift, Equiv.prodPProd, Prod
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w} (π a)
⊢ Countable (PSigma π)

Tactic:
Countable.of_equiv (Σ a : PLift α, PLift (π a.down)) (Equiv.psigmaEquivSigmaPLift π).symm

Premises used: Countable.of_equiv, PLift, PLift.down, Equiv.psigmaEquivSigmaPLift, Equiv.symm, Sigma
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
⊢ Countable (Fin 0 → ℕ)

Tactic:
infer_instance
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
n : ℕ
ihn : Countable (Fin n → ℕ)
⊢ Countable (Fin (n + 1) → ℕ)

Tactic:
Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)

Premises used: Countable.of_equiv, Nat, Fin.consEquiv, Prod
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
n : ℕ
ihn : Countable (Fin n → ℕ)
⊢ Countable (Fin (n + 1) → ℕ)

Tactic:
exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)

Premises used: Countable.of_equiv, Nat, Fin.consEquiv, Prod
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
n : ℕ
zero : Countable (Fin 0 → ℕ)
succ : ∀ (n : ℕ) (ihn : Countable (Fin n → ℕ)), Countable (Fin (n + 1) → ℕ)
⊢ Countable (Fin n → ℕ)

Tactic:
induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
⊢ ∀ (n : ℕ), Countable (Fin n → ℕ)

Tactic:
have (n : ℕ) : Countable (Fin n → ℕ) := by
    induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
rcases : ∀ (n : ℕ) (e : α ≃ Fin n), Countable ((a : α) → π a)
⊢ Countable ((a : α) → π a)

Tactic:
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
have : ∀ (f : (a : α) → Embedding.{w, 1} (π a) ℕ), Countable ((a : α) → π a)
⊢ Countable ((a : α) → π a)

Tactic:
have f := fun a => (nonempty_embedding_nat (π a)).some
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
f : (a : α) → Embedding.{w, 1} (π a) ℕ
⊢ Countable ((a : α) → π a)

Tactic:
((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable

Premises used: Function.Embedding.piCongrRight, Function.Embedding.countable, Equiv.toEmbedding, Function.Embedding.trans, Equiv.piCongrLeft'
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
f : (a : α) → Embedding.{w, 1} (π a) ℕ
⊢ Countable ((a : α) → π a)

Tactic:
exact ((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable

Premises used: Function.Embedding.piCongrRight, Function.Embedding.countable, Equiv.toEmbedding, Function.Embedding.trans, Equiv.piCongrLeft'
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
inst : Countable α
⊢ Exists.{max 1 u} fun (f : α → ℕ) ↦ Injective f

Tactic:
Countable.exists_injective_nat'

Premises used: Countable.exists_injective_nat'
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
⊢ Countable ℕ

Tactic:
⟨⟨id, injective_id⟩⟩

Premises used: id, Function.injective_id, Countable.mk, Exists.intro
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable β
f : α → β
hf : Injective f
⊢ Countable α

Tactic:
let ⟨g, hg⟩ := exists_injective_nat β
  ⟨⟨g ∘ f, hg.comp hf⟩⟩

Premises used: Function.comp, _private.0.Function.Injective.countable.match_1, Countable.exists_injective_nat, Function.Injective.comp, Countable.mk, Exists.intro, Countable
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable α
f : α → β
hf : Surjective f
⊢ Countable β

Tactic:
(injective_surjInv hf).countable

Premises used: Function.Injective.countable, Function.injective_surjInv
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
inst : Nonempty α
inst_1 : Countable α
⊢ ∃ (f : ℕ → α), Surjective f

Tactic:
let ⟨f, hf⟩ := exists_injective_nat α
  ⟨invFun f, invFun_surjective hf⟩

Premises used: Function.invFun, Exists, Function.invFun_surjective, _private.0.Function.Injective.countable.match_1, Countable.exists_injective_nat, Exists.intro, Function.Surjective
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
inst : Nonempty α
⊢ Countable α ↔ ∃ (f : ℕ → α), Surjective f

Tactic:
⟨@exists_surjective_nat _ _, fun ⟨_, hf⟩ ↦ hf.countable⟩

Premises used: Function.Surjective.countable, exists_surjective_nat, Iff.intro, _private.0.countable_iff_exists_surjective.match_1, Countable
-- Module: Mathlib.Data.Countable.Defs
Goal:
β : Sort v
α : Sort u_1
inst : Countable α
e : α ≃ β
⊢ Countable β

Tactic:
e.symm.injective.countable

Premises used: Function.Injective.countable, Equiv.injective, Equiv.symm
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Countable α ↔ Countable β

Tactic:
⟨fun h => @Countable.of_equiv _ _ h e, fun h => @Countable.of_equiv _ _ h e.symm⟩

Premises used: Countable.of_equiv, Iff.intro, Equiv.symm
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β_1 : Sort v
β : Type v
inst : Countable β
⊢ Countable (ULift.{u, v} β)

Tactic:
Countable.of_equiv _ Equiv.ulift.symm

Premises used: Countable.of_equiv, Equiv.ulift, Equiv.symm
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable α
⊢ Countable.{u + 1} (PLift α)

Tactic:
Equiv.plift.injective.countable

Premises used: Function.Injective.countable, Equiv.plift, Equiv.injective
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Subsingleton α
⊢ Countable α

Tactic:
⟨⟨fun _ => 0, fun x y _ => Subsingleton.elim x y⟩⟩

Premises used: Countable.mk, Exists.intro, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable α
p : α → Prop
⊢ Countable.{max 1 u} { x : α // p x }

Tactic:
Subtype.val_injective.countable

Premises used: Function.Injective.countable, Subtype.val_injective
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
n : ℕ
⊢ Countable (Fin n)

Tactic:
Function.Injective.countable (@Fin.eq_of_val_eq n)

Premises used: Function.Injective.countable, Fin.eq_of_val_eq
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Finite α
⊢ Countable α

Tactic:
let ⟨_, ⟨e⟩⟩ := Finite.exists_equiv_fin α
  Countable.of_equiv _ e.symm

Premises used: Countable.of_equiv, Finite.exists_equiv_fin, Countable, Equiv.symm, Fin, _private.0.Finite.to_countable.match_1
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
⊢ Countable PUnit

Tactic:
Subsingleton.to_countable

Premises used: Subsingleton.to_countable
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
p : Prop
⊢ Countable p

Tactic:
Subsingleton.to_countable

Premises used: Subsingleton.to_countable
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
⊢ Countable Bool

Tactic:
⟨⟨fun b => cond b 0 1, Bool.injective_iff.2 Nat.one_ne_zero⟩⟩

Premises used: cond, Iff.mpr, Bool.injective_iff, Nat.one_ne_zero, Countable.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
⊢ Countable Prop

Tactic:
Countable.of_equiv Bool Equiv.propEquivBool.symm

Premises used: Equiv.propEquivBool, Countable.of_equiv, Bool, Equiv.symm
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable α
r : α → α → Prop
⊢ Countable.{u} (Quot r)

Tactic:
Quot.mk_surjective.countable

Premises used: Function.Surjective.countable, Quot.mk_surjective
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable α
s : Setoid α
⊢ Countable.{u} (Quotient s)

Tactic:
inferInstanceAs <| Countable (@Quot α _)

Premises used: _private.0.instCountableQuotient._proof_1
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
rw : ¬¬Countable α ↔ Countable α
rw₁ rw₂ : Countable α ↔ Countable α
⊢ ¬Uncountable α ↔ Countable α

Tactic:
rw [uncountable_iff_not_countable, not_not]

Premises used: Classical.not_not, uncountable_iff_not_countable
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
⊢ ¬Countable α ↔ Uncountable α

Tactic:
(uncountable_iff_not_countable α).symm

Premises used: uncountable_iff_not_countable, Iff.symm
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
inst : Countable α
⊢ ¬Uncountable α

Tactic:
not_uncountable_iff.2 ‹_›

Premises used: Iff.mpr, not_uncountable_iff
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
inst : Uncountable α
⊢ ¬Countable α

Tactic:
Uncountable.not_countable

Premises used: Uncountable.not_countable
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Uncountable α
f : α → β
hf : Injective f
⊢ Uncountable β

Tactic:
⟨fun _ ↦ not_countable hf.countable⟩

Premises used: Function.Injective.countable, not_countable, Uncountable.mk
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Uncountable β
f : α → β
hf : Surjective f
⊢ Uncountable α

Tactic:
(injective_surjInv hf).uncountable

Premises used: Function.Injective.uncountable, Function.injective_surjInv
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Uncountable α
inst_1 : Countable β
f : α → β
⊢ ¬Injective f

Tactic:
fun hf ↦ not_countable hf.countable

Premises used: Function.Injective.countable, not_countable, Not
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Countable α
inst_1 : Uncountable β
f : α → β
⊢ ¬Surjective f

Tactic:
fun hf ↦
  not_countable hf.countable

Premises used: Function.Surjective.countable, not_countable, Not
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
inst : Nonempty α
rw : ¬Countable α ↔ ∀ (f : ℕ → α), ¬Surjective f
rw₁ : (¬∃ (f : ℕ → α), Surjective f) ↔ ∀ (f : ℕ → α), ¬Surjective f
rw₂ rw₃ : (∀ (x : ℕ → α), ¬Surjective x) ↔ ∀ (f : ℕ → α), ¬Surjective f
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f

Tactic:
rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]

Premises used: not_exists, countable_iff_exists_surjective, not_countable_iff
-- Module: Mathlib.Data.Countable.Defs
Goal:
β : Sort v
α : Sort u_1
inst : Uncountable α
e : α ≃ β
⊢ Uncountable β

Tactic:
e.injective.uncountable

Premises used: Function.Injective.uncountable, Equiv.injective
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Uncountable α ↔ Uncountable β

Tactic:
⟨fun h => @Uncountable.of_equiv _ _ h e, fun h => @Uncountable.of_equiv _ _ h e.symm⟩

Premises used: Iff.intro, Equiv.symm, Uncountable.of_equiv
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β_1 : Sort v
β : Type v
inst : Uncountable β
⊢ Uncountable (ULift.{u, v} β)

Tactic:
.of_equiv _ Equiv.ulift.symm

Premises used: Equiv.ulift, Equiv.symm, Uncountable.of_equiv
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Uncountable α
⊢ Uncountable.{u + 1} (PLift α)

Tactic:
.of_equiv _ Equiv.plift.symm

Premises used: Equiv.plift, Equiv.symm, Uncountable.of_equiv
-- Module: Mathlib.Data.Countable.Defs
Goal:
α : Sort u
β : Sort v
inst : Uncountable α
⊢ Infinite α

Tactic:
⟨fun _ ↦ not_countable (α := α) inferInstance⟩

Premises used: not_countable, inferInstance, Infinite.mk
-- Module: Mathlib.Data.Countable.Small
Goal:
α : Type v
inst : Countable α
⊢ Small.{w, v} α

Tactic:
let ⟨_, hf⟩ := exists_injective_nat α
  small_of_injective hf

Premises used: small_of_injective, Countable.exists_injective_nat, _private.0.Countable.toSmall.match_1, Small