chore(Topology): continuity -> fun_prop (#23136)

Author: grunweg

Mathlib/Dynamics/Flow.lean

@@ -153,14 +153,9 @@ def reverse : Flow τ α where
   map_add' _ _ _ := by dsimp; rw [neg_add, map_add]
   map_zero' _ := by dsimp; rw [neg_zero, map_zero_apply]
 
--- Porting note: add @continuity to Flow.toFun so that these works:
--- Porting note: Homeomorphism.continuous_toFun  : Continuous toFun  := by continuity
--- Porting note: Homeomorphism.continuous_invFun : Continuous invFun := by continuity
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_toFun (t : τ) : Continuous (ϕ.toFun t) := by
-  rw [← curry_uncurry ϕ.toFun]
-  apply continuous_curry
-  exact ϕ.cont'
+  fun_prop
 
 /-- The map `ϕ t` as a homeomorphism. -/
 def toHomeomorph (t : τ) : (α ≃ₜ α) where

Mathlib/Topology/Algebra/Monoid.lean

@@ -298,11 +298,8 @@ theorem isClosed_setOf_map_one [One M₁] [One M₂] : IsClosed { f : M₁ → M
 theorem isClosed_setOf_map_mul [Mul M₁] [Mul M₂] [ContinuousMul M₂] :
     IsClosed { f : M₁ → M₂ | ∀ x y, f (x * y) = f x * f y } := by
   simp only [setOf_forall]
-  exact
-    isClosed_iInter fun x =>
-      isClosed_iInter fun y =>
-        isClosed_eq (continuous_apply _)
-          (by continuity)
+  exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦
+    isClosed_eq (continuous_apply _) (by fun_prop)
 
 section Semigroup
 

Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

@@ -188,7 +188,7 @@ theorem sublattice_closure_eq_top (L : Set C(X, ℝ)) (nA : L.Nonempty)
   have U_nhd_y : ∀ x y, U x y ∈ 𝓝 y := by
     intro x y
     refine IsOpen.mem_nhds ?_ ?_
-    · apply isOpen_lt <;> continuity
+    · apply isOpen_lt <;> fun_prop
     · rw [Set.mem_setOf_eq, w₂]
       exact sub_lt_self _ pos
   -- Fixing `x` for a moment, we have a family of functions `fun y ↦ g x y`
@@ -377,7 +377,7 @@ theorem Subalgebra.SeparatesPoints.rclike_to_real {A : StarSubalgebra 𝕜 C(X,
     simp only [coe_smul, coe_one, smul_apply, one_apply, Algebra.id.smul_eq_mul, mul_one,
       const_apply]
   -- Consider now the function `fun x ↦ |f x - f x₂| ^ 2`
-  refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by continuity⟩, ?_, rfl⟩, ?_⟩
+  refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩
   · -- This is also an element of the subalgebra, and takes only real values
     rw [SetLike.mem_coe, Subalgebra.mem_comap]
     convert (A.restrictScalars ℝ).mul_mem hFA (star_mem hFA : star F ∈ A)

Mathlib/Topology/ExtremallyDisconnected.lean

@@ -300,6 +300,6 @@ instance instExtremallyDisconnected {ι : Type*} {π : ι → Type*} [∀ i, Top
     · rwa [← ij, sigma_mk_preimage_image_eq_self]
     · rw [sigma_mk_preimage_image' ij]
       exact isOpen_empty
-  · continuity
+  · fun_prop
 
 end

Mathlib/Topology/Homotopy/Basic.lean

@@ -212,7 +212,7 @@ def trans {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homotopy f₁
   toFun x := if (x.1 : ℝ) ≤ 1 / 2 then F.extend (2 * x.1) x.2 else G.extend (2 * x.1 - 1) x.2
   continuous_toFun := by
     refine
-      continuous_if_le (continuous_induced_dom.comp continuous_fst) continuous_const
+      continuous_if_le (by fun_prop) continuous_const
         (F.continuous.comp (by continuity)).continuousOn
         (G.continuous.comp (by continuity)).continuousOn ?_
     rintro x hx

Mathlib/Topology/Homotopy/HomotopyGroup.lean

@@ -268,7 +268,7 @@ theorem homotopicTo (i : N) {p q : Ω^ N X x} :
   · rintro y ⟨i, iH⟩
     rw [homotopyTo_apply, H.eq_fst, p.2]
     all_goals apply Cube.insertAt_boundary; right; exact ⟨i, iH⟩
-  · continuity
+  · fun_prop
   iterate 2 intro; ext; erw [homotopyTo_apply, toLoop_apply]; swap
   · apply H.apply_zero
   · apply H.apply_one
@@ -282,7 +282,7 @@ theorem homotopicTo (i : N) {p q : Ω^ N X x} :
 @[simps!] def homotopyFrom (i : N) {p q : Ω^ N X x} (H : (toLoop i p).Homotopy (toLoop i q)) :
     C(I × I^N, X) :=
   (ContinuousMap.comp ⟨_, ContinuousMap.continuous_uncurry⟩
-          (ContinuousMap.comp ⟨Subtype.val, by continuity⟩ H.toContinuousMap).curry).uncurry.comp <|
+          (ContinuousMap.comp ⟨Subtype.val, by fun_prop⟩ H.toContinuousMap).curry).uncurry.comp <|
     (ContinuousMap.id I).prodMap (Cube.splitAt i)
 
 theorem homotopicFrom (i : N) {p q : Ω^ N X x} :

Mathlib/Topology/MetricSpace/Perfect.lean

@@ -122,7 +122,7 @@ theorem Perfect.exists_nat_bool_injection
   · rintro y ⟨x, rfl⟩
     exact map_mem ⟨_, hdom⟩ 0
   · apply hdiam.map_continuous.comp
-    continuity
+    fun_prop
   intro x y hxy
   simpa only [← Subtype.val_inj] using hdisj'.map_injective hxy