fix

Author: staroperator

Mathlib/SetTheory/ZFC/Cardinal.lean

@@ -6,7 +6,7 @@ Authors: Dexin Zhang
 module
 
 public import Mathlib.SetTheory.Cardinal.Basic
-public import Mathlib.SetTheory.ZFC.Ordinal
+public import Mathlib.SetTheory.ZFC.Basic
 
 /-!
 # Cardinalities of ZFC sets
@@ -89,19 +89,4 @@ theorem lift_card_iUnion_le_sum_card {α} [Small.{v, u} α] {f : α → ZFSet.{v
   simpa [cardinalMk_coe_sort, ← coe_iUnion, -mem_iUnion] using
     mk_iUnion_le_sum_mk_lift (f := SetLike.coe ∘ f)
 
-open Ordinal
-
-@[simp]
-theorem _root_.Ordinal.card_toZFSet (o : Ordinal) : o.toZFSet.card = o.card := by
-  simpa [← coe_toZFSet, cardinalMk_coe_sort, mk_Iio_ordinal, ← lift_card] using
-    mk_image_eq (s := Set.Iio o) toZFSet_injective
-
-@[simp]
-theorem card_natCast {n : ℕ} : card n = n := by
-  rw [← toZFSet_natCast, card_toZFSet, card_nat]
-
-@[simp]
-theorem card_omega : card omega = ℵ₀ := by
-  rw [← toZFSet_omega0, card_toZFSet, card_omega0]
-
 end ZFSet

Mathlib/SetTheory/ZFC/Ordinal.lean

@@ -373,7 +373,7 @@ theorem card_toZFSet (o : Ordinal) : (toZFSet o).card = o.card := by
 end Ordinal
 
 namespace ZFSet
-open Ordinal
+open Ordinal Cardinal
 
 theorem isOrdinal_toZFSet (o : Ordinal) : IsOrdinal o.toZFSet := by
   refine ⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩
@@ -408,6 +408,10 @@ noncomputable def _root_.Ordinal.toZFSetIso : Ordinal ≃o {x // ZFSet.IsOrdinal
 theorem rank_natCast {n : ℕ} : rank n = n := by
   rw [← toZFSet_natCast, rank_toZFSet]
 
+@[simp]
+theorem card_natCast {n : ℕ} : card n = n := by
+  rw [← toZFSet_natCast, card_toZFSet, card_nat]
+
 theorem isOrdinal_natCast {n : ℕ} : IsOrdinal n := by
   rw [← toZFSet_natCast]
   exact isOrdinal_toZFSet n
@@ -416,6 +420,10 @@ theorem isOrdinal_natCast {n : ℕ} : IsOrdinal n := by
 theorem rank_omega : rank omega = ω := by
   rw [← toZFSet_omega0, rank_toZFSet]
 
+@[simp]
+theorem card_omega : card omega = ℵ₀ := by
+  rw [← toZFSet_omega0, card_toZFSet, card_omega0]
+
 theorem isOrdinal_omega : IsOrdinal omega := by
   rw [← toZFSet_omega0]
   exact isOrdinal_toZFSet ω