awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Fintype α
⊢ #(Finset α) = HPow.hPow (α := Cardinal.{u}) 2 (Fintype.card α)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ succ (↑n : Cardinal.{u_1}) = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1

Tactic:
(succ_le_of_lt ?_).antisymm (add_one_le_of_lt <| lt_succ _)

Premises used: LE.le.antisymm, Order.succ_le_of_lt, Order.lt_succ, Cardinal.add_one_le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
refine : (↑n : Cardinal.{u_1}) < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
⊢ succ (↑n : Cardinal.{u_1}) = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1

Tactic:
refine (succ_le_of_lt ?_).antisymm (add_one_le_of_lt <| lt_succ _)

Premises used: LE.le.antisymm, Order.succ_le_of_lt, Order.lt_succ, Cardinal.add_one_le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
rw : LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑n.succ : Cardinal.{u_1})
⊢ (↑n : Cardinal.{u_1}) < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1

Tactic:
rw [← Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑n.succ : Cardinal.{u_1})

Tactic:
Nat.cast_lt.2 (Nat.lt_succ_self _)

Premises used: Iff.mpr, Nat.lt_succ_self, Nat.cast_lt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑n.succ : Cardinal.{u_1})

Tactic:
exact Nat.cast_lt.2 (Nat.lt_succ_self _)

Premises used: Iff.mpr, Nat.lt_succ_self, Nat.cast_lt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n.succ : Cardinal.{u_1}) (succ (↑n : Cardinal.{u_1}))

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
c : Cardinal.{u_1}
rw : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔ succ (↑n : Cardinal.{u_1}) ≤ c
rw₁ rw₂ :
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔
    HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ≤ c ↔ (↑n : Cardinal.{u_1}) < c

Tactic:
rw [← Order.succ_le_iff, succ_natCast]

Premises used: Cardinal.succ_natCast, Order.succ_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
c : Cardinal.{u_1}
rw : c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ c < succ (↑n : Cardinal.{u_1})
rw₁ rw₂ :
  c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔
    c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
⊢ c < HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 ↔ c ≤ (↑n : Cardinal.{u_1})

Tactic:
rw [← Order.lt_succ_iff, succ_natCast]

Premises used: Cardinal.succ_natCast, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) 1 ≤ c ↔ (↑1 : Cardinal.{u_1}) < c

Tactic:
natCast_add_one_le_iff

Premises used: Cardinal.natCast_add_one_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : 2 = HAdd.hAdd (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) 1
⊢ 2 ≤ c ↔ 1 < c

Tactic:
convert! natCast_add_one_le_iff

Premises used: Cardinal.natCast_add_one_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h h₁ h₂ h₃ : 2 = HAdd.hAdd (α := ℕ) 1 1
⊢ 2 = HAdd.hAdd (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) 1

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HAdd.hAdd (α := ℕ) 0 1 = 1
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (succ 0) 1

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LT.lt (α := ℕ) 1 2
⊢ LT.lt.{u_1 + 1} (α := Cardinal.{u_1}) 1 2

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
inl : ∀ (hα : Finite α), ∃ (s : Finset α), n = s.card
inr : ∀ (hα : Infinite α), ∃ (s : Finset α), n = s.card
⊢ ∃ (s : Finset α), n = s.card

Tactic:
obtain hα | hα := finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα_1 : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.card.{u_1} (α := α) Finset.univ

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα_1 : Finite α
hα : Fintype α := Fintype.ofFinite α
inl : ∀ (t : Finset α) (h : (↑t.card : Cardinal.{u_1}) ≤ #α), ∃ (s : Finset α), t.card = s.card
⊢ ∃ (s : Finset α), n = s.card

Tactic:
obtain ⟨t, -, rfl⟩ := @Finset.exists_subset_card_eq α .univ n <| by simpa using h

Premises used: Finset.exists_subset_card_eq, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
hα_1 : Finite α
hα : Fintype α := Fintype.ofFinite α
t : Finset α
h : (↑t.card : Cardinal.{u_1}) ≤ #α
⊢ ∃ (s : Finset α), t.card = s.card

Tactic:
⟨t, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
hα_1 : Finite α
hα : Fintype α := Fintype.ofFinite α
t : Finset α
h : (↑t.card : Cardinal.{u_1}) ≤ #α
⊢ ∃ (s : Finset α), t.card = s.card

Tactic:
exact ⟨t, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα : Infinite α
inr : ∀ (s : Finset α) (hs : s.card = n), ∃ (s : Finset α), n = s.card
⊢ ∃ (s : Finset α), n = s.card

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n

Premises used: Infinite.exists_subset_card_eq
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα : Infinite α
s : Finset α
hs : s.card = n
⊢ ∃ (s : Finset α), n = s.card

Tactic:
⟨s, hs.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
hα : Infinite α
s : Finset α
hs : s.card = n
⊢ ∃ (s : Finset α), n = s.card

Tactic:
exact ⟨s, hs.symm⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
h : (↑n : Cardinal.{u_1}) ≤ #α
⊢ ∃ (s : Finset α), n ≤ s.card

Tactic:
have ⟨s, eq⟩ := exists_finset_eq_card h
  ⟨s, eq.le⟩

Premises used: Exists, _private.0.Cardinal.exists_finset_le_card.match_1, Cardinal.exists_finset_eq_card, Eq.le, LE.le, Exists.intro, Finset.card
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
H : ∀ (s : Finset α), s.card ≤ n
contrapose! : ∀ (H : (↑n : Cardinal.{u}) < #α), ∃ (s : Finset α), n < s.card
⊢ #α ≤ (↑n : Cardinal.{u})

Tactic:
contrapose! H
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
H : (↑n : Cardinal.{u}) < #α
apply : (↑(n + 1) : Cardinal.{u}) ≤ #α
⊢ ∃ (s : Finset α), n < s.card

Tactic:
apply exists_finset_le_card α (n + 1)

Premises used: HAdd.hAdd, Cardinal.exists_finset_le_card, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
H : (↑n : Cardinal.{u}) < #α
⊢ (↑(n + 1) : Cardinal.{u}) ≤ #α

Tactic:
simpa using H
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
hb : succ 1 ≤ b
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (succ 1) 2

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
hb : 1 < b
⊢ 2 ≤ b

Tactic:
rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a

Tactic:
(cantor a).trans_le (power_le_power_right hb)

Premises used: Cardinal.power_le_power_right, Cardinal.cantor, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a

Tactic:
exact (cantor a).trans_le (power_le_power_right hb)

Premises used: Cardinal.power_le_power_right, Cardinal.cantor, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
rw : succ 0 ≤ c ↔ 0 < c
rw₁ rw₂ : 0 < c ↔ 0 < c
⊢ 1 ≤ c ↔ 0 < c

Tactic:
rw [← succ_zero, succ_le_iff]

Premises used: Order.succ_le_iff, Cardinal.succ_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
rw : 0 < c ↔ c ≠ 0
rw₁ rw₂ : c ≠ 0 ↔ c ≠ 0
⊢ 1 ≤ c ↔ c ≠ 0

Tactic:
rw [Cardinal.one_le_iff_pos, pos_iff_ne_zero]

Premises used: Cardinal.one_le_iff_pos, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
⊢ c < 1 ↔ c = 0

Tactic:
simpa using lt_succ_bot_iff (a := c)

Premises used: Order.lt_succ_bot_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
⊢ c ≤ 1 ↔ c = 0 ∨ c = 1

Tactic:
simpa using le_succ_bot_iff (a := c)

Premises used: Order.le_succ_bot_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
rw : Nonempty (Fin (n + 1) ↪ ℕ)
⊢ (↑n : Cardinal.{u}) < ℵ₀

Tactic:
rw [← natCast_add_one_le_iff, ← Nat.cast_add_one, ← lift_mk_fin, aleph0, lift_mk_le.{u}]

Premises used: Cardinal.natCast_add_one_le_iff, Cardinal.lift_mk_fin, Cardinal.aleph0, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ Nonempty (Fin (n + 1) ↪ ℕ)

Tactic:
⟨⟨(↑), fun a b => Fin.ext⟩⟩

Premises used: Function.Embedding.mk, Fin.ext, Fin.val, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ Nonempty (Fin (n + 1) ↪ ℕ)

Tactic:
exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u}) < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u}) ≤ ℵ₀

Tactic:
natCast_lt_aleph0.le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ ℵ₀

Tactic:
natCast_le_aleph0

Premises used: Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ 1 < ℵ₀

Tactic:
simpa using natCast_lt_aleph0 (n := 1)

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ 1 ≤ ℵ₀

Tactic:
one_lt_aleph0.le

Premises used: Cardinal.one_lt_aleph0, LT.lt.le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
rcases :
  ∀ (c : Cardinal.{0}) (h' : c < #ℕ) (h : lift.{u_1, 0} c < ℵ₀), ∃ (n : ℕ), lift.{u_1, 0} c = (↑n : Cardinal.{u_1})
⊢ ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})

Tactic:
rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩

Premises used: Cardinal.lt_lift_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{0}
h' : c < #ℕ
h : lift.{u_1, 0} c < ℵ₀
rcases :
  ∀ (S : Set ℕ) (h' : #(↑S : Type) < #ℕ) (h : lift.{u_1, 0} #(↑S : Type) < ℵ₀),
    ∃ (n : ℕ), lift.{u_1, 0} #(↑S : Type) = (↑n : Cardinal.{u_1})
⊢ ∃ (n : ℕ), lift.{u_1, 0} c = (↑n : Cardinal.{u_1})

Tactic:
rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩

Premises used: Cardinal.le_mk_iff_exists_set, And.left, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
this : S.Finite
⊢ S.Finite

Tactic:
this
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : Cardinal.lift.{u_1, 0} #(↑S : Type) < ℵ₀
this : S.Finite
lift :
  ∀ (S : Finset ℕ) (h' : #(↑(↑S : Set ℕ) : Type) < #ℕ) (h : Cardinal.lift.{u_1, 0} #(↑(↑S : Set ℕ) : Type) < ℵ₀),
    ∃ (n : ℕ), Cardinal.lift.{u_1, 0} #(↑(↑S : Set ℕ) : Type) = (↑n : Cardinal.{u_1})
⊢ ∃ (n : ℕ), Cardinal.lift.{u_1, 0} #(↑S : Type) = (↑n : Cardinal.{u_1})

Tactic:
lift S to Finset ℕ using this

Premises used: Finset, Nat
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Finset ℕ
h' : #(↑(↑S : Set ℕ) : Type) < #ℕ
h : lift.{u_1, 0} #(↑(↑S : Set ℕ) : Type) < ℵ₀
⊢ ∃ (n : ℕ), lift.{u_1, 0} #(↑(↑S : Set ℕ) : Type) = (↑n : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
suffices : S.Finite
⊢ ∃ (n : ℕ), lift.{u_1, 0} #(↑S : Type) = (↑n : Cardinal.{u_1})

Tactic:
suffices S.Finite by
      lift S to Finset ℕ using this
      simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
contrapose! : ∀ (h' : S.Infinite), #ℕ ≤ #(↑S : Type)
⊢ S.Finite

Tactic:
contrapose! h'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
h' : S.Infinite
⊢ Infinite (↑S : Type)

Tactic:
haveI := Infinite.to_subtype h'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
h' : S.Infinite
this : Infinite (↑S : Type)
⊢ #ℕ ≤ #(↑S : Type)

Tactic:
⟨Infinite.natEmbedding S⟩

Premises used: Set.Elem, Nonempty.intro, Infinite.natEmbedding
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
S : Set ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
h' : S.Infinite
this : Infinite (↑S : Type)
⊢ #ℕ ≤ #(↑S : Type)

Tactic:
exact ⟨Infinite.natEmbedding S⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
obtain : ∀ (n : ℕ) (hn : c = (↑n : Cardinal.{u_1})), succ c = c + 1
⊢ succ c = c + 1

Tactic:
obtain ⟨n, hn⟩ := Cardinal.lt_aleph0.mp h

Premises used: Iff.mp, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = (↑n : Cardinal.{u_1})
rw : succ (↑n : Cardinal.{u_1}) = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
rw₁ rw₂ :
  HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
⊢ succ c = c + 1

Tactic:
rw [hn, succ_natCast]

Premises used: Cardinal.succ_natCast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : ∀ (n : ℕ), (↑n : Cardinal.{u_1}) ≤ c
hn : c < ℵ₀
rcases :
  ∀ (n : ℕ) (h : ∀ (n_1 : ℕ), LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑n_1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1}))
    (hn : (↑n : Cardinal.{u_1}) < ℵ₀), False
⊢ False

Tactic:
rcases lt_aleph0.1 hn with ⟨n, rfl⟩

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : ∀ (n_1 : ℕ), LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑n_1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
hn : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ False

Tactic:
(Nat.lt_succ_self _).not_ge (Nat.cast_le.1 (h (n + 1)))

Premises used: Nat.lt_succ_self, HAdd.hAdd, Iff.mp, Nat.cast_le, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : ∀ (n_1 : ℕ), LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑n_1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
hn : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ False

Tactic:
exact (Nat.lt_succ_self _).not_ge (Nat.cast_le.1 (h (n + 1)))

Premises used: Nat.lt_succ_self, HAdd.hAdd, Iff.mp, Nat.cast_le, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
rcases : ∀ (n : ℕ) (ha : (↑n : Cardinal.{u_1}) < ℵ₀), succ (↑n : Cardinal.{u_1}) < ℵ₀
⊢ succ a < ℵ₀

Tactic:
rcases lt_aleph0.1 ha with ⟨n, rfl⟩

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
ha : (↑n : Cardinal.{u_1}) < ℵ₀
rw : (↑(n + 1) : Cardinal.{u_1}) < ℵ₀
⊢ succ (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
rw [succ_natCast, ← Nat.cast_add_one]

Premises used: Cardinal.succ_natCast, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
ha : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ (↑(n + 1) : Cardinal.{u_1}) < ℵ₀

Tactic:
apply natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
rw : ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀
⊢ IsSuccLimit ℵ₀

Tactic:
rw [Cardinal.isSuccLimit_iff]

Premises used: Cardinal.isSuccLimit_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀

Tactic:
⟨aleph0_ne_zero, isSuccPrelimit_aleph0⟩

Premises used: And.intro, Cardinal.isSuccPrelimit_aleph0, Cardinal.aleph0_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀

Tactic:
exact ⟨aleph0_ne_zero, isSuccPrelimit_aleph0⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : IsSuccLimit.{u + 1} (α := Cardinal.{u}) (↑n.succ : Cardinal.{u})
⊢ IsSuccLimit.{u + 1} (α := Cardinal.{u}) (succ (↑n : Cardinal.{u}))

Tactic:
rw [Nat.cast_succ, ← succ_natCast] at h

Premises used: Nat.cast_succ, Cardinal.succ_natCast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : IsSuccLimit.{u + 1} (α := Cardinal.{u}) (succ (↑n : Cardinal.{u}))
⊢ False

Tactic:
Order.not_isSuccLimit_succ _ h

Premises used: Order.not_isSuccLimit_succ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : IsSuccLimit.{u + 1} (α := Cardinal.{u}) (succ (↑n : Cardinal.{u}))
⊢ False

Tactic:
exact Order.not_isSuccLimit_succ _ h

Premises used: Order.not_isSuccLimit_succ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
obtain : ∀ (n : ℕ) (h : (↑n : Cardinal.{u_1}) < ℵ₀), ¬IsSuccLimit.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1})
⊢ ¬IsSuccLimit c

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 h

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ ¬IsSuccLimit.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1})

Tactic:
not_isSuccLimit_natCast n

Premises used: Cardinal.not_isSuccLimit_natCast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
h : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ ¬IsSuccLimit.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1})

Tactic:
exact not_isSuccLimit_natCast n

Premises used: Cardinal.not_isSuccLimit_natCast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : IsSuccLimit c
contrapose! : ∀ (h : c < ℵ₀), ¬IsSuccLimit c
⊢ ℵ₀ ≤ c

Tactic:
contrapose! h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Tactic:
not_isSuccLimit_of_lt_aleph0 h

Premises used: Cardinal.not_isSuccLimit_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Tactic:
exact not_isSuccLimit_of_lt_aleph0 h

Premises used: Cardinal.not_isSuccLimit_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ ℵ₀.IsStrongLimit

Tactic:
⟨aleph0_ne_zero, fun x hx ↦ ?_⟩

Premises used: Cardinal.IsStrongLimit.mk, Cardinal.aleph0_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
refine : ∀ (x : Cardinal.{u_1}) (hx : x < ℵ₀), HPow.hPow (α := Cardinal.{u_1}) 2 x < ℵ₀
⊢ ℵ₀.IsStrongLimit

Tactic:
refine ⟨aleph0_ne_zero, fun x hx ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
x : Cardinal.{u_1}
hx : x < ℵ₀
obtain :
  ∀ (n : ℕ) (hx : (↑n : Cardinal.{u_1}) < ℵ₀),
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 2 (↑n : Cardinal.{u_1}) < ℵ₀
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < ℵ₀

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hx

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
hx : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 2 (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
mod_cast natCast_lt_aleph0

Premises used: congrArg, cast, Cardinal.aleph0, Cardinal.natCast_lt_aleph0, LT.lt, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_pow._simp_1
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
hx : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 2 (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
exact mod_cast natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
H : c.IsStrongLimit
⊢ ℵ₀ ≤ c

Tactic:
aleph0_le_of_isSuccLimit H.isSuccLimit

Premises used: Cardinal.IsStrongLimit.isSuccLimit, Cardinal.aleph0_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
inst : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i) (↑n : Cardinal.{v})
rw : ∃ (i : ι), f i = ⨆ (i : ι), f i
⊢ ∃ (i : ι), f i = (↑n : Cardinal.{v})

Tactic:
rw [← h]
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
inst : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i) (↑n : Cardinal.{v})
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
exists_eq_ciSup_of_not_isSuccLimit hf (h ▸ not_isSuccLimit_natCast n)

Premises used: exists_eq_ciSup_of_not_isSuccLimit, Eq.rec, Cardinal.not_isSuccLimit_natCast, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
inst : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i) (↑n : Cardinal.{v})
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
exact exists_eq_ciSup_of_not_isSuccLimit hf (h ▸ not_isSuccLimit_natCast n)

Premises used: exists_eq_ciSup_of_not_isSuccLimit, Eq.rec, Cardinal.not_isSuccLimit_natCast, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
x : Cardinal.{u_1}
⊢ Membership.mem (γ := Set Cardinal.{u_1}) (range Nat.cast) x ↔ x ∈ Iio ℵ₀

Tactic:
simp only [mem_Iio, mem_range, eq_comm, lt_aleph0]

Premises used: Set.mem_range, Set.mem_Iio, eq_comm, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
rw : #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
rw₁ : lift.{0, u} #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
rw₂ rw₃ : Nonempty.{max 1 (u + 1)} (α ≃ Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
⊢ #α = (↑n : Cardinal.{u}) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)

Tactic:
rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']

Premises used: Cardinal.mk, Cardinal.lift_mk_fin, Cardinal.lift_mk_eq', Cardinal.lift_uzero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #α < ℵ₀ ↔ Finite α

Tactic:
simp only [lt_aleph0, mk_eq_nat_iff, finite_iff_exists_equiv_fin]

Premises used: Cardinal.mk_eq_nat_iff, Cardinal.lt_aleph0, finite_iff_exists_equiv_fin
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #α < ℵ₀ ↔ Nonempty.{u + 1} (Fintype α)

Tactic:
lt_aleph0_iff_finite.trans (finite_iff_nonempty_fintype _)

Premises used: Cardinal.lt_aleph0_iff_finite, finite_iff_nonempty_fintype, Iff.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Finite α
⊢ #α < ℵ₀

Tactic:
lt_aleph0_iff_finite.2 ‹_›

Premises used: Iff.mpr, Cardinal.lt_aleph0_iff_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S : Set α
⊢ #(↑S : Type u) < ℵ₀ ↔ S.Finite

Tactic:
lt_aleph0_iff_finite.trans finite_coe_iff

Premises used: Set.finite_coe_iff, Cardinal.lt_aleph0_iff_finite, Iff.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
p : α → Prop
⊢ #{ x : α // p x } < ℵ₀ ↔ Set.Finite.{u} (α := α) {x : α | p x}

Tactic:
lt_aleph0_iff_set_finite

Premises used: Set.Mem, setOf, Cardinal.lt_aleph0_iff_set_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
rw : #α ≤ ℵ₀ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
rw₁ : #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
rw₂ : lift.{0, u} #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
rw₃ rw₄ : Nonempty.{max 1 (u + 1)} (α ↪ ℕ) ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
⊢ #α ≤ ℵ₀ ↔ Countable α

Tactic:
rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']

Premises used: Cardinal.mk, Cardinal.aleph0, Cardinal.lift_uzero, Cardinal.lift_mk_le', countable_iff_nonempty_embedding
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Countable α
⊢ #α ≤ ℵ₀

Tactic:
mk_le_aleph0_iff.mpr ‹_›

Premises used: Iff.mpr, Cardinal.mk_le_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
⊢ #(↑s : Type u) ≤ ℵ₀ ↔ s.Countable

Tactic:
mk_le_aleph0_iff

Premises used: Cardinal.mk_le_aleph0_iff, Set.Countable
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
p : α → Prop
⊢ #{ x : α // p x } ≤ ℵ₀ ↔ Set.Countable.{u} (α := α) {x : α | p x}

Tactic:
le_aleph0_iff_set_countable

Premises used: Cardinal.le_aleph0_iff_set_countable, Set.Mem, setOf
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
rw : ¬#α ≤ ℵ₀ ↔ Uncountable α
rw₁ : ¬#α ≤ ℵ₀ ↔ ¬Countable α
rw₂ : #α ≤ ℵ₀ ↔ Countable α
rw₃ rw₄ : Countable α ↔ Countable α
⊢ ℵ₀ < #α ↔ Uncountable α

Tactic:
rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]

Premises used: not_le, not_iff_not, Cardinal.mk_le_aleph0_iff, not_countable_iff