Name clashes

data/cardinal.lean

@@ -20,6 +20,8 @@ local attribute [instance] prop_decidable
 
 universes u v w x
 
+namespace cardinal
+
 structure embedding (α : Sort*) (β : Sort*) :=
 (to_fun : α → β)
 (inj    : injective to_fun)
@@ -224,7 +226,9 @@ let f' : (α → γ) → (β → γ) := λf b, if h : ∃c, e c = b then f (some
 
 end embedding
 
-protected def equiv.to_embedding {α : Type u} {β : Type v} (f : α ≃ β) : embedding α β :=
+end cardinal
+
+protected def equiv.to_embedding {α : Type u} {β : Type v} (f : α ≃ β) : cardinal.embedding α β :=
 ⟨f, f.bijective.1⟩
 
 @[simp] theorem equiv.to_embedding_coe_fn {α : Type u} {β : Type v} (f : α ≃ β) :

data/ordinal.lean

@@ -10,7 +10,7 @@ Ordinals are defined as equivalences of well-ordered sets by order isomorphism.
 import data.cardinal
 noncomputable theory
 
-open function
+open function cardinal
 local attribute [instance] classical.prop_decidable
 
 universes u v w

tests/finish3.lean

@@ -59,7 +59,7 @@ example : (∃ x : A, r) → r := by finish
 example (a : A) : r → (∃ x : A, r) := begin safe; apply a_2; assumption end
 example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := by finish
 
-theorem foo: (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
+theorem foo': (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
 by finish [iff_def]
 
 example (h : ∀ x, ¬ ¬ p x) : p a := by finish