awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr : ∀ (hle : 0 ≤ y), toENatAux.{u} (0 * y) = toENatAux.{u} 0 * y.toENatAux
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x, hle
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
inr : ∀ (hle : 0 ≤ y), toENatAux.{u} (0 * y) = toENatAux.{u} 0 * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr₁ : ∀ (hx : x ≠ 0), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr : toENatAux.{u} (x * y) = x.toENatAux * ⊤
Tactic: simp only [toENatAux_eq_top hy]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ toENatAux.{u} (x * y) = x.toENatAux * ⊤
have inr : x.toENatAux ≠ 0
Tactic: rw [toENatAux_eq_top, ENat.mul_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
inr : x.toENatAux ≠ 0
⊢ toENatAux.{u} (x * y) = x.toENatAux * ⊤
have inr₁ : ℵ₀ ≤ x * y
Tactic: rw [toENatAux_eq_top, ENat.mul_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ x.toENatAux ≠ 0
have inr : ¬x.toENatAux = 0
Tactic: rwa [Ne, toENatAux_eq_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
inr : ¬x.toENatAux = 0
⊢ x.toENatAux ≠ 0
have inr₁ : ¬x = 0
Tactic: rwa [Ne, toENatAux_eq_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (hypothesis)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have x₁ : 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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have 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
Tactic: wlog hle : x ≤ y
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
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
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have wlog : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
Tactic: wlog hle : x ≤ y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
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
have inr : toENatAux.{u} (y + x) = x.toENatAux + y.toENatAux
Tactic: rw [add_comm, this y x (le_of_not_ge hle), add_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
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
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have inr₁ : y.toENatAux + x.toENatAux = x.toENatAux + y.toENatAux
Tactic: rw [add_comm, this y x (le_of_not_ge hle), add_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
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
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have inr₂ : x.toENatAux + y.toENatAux = x.toENatAux + y.toENatAux
Tactic: rw [add_comm, this y x (le_of_not_ge hle), add_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have inl : ∀ (x : ℕ) (hle : (↑x : Cardinal.{u}) ≤ y),
  toENatAux.{u} ((↑x : Cardinal.{u}) + y) = toENatAux.{u} (↑x : Cardinal.{u}) + y.toENatAux
Tactic: lift x to ℕ using hle.trans_lt hy
Cleared hypotheses: x, hle
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : (↑x : Cardinal.{u}) ≤ y
⊢ toENatAux.{u} ((↑x : Cardinal.{u}) + y) = toENatAux.{u} (↑x : Cardinal.{u}) + y.toENatAux
have 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})
Tactic: lift y to ℕ using hy
Cleared hypotheses: y, hy, hle
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have inr : toENatAux.{u} (x + y) = ⊤
Tactic: simp only [toENatAux_eq_top hy, add_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (hypothesis)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
⊢ toENatAux.{u} (x + y) = x.toENatAux + y.toENatAux
have x₁ : 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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
⊢ StrictMonoOn (β := ℕ∞) (⇑toENat : (a : Cardinal.{u_1}) → ℕ∞) (Iic ℵ₀)
have simp : ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1
Tactic: simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
a : Cardinal.{u_1}
⊢ (↑((toENat : (a : Cardinal.{u_1}) → ℕ∞) a) : Cardinal.{u_1}) = a ↔ a ≤ ℵ₀
have rw : (∃ (b : ℕ∞), a = (↑b : Cardinal.{u_1})) ↔ a ≤ ℵ₀
Tactic: rw [eq_comm, ← enat_gc.exists_eq_l]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c c' : Cardinal.{u}
hc : c ≤ ℵ₀
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔ c ≤ c'
have lift : ∀ (c : ℕ∞),
  LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔
    (↑c : Cardinal.{u}) ≤ c'
Tactic: lift c to ℕ∞ using hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c' : Cardinal.{u}
c : ℕ∞
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔
    (↑c : Cardinal.{u}) ≤ c'
have simp_rw : c ≤ (toENat : (a : Cardinal.{u}) → ℕ∞) c' ↔ (↑c : Cardinal.{u}) ≤ c'
Tactic: simp_rw [toENat_ofENat, enat_gc _]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c c' : Cardinal.{u}
hc' : c' < ℵ₀
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c' : ℕ∞) ↔ c ≤ c'
have lift : ∀ (c' : ℕ),
  LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c' : Cardinal.{u}) : ℕ∞) ↔
    c ≤ (↑c' : Cardinal.{u})
Tactic: lift c' to ℕ using hc'
Cleared hypotheses: c', hc'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c : Cardinal.{u}
c' : ℕ
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c' : Cardinal.{u}) : ℕ∞) ↔
    c ≤ (↑c' : Cardinal.{u})
have simp_rw : LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑c' : ℕ∞) : ℕ∞) ↔ c ≤ (↑c' : Cardinal.{u})
Tactic: simp_rw [toENat_nat, ← toENat_le_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c : Cardinal.{u}
n : ℕ
⊢ LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u}) ≤ c
have rw : LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑n : Cardinal.{u}) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔
  (↑n : Cardinal.{u}) ≤ c
Tactic: rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c : Cardinal.{u}
n : ℕ
rw :
  LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑n : Cardinal.{u}) : ℕ∞)
      ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔
    (↑n : Cardinal.{u}) ≤ c
⊢ LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u}) ≤ c
have rw₁ : (↑n : Cardinal.{u}) ≤ c ↔ (↑n : Cardinal.{u}) ≤ c
Tactic: rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
c : Cardinal.{u}
ha : c ≤ ℵ₀
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} c) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)
have inl : ∀ (c : ℕ∞),
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} (↑c : Cardinal.{u})) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑c : Cardinal.{u}) : ℕ∞)
Tactic: lift c to ℕ∞ using ha
Cleared hypotheses: c, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (hypothesis)
Goal:
c : Cardinal.{u}
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} c) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞)
have x : c ≤ ℵ₀ ∨ ℵ₀ ≤ c
Tactic: cases le_total c ℵ₀ with
  | inl ha => lift c to ℕ∞ using ha; simp
  | inr ha => simp [toENat_eq_top.2, ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) #α : ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
have rw : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} #α) : ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
Tactic: rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
rw :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{v, u} #α) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) #α : ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
have rw₁ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{max v u}) → ℕ∞) (lift.{max u v, v} #β) : ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
Tactic: rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
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}) → ℕ∞) #β : ℕ∞)
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) #α : ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
have rw₂ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞) ((toENat : (a : Cardinal.{v}) → ℕ∞) #β : ℕ∞)
Tactic: rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m n : ℕ∞
⊢ (↑(m + n) : Cardinal.{u_1}) = (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1})
have a : (↑(m + n) : Cardinal.{u_1}) ∈ Iic ℵ₀
Tactic: apply toENat_injOn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m n : ℕ∞
a : (↑(m + n) : Cardinal.{u_1}) ∈ Iic ℵ₀
⊢ (↑(m + n) : Cardinal.{u_1}) = (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1})
have a₁ : (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1}) ∈ Iic ℵ₀
Tactic: apply toENat_injOn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m n : ℕ∞
a : (↑(m + n) : Cardinal.{u_1}) ∈ Iic ℵ₀
a₁ : (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1}) ∈ Iic ℵ₀
⊢ (↑(m + n) : Cardinal.{u_1}) = (↑m : Cardinal.{u_1}) + (↑n : Cardinal.{u_1})
have 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})) : ℕ∞)
Tactic: apply toENat_injOn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ (↑m : Cardinal.{u_1}) + ℵ₀ = ℵ₀
have rw : ℵ₀ + (↑m : Cardinal.{u_1}) = ℵ₀
Tactic: rw [add_comm, aleph0_add_ofENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
rw : ℵ₀ + (↑m : Cardinal.{u_1}) = ℵ₀
⊢ (↑m : Cardinal.{u_1}) + ℵ₀ = ℵ₀
have rw₁ : ℵ₀ = ℵ₀
Tactic: rw [add_comm, aleph0_add_ofENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ
hm : Ne (α := ℕ∞) (↑m : ℕ∞) 0
⊢ (↑(↑m : ℕ∞) : Cardinal.{u_1}) * ℵ₀ = ℵ₀
have coe : (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
Tactic: rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ
hm : Ne (α := ℕ∞) (↑m : ℕ∞) 0
coe : (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
⊢ (↑(↑m : ℕ∞) : Cardinal.{u_1}) * ℵ₀ = ℵ₀
have coe₁ : ℵ₀ = ℵ₀
Tactic: rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
hm : m ≠ 0
⊢ (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
have top : ∀ (hm : Ne (α := ℕ∞) ⊤ 0), (↑⊤ : Cardinal.{u_1}) * ℵ₀ = ℵ₀
Tactic: induction m with
  | top => exact aleph0_mul_aleph0
  | coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
hm : m ≠ 0
top : ∀ (hm : Ne (α := ℕ∞) ⊤ 0), (↑⊤ : Cardinal.{u_1}) * ℵ₀ = ℵ₀
⊢ (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
have coe : ∀ (m : ℕ) (hm : Ne (α := ℕ∞) (↑m : ℕ∞) 0), (↑(↑m : ℕ∞) : Cardinal.{u_1}) * ℵ₀ = ℵ₀
Tactic: induction m with
  | top => exact aleph0_mul_aleph0
  | coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
hm : m ≠ 0
⊢ ℵ₀ * (↑m : Cardinal.{u_1}) = ℵ₀
have rw : (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
Tactic: rw [mul_comm, ofENat_mul_aleph0 hm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
hm : m ≠ 0
rw : (↑m : Cardinal.{u_1}) * ℵ₀ = ℵ₀
⊢ ℵ₀ * (↑m : Cardinal.{u_1}) = ℵ₀
have rw₁ : ℵ₀ = ℵ₀
Tactic: rw [mul_comm, ofENat_mul_aleph0 hm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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 ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))
have rsuffices : ∀ (y : 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 α))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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) → α))
⊢ ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))
have rsuffices₁ : Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
Tactic: rsuffices ⟨y⟩ : Nonempty (Fin n ↪ (sᶜ : Set α))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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)
⊢ ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))
have h : Disjoint s (range (ι := Fin n) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ sᶜ)) : (a : Fin n) → α))
Tactic: use y.trans (subtype _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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)
⊢ Disjoint s (range (ι := Fin n) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ sᶜ)) : (a : Fin n) → α))
have h : ∀ ⦃a : α⦄,
  Membership.mem (γ := Set α) (range (ι := Fin n) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ sᶜ)) : (a : Fin n) → α)) a →
    a ∉ s
Tactic: rw [Set.disjoint_right]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
hs : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
have inl : ∀ (hα : Finite α), Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
Tactic: rcases finite_or_infinite α with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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))
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
have inr : ∀ (hα : Infinite α), Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
Tactic: rcases finite_or_infinite α with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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 α
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
have inl : Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
Tactic: apply nonempty_of_card_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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 α
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl : 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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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)
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl₁ : s.ncard + n ≤ s.ncard + 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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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)
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl₂ : s.ncard + n ≤ s.ncard + Nat.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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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)
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl₃ : s.ncard + n ≤ s.ncard + sᶜ.ncard
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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl₄ : s.ncard + n ≤ Nat.card α
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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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 α
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl₅ : LE.le (α := ℕ∞) (↑(s.ncard + n) : ℕ∞) (↑(Nat.card α) : ℕ∞)
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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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 α) : ℕ∞)
⊢ Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑sᶜ : Type u_1)
have inl₆ : (↑(s.ncard + n) : ℕ∞) ≤ ENat.card α
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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
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 α
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin n ↪ (↑sᶜ : Type u_1))
have inl : Fintype.card (Fin n) ≤ Fintype.card.{u_1} (↑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]