feat: port Topology.ContinuousFunction.Ideals (#4852)

Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Mathlib.lean

@@ -2800,6 +2800,7 @@ import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Topology.ContinuousFunction.Bounded
 import Mathlib.Topology.ContinuousFunction.CocompactMap
 import Mathlib.Topology.ContinuousFunction.Compact
+import Mathlib.Topology.ContinuousFunction.Ideals
 import Mathlib.Topology.ContinuousFunction.LocallyConstant
 import Mathlib.Topology.ContinuousFunction.Ordered
 import Mathlib.Topology.ContinuousFunction.Polynomial

Mathlib/Topology/Algebra/Ring/Ideal.lean

@@ -38,10 +38,13 @@ theorem Ideal.coe_closure (I : Ideal R) : (I.closure : Set R) = closure I :=
   rfl
 #align ideal.coe_closure Ideal.coe_closure
 
-@[simp]
-theorem Ideal.closure_eq_of_isClosed (I : Ideal R) [hI : IsClosed (I : Set R)] : I.closure = I :=
+-- porting note: removed `@[simp]` because we make the instance argument explicit since otherwise
+-- it causes timeouts as `simp` tries and fails to generated an `IsClosed` instance.
+-- we also `alignₓ` because of the change in argument type
+-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.20heartbeats.20of.20the.20linter
+theorem Ideal.closure_eq_of_isClosed (I : Ideal R) (hI : IsClosed (I : Set R)) : I.closure = I :=
   SetLike.ext' hI.closure_eq
-#align ideal.closure_eq_of_is_closed Ideal.closure_eq_of_isClosed
+#align ideal.closure_eq_of_is_closed Ideal.closure_eq_of_isClosedₓ
 
 end Ring