awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} (↑m : Cardinal.{v}) = lift.{u, v} x ↔ (↑m : Cardinal.{v}) = x
rw₁ rw₂ : (↑m : Cardinal.{v}) = x ↔ (↑m : Cardinal.{v}) = x
⊢ (↑m : Cardinal.{max u v}) = lift.{u, v} x ↔ (↑m : Cardinal.{v}) = x

Tactic:
rw [← lift_ofENat.{u, v}, lift_inj]

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ range ofENat = Iic ℵ₀

Tactic:
(range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_

Premises used: Iff.mpr, Cardinal.ofENat_le_aleph0, Cardinal, setOf, Quotient, HasSubset.Subset.antisymm, Set.Iic, Set.range_subset_iff
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
refine : ∀ (x : Cardinal.{u_1}) (hx : x ≤ ℵ₀), x ∈ range ofENat
⊢ range ofENat = Iic ℵ₀

Tactic:
refine (range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_

Premises used: Iff.mpr, Cardinal.ofENat_le_aleph0, HasSubset.Subset.antisymm, Set.range_subset_iff
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
inl : ∀ (hlt : x < ℵ₀), x ∈ range ofENat
inr : ∀ (hx : ℵ₀ ≤ ℵ₀), ℵ₀ ∈ range ofENat
⊢ x ∈ range ofENat

Tactic:
rcases hx.lt_or_eq with hlt | rfl

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x < ℵ₀

Tactic:
hlt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
inl : ∀ (x : ℕ) (hx : (↑x : Cardinal.{u_1}) ≤ ℵ₀), (↑x : Cardinal.{u_1}) ∈ range ofENat
⊢ x ∈ range ofENat

Tactic:
lift x to ℕ using hlt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : ℕ
hx : (↑x : Cardinal.{u_1}) ≤ ℵ₀
⊢ (↑x : Cardinal.{u_1}) ∈ range ofENat

Tactic:
mem_range_self (x : ℕ∞)

Premises used: Set.mem_range_self, Set.Mem, Nat.cast, Cardinal.ofENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : ℕ
hx : (↑x : Cardinal.{u_1}) ≤ ℵ₀
⊢ (↑x : Cardinal.{u_1}) ∈ range ofENat

Tactic:
exact mem_range_self (x : ℕ∞)

Premises used: Set.mem_range_self, Nat.cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
mem_range_self (⊤ : ℕ∞)

Premises used: Set.mem_range_self, Set.Mem, Cardinal.ofENat, Top.top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
exact mem_range_self (⊤ : ℕ∞)

Premises used: Set.mem_range_self, Top.top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ
⊢ toENatAux.{u_1} (↑n : Cardinal.{u_1}) = (↑n : ℕ∞)

Tactic:
Nat.cast_injective.extend_apply ..

Premises used: Function.Injective.extend_apply, Nat.cast_injective, Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ toENatAux.{u_1} 0 = 0

Tactic:
toENatAux_nat 0

Premises used: Cardinal.toENatAux_nat, WithTop.some, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a.toENatAux = ⊤

Tactic:
extend_apply' _ _ _ fun ⟨_n, hn⟩ ↦ ha.not_gt <| hn ▸ natCast_lt_aleph0

Premises used: False, _private.0.Cardinal.toENatAux_eq_top.match_1, Eq.rec, Cardinal.natCast_lt_aleph0, LE.le.not_gt, Function.extend_apply', Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ x < ℵ₀

Tactic:
hx
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
x : Cardinal.{u_1}
hx : x < ℵ₀
inl : ∀ (x : ℕ), (↑n : Cardinal.{u_1}) ≤ (↑x : Cardinal.{u_1}) ↔ n ≤ toENatAux.{u_1} (↑x : Cardinal.{u_1})
⊢ (↑n : Cardinal.{u_1}) ≤ x ↔ n ≤ x.toENatAux

Tactic:
lift x to ℕ using hx
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
x : ℕ
⊢ (↑n : Cardinal.{u_1}) ≤ (↑x : Cardinal.{u_1}) ↔ n ≤ toENatAux.{u_1} (↑x : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
x : Cardinal.{u_1}
hx : ℵ₀ ≤ x
⊢ (↑n : Cardinal.{u_1}) ≤ x ↔ n ≤ x.toENatAux

Tactic:
simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

Premises used: Cardinal.toENatAux_eq_top, Cardinal.ofENat_le_aleph0, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
x : Cardinal.{u_1}
⊢ x < ℵ₀ ∨ ℵ₀ ≤ x

Tactic:
cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

Premises used: Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
n : ℕ
hx : x < ℵ₀
⊢ x < ℵ₀

Tactic:
hx
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
n : ℕ
hx : x < ℵ₀
inl :
  ∀ (x : ℕ),
    toENatAux.{u_1} (↑x : Cardinal.{u_1}) ≤ (↑n : ℕ∞) ↔
      LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑x : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
⊢ x.toENatAux ≤ (↑n : ℕ∞) ↔ x ≤ (↑n : Cardinal.{u_1})

Tactic:
lift x to ℕ using hx
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n x : ℕ
⊢ toENatAux.{u_1} (↑x : Cardinal.{u_1}) ≤ (↑n : ℕ∞) ↔
    LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑x : Cardinal.{u_1}) (↑n : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
n : ℕ
hx : ℵ₀ ≤ x
⊢ x.toENatAux ≤ (↑n : ℕ∞) ↔ x ≤ (↑n : Cardinal.{u_1})

Tactic:
simp [toENatAux_eq_top hx, natCast_lt_aleph0.trans_le hx]

Premises used: Cardinal.toENatAux_eq_top, Cardinal.natCast_lt_aleph0, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
n : ℕ
⊢ x < ℵ₀ ∨ ℵ₀ ≤ x

Tactic:
cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, natCast_lt_aleph0.trans_le hx]

Premises used: Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux = (↑n : ℕ∞) ↔ x = (↑n : Cardinal.{u_1})

Tactic:
simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]

Premises used: Cardinal.toENatAux_gc, le_antisymm_iff, Cardinal.ofENat_nat, Cardinal.toENatAux_le_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{u_1}
⊢ x.toENatAux = 0 ↔ x = 0

Tactic:
toENatAux_eq_nat

Premises used: Cardinal.toENatAux_eq_nat, WithTop.some
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
inr :
  ∀ (this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux) (hle : ¬x ≤ y),
    toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
wlog : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux

Tactic:
wlog hle : x ≤ y
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
inr : toENatAux.{u} (y * x) = x.toENatAux * y.toENatAux
inr₁ : y.toENatAux * x.toENatAux = x.toENatAux * y.toENatAux
inr₂ inr₃ : x.toENatAux * y.toENatAux = x.toENatAux * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux

Tactic:
rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]

Premises used: le_of_not_ge, mul_comm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ x < ℵ₀

Tactic:
hle.trans_lt hy

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
inl :
  ∀ (x : ℕ) (hle : (↑x : Cardinal.{u}) ≤ y),
    toENatAux.{u} ((↑x : Cardinal.{u}) * y) = toENatAux.{u} (↑x : Cardinal.{u}) * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux

Tactic:
lift x to ℕ using hle.trans_lt hy

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : (↑x : Cardinal.{u}) ≤ y
⊢ y < ℵ₀

Tactic:
hy
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : (↑x : Cardinal.{u}) ≤ y
inl :
  ∀ (y : ℕ) (hle : LE.le.{u + 1} (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})),
    toENatAux.{u} (HMul.hMul (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})) =
      toENatAux.{u} (↑x : Cardinal.{u}) * toENatAux.{u} (↑y : Cardinal.{u})
⊢ toENatAux.{u} ((↑x : Cardinal.{u}) * y) = toENatAux.{u} (↑x : Cardinal.{u}) * y.toENatAux

Tactic:
lift y to ℕ using hy
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : ℕ
hle : LE.le.{u + 1} (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})
⊢ toENatAux.{u} (HMul.hMul (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})) =
    toENatAux.{u} (↑x : Cardinal.{u}) * toENatAux.{u} (↑y : Cardinal.{u})

Tactic:
simp only [← Nat.cast_mul, toENatAux_nat]

Premises used: Cardinal.toENatAux_nat, Nat.cast_mul
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
inr : ∀ (hle : 0 ≤ y), toENatAux.{u} (0 * y) = toENatAux.{u} 0 * y.toENatAux
inr₁ : ∀ (hx : x ≠ 0), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
y : Cardinal.{u}
hy : ℵ₀ ≤ y
hle : 0 ≤ y
⊢ toENatAux.{u} (0 * y) = toENatAux.{u} 0 * y.toENatAux

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
inr : toENatAux.{u} (x * y) = x.toENatAux * ⊤
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux

Tactic:
simp only [toENatAux_eq_top hy]

Premises used: Cardinal.toENatAux_eq_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
inr : x.toENatAux ≠ 0
inr₁ : ℵ₀ ≤ x * y
⊢ toENatAux.{u} (x * y) = x.toENatAux * ⊤

Tactic:
rw [toENatAux_eq_top, ENat.mul_top]

Premises used: Cardinal.toENatAux_eq_top, ENat.mul_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
inr : ¬x.toENatAux = 0
inr₁ inr₂ inr₃ inr₄ : ¬x = 0
⊢ x.toENatAux ≠ 0

Tactic:
rwa [Ne, toENatAux_eq_zero]

Premises used: Ne, Cardinal.toENatAux_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y

Tactic:
le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero, le_mul_of_one_le_of_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y

Tactic:
exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero, le_mul_of_one_le_of_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
⊢ y < ℵ₀ ∨ ℵ₀ ≤ y

Tactic:
cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_mul, toENatAux_nat]
    | inr hy =>
      rcases eq_or_ne x 0 with rfl | hx
      · simp
      · simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

Premises used: Cardinal.toENatAux_eq_top, Cardinal.toENatAux_nat, Ne, Cardinal.aleph0, Nat.cast_mul, Cardinal.toENatAux_eq_zero, eq_or_ne, lt_or_ge, OfNat.ofNat, ENat.mul_top, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
inr :
  ∀ (this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux) (hle : ¬x ≤ y),
    toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
wlog : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux

Tactic:
wlog hle : x ≤ y
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
inr : toENatAux.{u} (y + x) = x.toENatAux + y.toENatAux
inr₁ : y.toENatAux + x.toENatAux = x.toENatAux + y.toENatAux
inr₂ inr₃ : x.toENatAux + y.toENatAux = x.toENatAux + y.toENatAux
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux

Tactic:
rw [add_comm, this y x (le_of_not_ge hle), add_comm]

Premises used: le_of_not_ge, add_comm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
inl :
  ∀ (x : ℕ) (hle : (↑x : Cardinal.{u}) ≤ y),
    toENatAux.{u} ((↑x : Cardinal.{u}) + y) = toENatAux.{u} (↑x : Cardinal.{u}) + y.toENatAux
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux

Tactic:
lift x to ℕ using hle.trans_lt hy

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : (↑x : Cardinal.{u}) ≤ y
inl :
  ∀ (y : ℕ) (hle : LE.le.{u + 1} (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})),
    toENatAux.{u} (HAdd.hAdd (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})) =
      toENatAux.{u} (↑x : Cardinal.{u}) + toENatAux.{u} (↑y : Cardinal.{u})
⊢ toENatAux.{u} ((↑x : Cardinal.{u}) + y) = toENatAux.{u} (↑x : Cardinal.{u}) + y.toENatAux

Tactic:
lift y to ℕ using hy
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : ℕ
hle : LE.le.{u + 1} (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})
⊢ toENatAux.{u} (HAdd.hAdd (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})) =
    toENatAux.{u} (↑x : Cardinal.{u}) + toENatAux.{u} (↑y : Cardinal.{u})

Tactic:
simp only [← Nat.cast_add, toENatAux_nat]

Premises used: Cardinal.toENatAux_nat, Nat.cast_add
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
inr : toENatAux.{u} (x + y) = ⊤
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux

Tactic:
simp only [toENatAux_eq_top hy, add_top]

Premises used: Cardinal.toENatAux_eq_top, add_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ toENatAux.{u} (x + y) = ⊤

Tactic:
toENatAux_eq_top <| le_add_left hy

Premises used: Cardinal.toENatAux_eq_top, le_add_left
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ toENatAux.{u} (x + y) = ⊤

Tactic:
exact toENatAux_eq_top <| le_add_left hy

Premises used: Cardinal.toENatAux_eq_top, le_add_left
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x y : Cardinal.{u}
hle : x ≤ y
⊢ y < ℵ₀ ∨ ℵ₀ ≤ y

Tactic:
cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_add, toENatAux_nat]
    | inr hy =>
      simp only [toENatAux_eq_top hy, add_top]
      exact toENatAux_eq_top <| le_add_left hy

Premises used: Cardinal.toENatAux_eq_top, add_top, Cardinal.toENatAux_nat, Cardinal.aleph0, Nat.cast_add, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ GaloisConnection ofENat (⇑toENat : (a : Cardinal.{u_1}) → ℕ∞)

Tactic:
toENatAux_gc

Premises used: dite, Cardinal.toENatAux_gc, Function.extend, Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
⊢ (toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑n : Cardinal.{u_1}) = n

Tactic:
toENatAux_ofENat n

Premises used: dite, Function.extend, Cardinal.toENatAux_ofENat, Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ (⇑toENat : (a : Cardinal.{u_1}) → ℕ∞) ∘ ofENat = id

Tactic:
funext toENat_ofENat

Premises used: Cardinal.toENat_ofENat, funext
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
simp : ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1
⊢ StrictMonoOn (β := ℕ∞) (⇑toENat : (a : Cardinal.{u_1}) → ℕ∞) (Iic ℵ₀)

Tactic:
simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]

Premises used: Cardinal.toENat_ofENat, Cardinal.range_ofENat, Set.forall_mem_range, Cardinal.ofENat_lt_ofENat, StrictMonoOn
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1

Tactic:
fun _ _ ↦ id

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1

Tactic:
exact fun _ _ ↦ id

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ InjOn (β := ℕ∞) (⇑toENat : (a : Cardinal.{u_1}) → ℕ∞) (Iic ℵ₀)

Tactic:
toENat_strictMonoOn.injOn

Premises used: StrictMonoOn.injOn, Cardinal.toENat_strictMonoOn
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
a : Cardinal.{u_1}
⊢ (↑((toENat : (a : Cardinal.{u_1}) → ℕ∞) a) : Cardinal.{u_1}) ≤ a

Tactic:
enat_gc.l_u_le _

Premises used: Cardinal.enat_gc, GaloisConnection.l_u_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
a : Cardinal.{u_1}
rw : (∃ (b : ℕ∞), a = (↑b : Cardinal.{u_1})) ↔ a ≤ ℵ₀
⊢ (↑((toENat : (a : Cardinal.{u_1}) → ℕ∞) a) : Cardinal.{u_1}) = a ↔ a ≤ ℵ₀

Tactic:
rw [eq_comm, ← enat_gc.exists_eq_l]

Premises used: GaloisConnection.exists_eq_l, eq_comm, Cardinal.enat_gc
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
a : Cardinal.{u_1}
⊢ (∃ (b : ℕ∞), a = (↑b : Cardinal.{u_1})) ↔ a ≤ ℵ₀

Tactic:
simpa only [mem_range, eq_comm] using Set.ext_iff.1 range_ofENat a

Premises used: Set.mem_range, Cardinal.range_ofENat, eq_comm, Iff.mp, Set.ext_iff
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑n : Cardinal.{u_1}) : ℕ∞) ((↑n : ℕ∞) : ℕ∞)

Tactic:
map_natCast _ n

Premises used: map_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) (OfNat.ofNat n) : ℕ∞) (OfNat.ofNat n : ℕ∞)

Tactic:
toENat_nat _

Premises used: Cardinal.toENat_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c ≤ (↑n : Cardinal.{u})

Tactic:
toENatAux_le_nat

Premises used: dite, Function.extend, Cardinal.toENatAux_le_nat, Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (1 : ℕ∞) ↔ c ≤ 1

Tactic:
toENat_le_natCast

Premises used: WithTop.some, Cardinal.toENat_le_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (OfNat.ofNat n : ℕ∞) ↔ c ≤ OfNat.ofNat n

Tactic:
toENat_le_natCast

Premises used: Cardinal.toENat_le_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c c' : Cardinal.{u}
hc : c ≤ ℵ₀
⊢ c ≤ ℵ₀

Tactic:
hc
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c c' : Cardinal.{u}
hc : c ≤ ℵ₀
lift :
  ∀ (c : ℕ∞),
    LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)
        ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔
      (↑c : Cardinal.{u}) ≤ c'
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔ c ≤ c'

Tactic:
lift c to ℕ∞ using hc
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c' : Cardinal.{u}
c : ℕ∞
simp_rw : c ≤ (toENat : (a : Cardinal.{u}) → ℕ∞) c' ↔ (↑c : Cardinal.{u}) ≤ c'
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔
    (↑c : Cardinal.{u}) ≤ c'

Tactic:
simp_rw [toENat_ofENat, enat_gc _]

Premises used: Cardinal.toENat_ofENat, Cardinal.enat_gc
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c c' : Cardinal.{u}
hc' : c' < ℵ₀
⊢ c' < ℵ₀

Tactic:
hc'
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c c' : Cardinal.{u}
hc' : c' < ℵ₀
lift :
  ∀ (c' : ℕ),
    LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)
        ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c' : Cardinal.{u}) : ℕ∞) ↔
      c ≤ (↑c' : Cardinal.{u})
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔ c ≤ c'

Tactic:
lift c' to ℕ using hc'
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
c' : ℕ
simp_rw : LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑c' : ℕ∞) : ℕ∞) ↔ c ≤ (↑c' : Cardinal.{u})
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c' : Cardinal.{u}) : ℕ∞) ↔
    c ≤ (↑c' : Cardinal.{u})

Tactic:
simp_rw [toENat_nat, ← toENat_le_natCast]

Premises used: Cardinal.toENat_le_natCast, Cardinal.toENat_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c c' : Cardinal.{u}
hc : c ≤ ℵ₀
hc' : c' ≤ ℵ₀
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔ c = c'

Tactic:
toENat_strictMonoOn.injOn.eq_iff hc hc'

Premises used: StrictMonoOn.injOn, Set.InjOn.eq_iff, Cardinal.toENat_strictMonoOn
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
rw :
  LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑n : Cardinal.{u}) : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔
    (↑n : Cardinal.{u}) ≤ c
rw₁ rw₂ : (↑n : Cardinal.{u}) ≤ c ↔ (↑n : Cardinal.{u}) ≤ c
⊢ LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u}) ≤ c

Tactic:
rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]

Premises used: Cardinal.toENat_le_iff_of_le_aleph0, Cardinal.toENat_nat, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ LE.le (α := ℕ∞) (1 : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ 1 ≤ c

Tactic:
natCast_le_toENat

Premises used: WithTop.some, Cardinal.natCast_le_toENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ LE.le (α := ℕ∞) (OfNat.ofNat n : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ OfNat.ofNat n ≤ c

Tactic:
natCast_le_toENat

Premises used: Cardinal.natCast_le_toENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
⊢ LT.lt (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c < (↑n : Cardinal.{u})

Tactic:
simp [← not_le]

Premises used: not_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ LT.lt (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (1 : ℕ∞) ↔ c < 1

Tactic:
toENat_lt_natCast

Premises used: Cardinal.toENat_lt_natCast, WithTop.some
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ LT.lt (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (OfNat.ofNat n : ℕ∞) ↔ c < OfNat.ofNat n

Tactic:
toENat_lt_natCast

Premises used: Cardinal.toENat_lt_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
⊢ LT.lt (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u}) < c

Tactic:
simp [← not_le]

Premises used: not_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ LT.lt (α := ℕ∞) (1 : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ 1 < c

Tactic:
natCast_lt_toENat

Premises used: Cardinal.natCast_lt_toENat, WithTop.some
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ LT.lt (α := ℕ∞) (OfNat.ofNat n : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ OfNat.ofNat n < c

Tactic:
natCast_lt_toENat

Premises used: Cardinal.natCast_lt_toENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c = (↑n : Cardinal.{u})

Tactic:
toENatAux_eq_nat

Premises used: Cardinal.toENatAux_eq_nat, dite, Function.extend, Cardinal.toENatAux
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (0 : ℕ∞) ↔ c = 0

Tactic:
toENat_eq_natCast

Premises used: WithTop.some, Cardinal.toENat_eq_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (1 : ℕ∞) ↔ c = 1

Tactic:
toENat_eq_natCast

Premises used: WithTop.some, Cardinal.toENat_eq_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (OfNat.ofNat n : ℕ∞) ↔ c = OfNat.ofNat n

Tactic:
toENat_eq_natCast

Premises used: Cardinal.toENat_eq_natCast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
⊢ Eq (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u}) = c

Tactic:
simp [eq_comm (a := Nat.cast _)]

Premises used: eq_comm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℕ∞) (OfNat.ofNat n : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ OfNat.ofNat n = c

Tactic:
natCast_eq_toENat

Premises used: Cardinal.natCast_eq_toENat