feat(set_theory/zfc): more quotient lemmas (#15324)

It seems like we decided to use a custom `mk` definition for `Set` instead of `quotient.mk`. As such, we transfer the basic results on quotients to `Set`, in order to aid rewriting.
leanprover-community · Jul 15, 2022 · 7929a63 · 7929a63
1 parent 15da625
commit 7929a63
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/set_theory/zfc.lean b/src/set_theory/zfc.lean
@@ -371,7 +371,11 @@ open pSet
 /-- Turns a pre-set into a ZFC set. -/
 def mk : pSet → Set := quotient.mk
 
-@[simp] theorem mk_eq (x : pSet) : @eq Set ⟦x⟧ (mk x) := rfl
+@[simp] theorem mk_eq (x : pSet) : ⟦x⟧ = mk x := rfl
+@[simp] theorem mk_out : ∀ x : Set, mk x.out = x := quotient.out_eq
+theorem eq {x y : pSet} : mk x = mk y ↔ equiv x y := quotient.eq
+theorem sound {x y : pSet} (h : pSet.equiv x y) : mk x = mk y := quotient.sound h
+theorem exact {x y : pSet} : mk x = mk y → pSet.equiv x y := quotient.exact
 
 @[simp] lemma eval_mk {n f x} :
   (@resp.eval (n+1) f : Set → arity Set n) (mk x) = resp.eval n (resp.f f x) :=