awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔ ℵ₀ ≤ c

Tactic:
enat_gc.u_eq_top

Premises used: GaloisConnection.u_eq_top, Cardinal.enat_gc
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ Ne (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔ c < ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ LT.lt (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔ c < ℵ₀

Tactic:
simp [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
ha : c ≤ ℵ₀
⊢ c ≤ ℵ₀

Tactic:
ha
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
ha : c ≤ ℵ₀
inl :
  ∀ (c : ℕ∞),
    Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} (↑c : Cardinal.{u})) : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} c) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)

Tactic:
lift c to ℕ∞ using ha
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : ℕ∞
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} (↑c : Cardinal.{u})) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
ha : ℵ₀ ≤ c
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} c) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)

Tactic:
simp [toENat_eq_top.2, ha]

Premises used: Iff.mpr, Cardinal.toENat_eq_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ c ≤ ℵ₀ ∨ ℵ₀ ≤ c

Tactic:
cases le_total c ℵ₀ with
  | inl ha => lift c to ℕ∞ using ha; simp
  | inr ha => simp [toENat_eq_top.2, ha]

Premises used: Iff.mpr, le_total, Cardinal.aleph0, Cardinal.toENat_eq_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
α : Type u
β : Type v
e : α ≃ β
rw :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} #α) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
rw₁ :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{max u v, v} #β) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
rw₂ rw₃ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) #α : ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)

Tactic:
rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]

Premises used: Cardinal.toENat_lift
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
a : (↑(m + n) : Cardinal.{u_1}) ∈ Iic ℵ₀
a₁ : (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1}) ∈ Iic ℵ₀
a₂ :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑(m + n) : Cardinal.{u_1}) : ℕ∞)
    ((toENat : (a : Cardinal.{u_1}) → ℕ∞) ((↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1})) : ℕ∞)
⊢ (↑(m + n) : Cardinal.{u_1}) = (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1})

Tactic:
apply toENat_injOn

Premises used: Cardinal.toENat_injOn
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ (↑(m + n) : Cardinal.{u_1}) ∈ Iic ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1}) ∈ Iic ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑(m + n) : Cardinal.{u_1}) : ℕ∞)
    ((toENat : (a : Cardinal.{u_1}) → ℕ∞) ((↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1})) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
⊢ ℵ₀ + (↑m : Cardinal.{u_1}) = ℵ₀

Tactic:
(ofENat_add ⊤ m).symm

Premises used: Cardinal.ofENat_add, Cardinal.ofENat, Top.top, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
rw : ℵ₀ + (↑m : Cardinal.{u_1}) = ℵ₀
rw₁ rw₂ : ℵ₀ = ℵ₀
⊢ (↑m : Cardinal.{u_1}) + ℵ₀ = ℵ₀

Tactic:
rw [add_comm, aleph0_add_ofENat]

Premises used: add_comm, Cardinal.aleph0_add_ofENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
hm : Ne (α := ℕ∞) ⊤ 0
⊢ (↑⊤ : Cardinal.{u_1}) * ℵ₀ = ℵ₀

Tactic:
aleph0_mul_aleph0

Premises used: Cardinal.ofENat, Cardinal.aleph0_mul_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
hm : Ne (α := ℕ∞) ⊤ 0
⊢ (↑⊤ : Cardinal.{u_1}) * ℵ₀ = ℵ₀

Tactic:
exact aleph0_mul_aleph0

Premises used: Cardinal.aleph0_mul_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
hm : Ne (α := ℕ∞) (↑m : ℕ∞) 0
coe : (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
coe₁ coe₂ : ℵ₀ = ℵ₀
⊢ (↑(↑m : ℕ∞) : Cardinal.{u_1}) * ℵ₀ = ℵ₀

Tactic:
rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

Premises used: Cardinal.nat_mul_aleph0, Cardinal.ofENat_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
hm : m ≠ 0
top : ∀ (hm : Ne (α := ℕ∞) ⊤ 0), (↑⊤ : Cardinal.{u_1}) * ℵ₀ = ℵ₀
coe : ∀ (m : ℕ) (hm : Ne (α := ℕ∞) (↑m : ℕ∞) 0), (↑(↑m : ℕ∞) : Cardinal.{u_1}) * ℵ₀ = ℵ₀
⊢ (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀

Tactic:
induction m with
  | top => exact aleph0_mul_aleph0
  | coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

Premises used: Cardinal.nat_mul_aleph0, Cardinal.ofENat_nat, Cardinal.aleph0_mul_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
hm : m ≠ 0
rw : (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
rw₁ rw₂ : ℵ₀ = ℵ₀
⊢ ℵ₀ * (↑m : Cardinal.{u_1}) = ℵ₀

Tactic:
rw [mul_comm, ofENat_mul_aleph0 hm]

Premises used: Cardinal.ofENat_mul_aleph0, mul_comm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ (↑(m * n) : Cardinal.{u_1}) ∈ Iic ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑(m * n) : Cardinal.{u_1}) : ℕ∞)
    ((toENat : (a : Cardinal.{u_1}) → ℕ∞) ((↑m : Cardinal.{u_1}) * (↑n : Cardinal.{u_1})) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
rsuffices : ∀ (y : Fin n ↪ (↑sᶜ : Type u_1)), ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))
rsuffices₁ : Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
⊢ ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))

Tactic:
rsuffices ⟨y⟩ : Nonempty (Fin n ↪ (sᶜ : Set α))

Premises used: Compl.compl, Set.Elem, Function.Embedding, Nonempty, Fin
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
y : Fin n ↪ (↑sᶜ : Type u_1)
h : Disjoint s (range (ι := Fin n) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ sᶜ)) : (a : Fin n) → α))
⊢ ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))

Tactic:
use y.trans (subtype _)

Premises used: Function.Embedding.trans, Function.Embedding.subtype
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
y : Fin n ↪ (↑sᶜ : Type u_1)
h :
  ∀ ⦃a : α⦄,
    Membership.mem (γ := Set α) (range (ι := Fin n) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ sᶜ)) : (a : Fin n) → α)) a →
      a ∉ s
⊢ Disjoint s (range (ι := Fin n) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ sᶜ)) : (a : Fin n) → α))

Tactic:
rw [Set.disjoint_right]

Premises used: Set.disjoint_right
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
y : Fin n ↪ (↑sᶜ : Type u_1)
i : Fin n
⊢ ((y.trans (subtype fun (x : α) ↦ x ∈ sᶜ) : (a : Fin n) → α) i : α) ∉ s

Tactic:
simpa only [← mem_compl_iff] using Subtype.coe_prop (y i)

Premises used: Subtype.coe_prop, DFunLike.coe, Set.mem_compl_iff
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
inl : ∀ (hα : Finite α), Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
inr : ∀ (hα : Infinite α), Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))

Tactic:
rcases finite_or_infinite α with hα | hα

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
hα : Finite α
x : Fintype α := Fintype.ofFinite α
inl : Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))

Tactic:
apply nonempty_of_card_le

Premises used: Function.Embedding.nonempty_of_card_le
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
hα : Finite α
x : Fintype α := Fintype.ofFinite α
inl : n ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
inl₁ : s.ncard + n ≤ s.ncard + Fintype.card.{u_1} (↑sᶜ : Type u_1)
inl₂ : s.ncard + n ≤ s.ncard + Nat.card.{u_1} (↑sᶜ : Type u_1)
inl₃ : s.ncard + n ≤ s.ncard + sᶜ.ncard
inl₄ : s.ncard + n ≤ Nat.card α
inl₅ : LE.le (α := ℕ∞) (↑(s.ncard + n) : ℕ∞) (↑(Nat.card α) : ℕ∞)
inl₆ : (↑(s.ncard + n) : ℕ∞) ≤ ENat.card α
inl₇ inl₈ inl₉ inl₁₀ : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)

Tactic:
rwa [Fintype.card_fin, ← add_le_add_iff_left s.ncard,
      ← Nat.card_eq_fintype_card, Nat.card_coe_set_eq,
        ncard_add_ncard_compl, ← ENat.coe_le_coe,
        ← ENat.card_eq_coe_natCard, ENat.coe_add]

Premises used: Fintype.card_fin, add_le_add_iff_left, Nat.card_coe_set_eq, Set.ncard_add_ncard_compl, ENat.coe_le_coe, Set.ncard, ENat.coe_add, Nat.card_eq_fintype_card, ENat.card_eq_coe_natCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
hα : Finite α
x : Fintype α := Fintype.ofFinite α
inl : Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))

Tactic:
classical
    apply nonempty_of_card_le
    rwa [Fintype.card_fin, ← add_le_add_iff_left s.ncard,
      ← Nat.card_eq_fintype_card, Nat.card_coe_set_eq,
        ncard_add_ncard_compl, ← ENat.coe_le_coe,
        ← ENat.card_eq_coe_natCard, ENat.coe_add]

Premises used: Fintype.card_fin, add_le_add_iff_left, Nat.card_coe_set_eq, Set.ncard_add_ncard_compl, ENat.coe_le_coe, Set.ncard, ENat.coe_add, Nat.card_eq_fintype_card, Function.Embedding.nonempty_of_card_le, ENat.card_eq_coe_natCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
hα : Infinite α
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))

Tactic:
⟨valEmbedding.trans s.toFinite.infinite_compl.to_subtype.natEmbedding⟩

Premises used: Fin.valEmbedding, Nonempty.intro, Function.Embedding.trans, Infinite.natEmbedding
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
hα : Infinite α
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))

Tactic:
exact ⟨valEmbedding.trans s.toFinite.infinite_compl.to_subtype.natEmbedding⟩
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite α
hs : s.ncard + n ≤ Nat.card α
hs₁ : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
⊢ ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))

Tactic:
apply exists_embedding_disjoint_range_of_add_le_ENat_card

Premises used: Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite α
hs : s.ncard + n ≤ Nat.card α
hs₁ : (↑(s.ncard + n) : ℕ∞) ≤ ENat.card α
hs₂ : LE.le (α := ℕ∞) (↑(s.ncard + n) : ℕ∞) (↑(Nat.card α) : ℕ∞)
hs₃ hs₄ hs₅ hs₆ : s.ncard + n ≤ Nat.card α
⊢ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α

Tactic:
rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]

Premises used: ENat.coe_le_coe, ENat.coe_add, ENat.card_eq_coe_natCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
⊢ HAdd.hAdd (α := ℕ∞) (↑(ncard (α := α) (range (ι := Fin m) (⇑x : (a : Fin m) → α))) : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α

Tactic:
simpa [← Nat.card_coe_set_eq, Nat.card_range_of_injective x.injective]

Premises used: Nat.card_coe_set_eq, Function.Embedding.injective, Nat.card_range_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
obtain :
  ∀ (y : Fin n ↪ α)
    (hxy :
      Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))),
    ∃ (a : Fin (m + n) ↪ α), (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) a = x
⊢ ∃ (a : Fin (m + n) ↪ α), (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) a = x

Tactic:
obtain ⟨y, hxy⟩ :=
    exists_embedding_disjoint_range_of_add_le_ENat_card (s := range x)
      (by simpa [← Nat.card_coe_set_eq, Nat.card_range_of_injective x.injective])

Premises used: Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))
h : (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) = x
⊢ ∃ (a : Fin (m + n) ↪ α), (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) a = x

Tactic:
use append hxy

Premises used: Fin.Embedding.append
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))
h :
  ∀ (i : Fin m),
    Eq (α := α) (((fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) : (a : Fin m) → α) i : α)
      ((x : (a : Fin m) → α) i : α)
⊢ (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) = x

Tactic:
ext i
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))
i : Fin m
⊢ Eq (α := α) (((fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) : (a : Fin m) → α) i : α)
    ((x : (a : Fin m) → α) i : α)

Tactic:
simp [trans_apply, coe_castAddEmb, append]

Premises used: Function.Embedding.trans_apply, Fin.coe_castAddEmb, Fin.Embedding.append
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
hmn : m ≤ n
hn : (↑n : ℕ∞) ≤ ENat.card α
obtain :
  ∀ (k : ℕ) (hmn : m ≤ m + k) (hn : (↑(m + k) : ℕ∞) ≤ ENat.card α),
    Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin n ↪ α) ↦ (castLEEmb hmn).trans x

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m k : ℕ
hmn : m ≤ m + k
hn : (↑(m + k) : ℕ∞) ≤ ENat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x

Tactic:
Fin.Embedding.restrictSurjective_of_add_le_ENatCard hn

Premises used: Fin.castAddEmb, Fin.Embedding.restrictSurjective_of_add_le_ENatCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m k : ℕ
hmn : m ≤ m + k
hn : (↑(m + k) : ℕ∞) ≤ ENat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x

Tactic:
exact Fin.Embedding.restrictSurjective_of_add_le_ENatCard hn

Premises used: Fin.Embedding.restrictSurjective_of_add_le_ENatCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hn : m + n ≤ Nat.card α
hn₁ : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x

Tactic:
apply restrictSurjective_of_add_le_ENatCard

Premises used: Fin.Embedding.restrictSurjective_of_add_le_ENatCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hn : m + n ≤ Nat.card α
hn₁ : (↑(m + n) : ℕ∞) ≤ ENat.card α
hn₂ : LE.le (α := ℕ∞) (↑(m + n) : ℕ∞) (↑(Nat.card α) : ℕ∞)
hn₃ hn₄ hn₅ hn₆ : m + n ≤ Nat.card α
⊢ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α

Tactic:
rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]

Premises used: ENat.coe_le_coe, ENat.coe_add, ENat.card_eq_coe_natCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hmn : m ≤ n
hn : n ≤ Nat.card α
obtain :
  ∀ (k : ℕ) (hmn : m ≤ m + k) (hn : m + k ≤ Nat.card α),
    Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin n ↪ α) ↦ (castLEEmb hmn).trans x

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m : ℕ
inst : Finite α
k : ℕ
hmn : m ≤ m + k
hn : m + k ≤ Nat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x

Tactic:
Fin.Embedding.restrictSurjective_of_add_le_natCard hn

Premises used: Fin.castAddEmb, Fin.Embedding.restrictSurjective_of_add_le_natCard
-- Module: Mathlib.SetTheory.Cardinal.Embedding
Goal:
α : Type u_1
m : ℕ
inst : Finite α
k : ℕ
hmn : m ≤ m + k
hn : m + k ≤ Nat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x

Tactic:
exact Fin.Embedding.restrictSurjective_of_add_le_natCard hn

Premises used: Fin.Embedding.restrictSurjective_of_add_le_natCard
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Fintype α
⊢ Nat.card α = Fintype.card α

Tactic:
mk_toNat_eq_card

Premises used: Cardinal.mk_toNat_eq_card, Nat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
x : Fintype α
⊢ Fintype.card α = Nat.card α

Tactic:
mk_toNat_eq_card.symm

Premises used: Cardinal.mk_toNat_eq_card, Nat.card, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
s : Finset α
⊢ Nat.card.{u_1} ↥s = s.card

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_coe]

Premises used: Fintype.card_coe, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ Nat.card.{u_1} (↑s : Type u_1) = s.toFinset.card

Tactic:
simp only [← Nat.card_eq_finsetCard, s.mem_toFinset]

Premises used: Nat.card_eq_finsetCard, Set.mem_toFinset
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ Nat.card.{u_1} (↑s : Type u_1) = hs.toFinset (s := s).card

Tactic:
simp only [← Nat.card_eq_finsetCard, hs.mem_toFinset]

Premises used: Nat.card_eq_finsetCard, Set.Finite.mem_toFinset
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
rw : Nat.card.{u_1} { x : α // p x } = Fintype.card.{u_1} { x : α // p x }
rw₁ rw₂ : Nat.card.{u_1} { x : α // p x } = Nat.card.{u_1} { x : α // p x }
⊢ Nat.card.{u_1} { x : α // p x } = s.card

Tactic:
rw [← Fintype.subtype_card s H, Fintype.card_eq_nat_card]

Premises used: Fintype.subtype_card, Fintype.card_eq_nat_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : IsEmpty α
⊢ Nat.card α = 0

Tactic:
simp [Nat.card]

Premises used: Nat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Infinite α
⊢ Nat.card α = 0

Tactic:
mk_toNat_of_infinite

Premises used: Nat.card, Cardinal.mk_toNat_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Finite α
rw : #α < ℵ₀
⊢ (↑(Nat.card α) : Cardinal.{u_1}) = #α

Tactic:
rw [Nat.card, Cardinal.cast_toNat_of_lt_aleph0]

Premises used: Nat.card, Cardinal.cast_toNat_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Finite α
⊢ #α < ℵ₀

Tactic:
Cardinal.lt_aleph0_of_finite _

Premises used: Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Finite α
⊢ #α < ℵ₀

Tactic:
exact Cardinal.lt_aleph0_of_finite _

Premises used: Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
⊢ Nat.card.{u_1} (↑s : Type u_1) = 0

Tactic:
@card_eq_zero_of_infinite _ hs.to_subtype

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

Tactic:
simp [Nat.card, mk_eq_zero_iff, aleph0_le_mk_iff]

Premises used: Cardinal.aleph0_le_mk_iff, Nat.card, Cardinal.mk_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α

Tactic:
simp [card_eq_zero, not_or]

Premises used: not_or, Nat.card_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ 0 < Nat.card α ↔ Nonempty α ∧ Finite α

Tactic:
simp [Nat.card, mk_eq_zero_iff, mk_lt_aleph0_iff]

Premises used: Nat.card, Cardinal.mk_eq_zero_iff, Cardinal.mk_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Nonempty α
inst_1 : Finite α
⊢ 0 < Nat.card α

Tactic:
card_pos_iff.2 ⟨‹_›, ‹_›⟩

Premises used: Iff.mpr, Nat.card_pos_iff, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
h : Nat.card α ≠ 0
⊢ Finite α

Tactic:
(card_ne_zero.1 h).2

Premises used: And.right, Iff.mp, Nat.card_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Nat.card α = Nat.card β

Tactic:
Cardinal.toNat_congr f

Premises used: Cardinal.toNat_congr, Nat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u
β : Type v
inst : Finite β
f : α → β
hf : Injective f
⊢ lift.{u, v} #β < ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u
β : Type v
inst : Finite β
f : α → β
hf : Injective f
⊢ Nat.card α ≤ Nat.card β

Tactic:
simpa using toNat_le_toNat (lift_mk_le_lift_mk_of_injective hf) (by simp)

Premises used: Cardinal.toNat_le_toNat, Cardinal.lift_mk_le_lift_mk_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u
β : Type v
inst : Finite α
f : α → β
hf : Surjective f
⊢ lift.{u, v} #β ≤ lift.{v, u} #α

Tactic:
have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u
β : Type v
inst : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ lift.{v, u} #α < ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u
β : Type v
inst : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ Nat.card β ≤ Nat.card α

Tactic:
simpa using toNat_le_toNat this (by simp)

Premises used: Cardinal.toNat_le_toNat
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Bijective f
⊢ Nat.card α = Nat.card β

Tactic:
card_congr (Equiv.ofBijective f hf)

Premises used: Nat.card_congr, Equiv.ofBijective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
rw : Injective f → (Surjective f ↔ Nat.card α = Nat.card β)
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
rw [Bijective, and_congr_right_iff]

Premises used: and_congr_right_iff, Function.Bijective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
h : Injective f
have : ∀ (this : Fintype β), Surjective f ↔ Nat.card α = Nat.card β
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofFinite β