awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inl : ∀ (hy : y = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
Tactic: rcases hy with hy | hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
inl :
  ∀ (hy : y = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inl₁ : ∀ (hy : y ∈ s), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
Tactic: rcases hy with hy | hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inr : ∀ (hy : y = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
Tactic: rcases hy with hy | hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
inr :
  ∀ (hy : y = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inr₁ : ∀ (hy : y ∈ s), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
Tactic: rcases hy with hy | hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inl : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) f) ((fun (x : (i : ι) → β i) ↦ x i) y) → f = y
Tactic: subst x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inr : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) f) → x = f
Tactic: subst y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
⊢ Membership.mem (γ := Subfield ↥(closure s)) (rangeOfWType s) a
have rw : (↑a : α) ∈
  Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Subfield α) (closure s) x) ''
    (↑(rangeOfWType s) : Set ↥(closure s))
Tactic: rw [← SetLike.mem_coe, ← Subtype.val_injective.mem_set_image]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
⊢ (↑a : α) ∈
    Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Subfield α) (closure s) x) ''
      (↑(rangeOfWType s) : Set ↥(closure s))
have change : Membership.mem (γ := Subfield α) (map (subtype (closure s)) (rangeOfWType s)) (↑a : α)
Tactic: change ↑a ∈ map (closure s).subtype _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
a : ↥(closure s)
h : Membership.mem (γ := Subfield ↥(closure s)) ⊤ a
⊢ Membership.mem (γ := Subfield α) (map (subtype (closure s)) (rangeOfWType s)) (↑a : α)
have refine : ∀ (a : α) (ha : a ∈ s), a ∈ (↑(map (subtype (closure s)) (rangeOfWType s)) : Set α)
Tactic: refine closure_le.mpr (fun a ha ↦ ?_) a.prop
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ Function.Surjective (β := ↥(closure s)) (WType.elim (β := Operands s) (↥(closure s)) (operate s))
have rw : Eq (α := Set ↥(closure s)) (Set.range (WType.elim (β := Operands s) (↥(closure s)) (operate s))) Set.univ
Tactic: rw [← Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ #(WType (Operands s)) ≤ max #(↑s : Type u) ℵ₀
have h : max #(↑s : Type u) ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ (↑s : Type u))) ℵ₀
Tactic: convert! WType.cardinalMk_le_max_aleph0_of_finite' using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
h : max #(↑s : Type u) ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ (↑s : Type u))) ℵ₀
⊢ #(WType (Operands s)) ≤ max #(↑s : Type u) ℵ₀
have convert_3 : ∀ (a : Fin 6 ⊕ (↑s : Type u)), Finite (Operands s a)
Tactic: convert! WType.cardinalMk_le_max_aleph0_of_finite' using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ (↑s : Type u))) ℵ₀
have h : max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
Tactic: rw [lift_uzero, mk_sum, lift_uzero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (hypothesis)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have this : lift.{u, 0} #(Fin 6) < ℵ₀
Tactic: have : lift.{u, 0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have h : ∀ (h : #(↑s : Type u) < ℵ₀), max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
Tactic: obtain h | h := lt_or_ge #s ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ∀ (h : #(↑s : Type u) < ℵ₀), max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have h₁ : ∀ (h : ℵ₀ ≤ #(↑s : Type u)), max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
Tactic: obtain h | h := lt_or_ge #s ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #(↑s : Type u) < ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have h₁ : lift.{u, 0} #(Fin 6) + #(↑s : Type u) ≤ ℵ₀
Tactic: rw [max_eq_right h.le, max_eq_right]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #(↑s : Type u)
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have h₁ : #(↑s : Type u) = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
Tactic: rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #(↑s : Type u)
h₁ : #(↑s : Type u) = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have h₂ : #(↑s : Type u) = max #(↑s : Type u) ℵ₀
Tactic: rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #(↑s : Type u)
h₁ : #(↑s : Type u) = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
h₂ : #(↑s : Type u) = max #(↑s : Type u) ℵ₀
⊢ max #(↑s : Type u) ℵ₀ = max (lift.{u, 0} #(Fin 6) + #(↑s : Type u)) ℵ₀
have h₃ : #(↑s : Type u) = #(↑s : Type u)
Tactic: rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
⊢ Finite (Operands s (Sum.inl n))
have convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, sorry⟩)))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)))
⊢ Finite (Operands s (Sum.inl n))
have convert_3₁ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨1, sorry⟩)))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)))
convert_3₁ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)))
⊢ Finite (Operands s (Sum.inl n))
have convert_3₂ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨2, sorry⟩)))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)))
convert_3₁ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)))
convert_3₂ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)))
⊢ Finite (Operands s (Sum.inl n))
have convert_3₃ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨3, sorry⟩)))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)))
convert_3₁ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)))
convert_3₂ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)))
convert_3₃ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)))
⊢ Finite (Operands s (Sum.inl n))
have convert_3₄ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨4, sorry⟩)))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Subfield (goal)
Goal:
α : Type u
s : Set α
inst : DivisionRing α
n : Fin 6
convert_3 : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)))
convert_3₁ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)))
convert_3₂ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)))
convert_3₃ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)))
convert_3₄ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)))
⊢ Finite (Operands s (Sum.inl n))
have convert_3₅ : Finite (Operands s (Sum.inl ((fun (i : Fin 6) ↦ i) ⟨5, sorry⟩)))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (0 : ℕ) ↔ c = 0 ∨ ℵ₀ ≤ c
have rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
Tactic: rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (0 : ℕ) ↔ c = 0 ∨ ℵ₀ ≤ c
have rw₁ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (0 : ℕ∞) ∨
    Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔
  c = 0 ∨ ℵ₀ ≤ c
Tactic: rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
rw₁ :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (0 : ℕ∞) ∨
      Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔
    c = 0 ∨ ℵ₀ ≤ c
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (0 : ℕ) ↔ c = 0 ∨ ℵ₀ ≤ c
have rw₂ : c = 0 ∨ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔ c = 0 ∨ ℵ₀ ≤ c
Tactic: rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
rw₁ :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (0 : ℕ∞) ∨
      Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔
    c = 0 ∨ ℵ₀ ≤ c
rw₂ : c = 0 ∨ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔ c = 0 ∨ ℵ₀ ≤ c
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (0 : ℕ) ↔ c = 0 ∨ ℵ₀ ≤ c
have rw₃ : c = 0 ∨ ℵ₀ ≤ c ↔ c = 0 ∨ ℵ₀ ≤ c
Tactic: rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) = c
have lift : ∀ (c : ℕ),
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) (↑c : Cardinal.{u_1})) : Cardinal.{u_1})
    (↑c : Cardinal.{u_1})
Tactic: lift c to ℕ using h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : ℕ
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) (↑c : Cardinal.{u_1})) : Cardinal.{u_1})
    (↑c : Cardinal.{u_1})
have rw : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑c : Cardinal.{u_1})
Tactic: rw [toNat_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
h : c < ℵ₀
⊢ Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) c) : Cardinal.{u})
    (↑(Classical.choose (p := fun (x : ℕ) ↦ c = (↑x : Cardinal.{u})) ⋯) : Cardinal.{u})
have rw : c = (↑(Classical.choose (p := fun (x : ℕ) ↦ c = (↑x : Cardinal.{u})) sorry) : Cardinal.{u})
Tactic: rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
h : c < ℵ₀
rw : c = (↑(Classical.choose (p := fun (x : ℕ) ↦ c = (↑x : Cardinal.{u})) ⋯) : Cardinal.{u})
⊢ Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) c) : Cardinal.{u})
    (↑(Classical.choose (p := fun (x : ℕ) ↦ c = (↑x : Cardinal.{u})) ⋯) : Cardinal.{u})
have rw₁ : c = c
Tactic: rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_2}) 0
have rw : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑0 : Cardinal.{u_2}) 0
Tactic: rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑0 : Cardinal.{u_2}) 0
⊢ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_2}) 0
have rw₁ : Eq.{u_2 + 2} (α := Cardinal.{u_2}) 0 0
Tactic: rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u_1}
h : (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) = c
⊢ c < ℵ₀
have rw : (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) < ℵ₀
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
⊢ StrictMonoOn (β := ℕ) (⇑toNat : (a : Cardinal.{u_1}) → ℕ) (Iio ℵ₀)
have simp : ∀ (i i_1 : ℕ), i < i_1 → i < i_1
Tactic: simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ (toNat : (a : Cardinal.{u}) → ℕ) c = n ↔ c = (↑n : Cardinal.{u})
have rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = n ↔ c = (↑n : Cardinal.{u})
Tactic: rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = n ↔ c = (↑n : Cardinal.{u})
⊢ (toNat : (a : Cardinal.{u}) → ℕ) c = n ↔ c = (↑n : Cardinal.{u})
have rw₁ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c = (↑n : Cardinal.{u})
Tactic: rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = n ↔ c = (↑n : Cardinal.{u})
rw₁ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c = (↑n : Cardinal.{u})
⊢ (toNat : (a : Cardinal.{u}) → ℕ) c = n ↔ c = (↑n : Cardinal.{u})
have rw₂ : c = (↑n : Cardinal.{u}) ↔ c = (↑n : Cardinal.{u})
Tactic: rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (1 : ℕ) ↔ c = 1
have rw : c = (↑1 : Cardinal.{u}) ↔ c = 1
Tactic: rw [toNat_eq_iff one_ne_zero, Nat.cast_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c : Cardinal.{u}
rw : c = (↑1 : Cardinal.{u}) ↔ c = 1
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (1 : ℕ) ↔ c = 1
have rw₁ : c = 1 ↔ c = 1
Tactic: rw [toNat_eq_iff one_ne_zero, Nat.cast_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) #α : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
have rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{v, u} #α) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
Tactic: rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{v, u} #α) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) #α : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
have rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{max u v, v} #β) : ℕ)
  ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
Tactic: rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{v, u} #α) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{max u v, v} #β) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) #α : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
have rw₂ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
Tactic: rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ (toNat : (a : Cardinal.{u}) → ℕ) (c + d) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)
have lift : ∀ (c : ℕ),
  (toNat : (a : Cardinal.{u}) → ℕ) ((↑c : Cardinal.{u}) + d) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
      ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)
Tactic: lift c to ℕ using hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
⊢ (toNat : (a : Cardinal.{u}) → ℕ) ((↑c : Cardinal.{u}) + d) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
      ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)
have lift : ∀ (d : ℕ),
  (toNat : (a : Cardinal.{u}) → ℕ) (HAdd.hAdd (α := Cardinal.{u}) (↑c : Cardinal.{u}) (↑d : Cardinal.{u})) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
      ((toNat : (a : Cardinal.{u}) → ℕ) (↑d : Cardinal.{u}) : ℕ)
Tactic: lift d to ℕ using hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
c d : ℕ
⊢ (toNat : (a : Cardinal.{u}) → ℕ) (HAdd.hAdd (α := Cardinal.{u}) (↑c : Cardinal.{u}) (↑d : Cardinal.{u})) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
      ((toNat : (a : Cardinal.{u}) → ℕ) (↑d : Cardinal.{u}) : ℕ)
have norm_cast : c + d = c + d
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
a : Cardinal.{u_1}
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
have inl : ∀ (h : a < ℵ₀), (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
Tactic: obtain h | h := lt_or_ge a ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
a : Cardinal.{u_1}
inl : ∀ (h : a < ℵ₀), (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
have inr : ∀ (h : ℵ₀ ≤ a), (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
Tactic: obtain h | h := lt_or_ge a ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a ≤ n ↔ a ≤ (↑n : Cardinal.{u})
have nth_rw : LE.le (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) a : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑n : Cardinal.{u}) : ℕ) ↔
  a ≤ (↑n : Cardinal.{u})
Tactic: nth_rw 1 [← Cardinal.toNat_natCast.{u} n,
    Cardinal.toNat_le_iff_le_of_lt_aleph0 lt (Cardinal.natCast_lt_aleph0)]