chore(set_theory/zfc/basic): reverse sInter_coe (#18773)

vihdzp · vihdzp · commit f0b3759a8ef0 · 2023-04-25T23:03:09.000Z
It now matches `coe_sUnion`, and works as a `norm_cast` lemma. Mathlib 4: leanprover-community/mathlib4#3345
diff --git a/src/set_theory/zfc/basic.lean b/src/set_theory/zfc/basic.lean
@@ -1114,8 +1114,9 @@ begin
   exact H _ hxz
 end
 
-@[simp, norm_cast] theorem sInter_coe {x : Set.{u}} (h : x.nonempty) : ⋂₀ (x : Class.{u}) = ⋂₀ x :=
-set.ext $ λ y, sInter_apply.trans (Set.mem_sInter h).symm
+@[simp, norm_cast] theorem coe_sInter {x : Set.{u}} (h : x.nonempty) :
+  ↑(⋂₀ x) = ⋂₀ (x : Class.{u}) :=
+set.ext $ λ y, (Set.mem_sInter h).trans sInter_apply.symm
 
 theorem mem_of_mem_sInter {x y z : Class} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) : y ∈ z :=
 by { obtain ⟨w, rfl, hw⟩ := hy, exact coe_mem.2 (hw z hz) }
