Rm simp

Author: gaearon

analysis/Analysis/Section_3_4.lean

@@ -398,7 +398,6 @@ lemma SetTheory.Set.mem_powerset' {S S' : Set} : (S': Object) ∈ S.powerset ↔
   simp
 
 /-- Another helper lemma for Exercise 3.4.7. -/
-@[simp]
 lemma SetTheory.Set.mem_union_powerset_replace_iff {S : Set} {P : S.powerset → Object → Prop} {hP : _} {x : Object} :
     x ∈ union (S.powerset.replace (P := P) hP) ↔
     ∃ (S' : S.powerset) (U : Set), P S' U ∧ x ∈ U := by