chore(*): use autoparams and fun_prop (#31317)

urkud · urkud · commit efdba0409fd6 · 2025-11-06T11:49:37.000Z
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
@@ -36,9 +36,6 @@ def homeomorph {R S A : Type*} [Semifield R] [Semifield S] [Ring A]
   invFun := MapsTo.restrict (algebraMap R S) _ _ (image_subset_iff.mp h.algebraMap_image.subset)
   left_inv x := Subtype.ext <| h.rightInvOn x.2
   right_inv x := Subtype.ext <| h.left_inv x
-  continuous_toFun := continuous_induced_rng.mpr <| f.continuous.comp continuous_induced_dom
-  continuous_invFun := continuous_induced_rng.mpr <|
-    continuous_algebraMap R S |>.comp continuous_induced_dom
 
 lemma compactSpace {R S A : Type*} [Semifield R] [Semifield S] [Ring A]
     [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [TopologicalSpace R]
@@ -181,9 +178,6 @@ def homeomorph {R S A : Type*} [Semifield R] [Field S] [NonUnitalRing A]
   invFun := MapsTo.restrict (algebraMap R S) _ _ (image_subset_iff.mp h.algebraMap_image.subset)
   left_inv x := Subtype.ext <| h.rightInvOn x.2
   right_inv x := Subtype.ext <| h.left_inv x
-  continuous_toFun := continuous_induced_rng.mpr <| f.continuous.comp continuous_induced_dom
-  continuous_invFun := continuous_induced_rng.mpr <|
-    continuous_algebraMap R S |>.comp continuous_induced_dom
 
 universe u v w
 
diff --git a/Mathlib/Analysis/Complex/Circle.lean b/Mathlib/Analysis/Complex/Circle.lean
@@ -197,7 +197,7 @@ theorem fourierChar_apply' (x : ℝ) : 𝐞 x = Circle.exp (2 * π * x) := rfl
 
 theorem fourierChar_apply (x : ℝ) : 𝐞 x = Complex.exp (↑(2 * π * x) * Complex.I) := rfl
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_fourierChar : Continuous 𝐞 := Circle.exp.continuous.comp (continuous_mul_left _)
 
 theorem fourierChar_ne_one : fourierChar ≠ 1 := by
@@ -218,8 +218,8 @@ theorem probChar_apply' (x : ℝ) : probChar x = Circle.exp x := rfl
 
 theorem probChar_apply (x : ℝ) : probChar x = Complex.exp (x * Complex.I) := rfl
 
-@[continuity]
-theorem continuous_probChar : Continuous probChar := Circle.exp.continuous
+@[continuity, fun_prop]
+theorem continuous_probChar : Continuous probChar := map_continuous Circle.exp
 
 theorem probChar_ne_one : probChar ≠ 1 := by
   rw [DFunLike.ne_iff]
diff --git a/Mathlib/Analysis/Fourier/AddCircleMulti.lean b/Mathlib/Analysis/Fourier/AddCircleMulti.lean
@@ -49,8 +49,7 @@ variable (n : d → ℤ)
 /-- Exponential monomials in `d` variables. -/
 def mFourier : C(UnitAddTorus d, ℂ) where
   toFun x := ∏ i : d, fourier (n i) (x i)
-  continuous_toFun := continuous_finset_prod _
-    fun i _ ↦ (fourier (n i)).continuous.comp (continuous_apply i)
+  continuous_toFun := by fun_prop
 
 variable {n} {x : UnitAddTorus d}
 
diff --git a/Mathlib/Condensed/Light/TopCatAdjunction.lean b/Mathlib/Condensed/Light/TopCatAdjunction.lean
@@ -163,7 +163,6 @@ can only prove this for `X : TopCat.{0}`.
 noncomputable def sequentialAdjunctionHomeo (X : TopCat.{0}) [SequentialSpace X] :
     X.toLightCondSet.toTopCat ≃ₜ X where
   toEquiv := topCatAdjunctionCounitEquiv X
-  continuous_toFun := (topCatAdjunctionCounit X).hom.continuous
   continuous_invFun := by
     apply SeqContinuous.continuous
     unfold SeqContinuous
diff --git a/Mathlib/Condensed/TopCatAdjunction.lean b/Mathlib/Condensed/TopCatAdjunction.lean
@@ -178,7 +178,6 @@ noncomputable def compactlyGeneratedAdjunctionCounitHomeo
     (X : TopCat.{u + 1}) [UCompactlyGeneratedSpace.{u} X] :
     X.toCondensedSet.toTopCat ≃ₜ X where
   toEquiv := topCatAdjunctionCounitEquiv X
-  continuous_toFun := (topCatAdjunctionCounit X).hom.continuous
   continuous_invFun := by
     apply continuous_from_uCompactlyGeneratedSpace
     exact fun _ _ ↦ continuous_coinducingCoprod X.toCondensedSet _
diff --git a/Mathlib/Topology/Category/CompHausLike/Limits.lean b/Mathlib/Topology/Category/CompHausLike/Limits.lean
@@ -199,8 +199,7 @@ pairs `(x,y)` such that `f x = g y`, with the topology induced by the product.
 def pullback : CompHausLike P :=
   letI set := { xy : X × Y | f xy.fst = g xy.snd }
   haveI : CompactSpace set :=
-    isCompact_iff_compactSpace.mp (isClosed_eq (f.hom.continuous.comp continuous_fst)
-      (g.hom.continuous.comp continuous_snd)).isCompact
+    isCompact_iff_compactSpace.mp (isClosed_eq (by fun_prop) (by fun_prop)).isCompact
   CompHausLike.of P set
 
 /--
diff --git a/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean b/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
@@ -207,8 +207,7 @@ instance (priority := 100) [SequentialSpace X] : UCompactlyGeneratedSpace.{u} X
   apply IsClosed.mem_of_tendsto _ ((continuous_uliftUp.tendsto ∞).comp this)
   · simp only [Function.comp_apply, mem_preimage, eventually_atTop, ge_iff_le]
     exact ⟨0, fun b _ ↦ hu b⟩
-  · exact h (CompHaus.of (ULift.{u} (OnePoint ℕ)))
-      ⟨g, (continuousMapMkNat u p hup).continuous.comp continuous_uliftDown⟩
+  · exact h (CompHaus.of (ULift.{u} (OnePoint ℕ))) ⟨g, by fun_prop⟩
 
 end UCompactlyGeneratedSpace
 
diff --git a/Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean b/Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
@@ -130,7 +130,6 @@ infinity. -/
 def ContinuousMap.liftZeroAtInfty [CompactSpace α] : C(α, β) ≃ C₀(α, β) where
   toFun f :=
     { toFun := f
-      continuous_toFun := f.continuous
       zero_at_infty' := by simp }
   invFun f := f
 
diff --git a/Mathlib/Topology/PartitionOfUnity.lean b/Mathlib/Topology/PartitionOfUnity.lean
@@ -544,8 +544,7 @@ theorem exists_finset_toPOUFun_eventuallyEq (i : ι) (x : X) : ∃ t : Finset ι
   exact hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩
 
 theorem continuous_toPOUFun (i : ι) : Continuous (f.toPOUFun i) := by
-  refine (f i).continuous.mul <|
-    continuous_finprod_cond (fun j _ => continuous_const.sub (f j).continuous) ?_
+  refine (map_continuous <| f i).mul <| continuous_finprod_cond (fun j _ => by fun_prop) ?_
   simp only [mulSupport_one_sub]
   exact f.locallyFinite
 
diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean
@@ -459,7 +459,7 @@ theorem exists_extension_forall_mem_of_isClosedEmbedding (f : C(X, ℝ)) {t : Se
   have h : ℝ ≃o Ioo (-1 : ℝ) 1 := orderIsoIooNegOneOne ℝ
   let F : X →ᵇ ℝ :=
     { toFun := (↑) ∘ h ∘ f
-      continuous_toFun := continuous_subtype_val.comp (h.continuous.comp f.continuous)
+      continuous_toFun := by fun_prop
       map_bounded' := isBounded_range_iff.1
         ((isBounded_Ioo (-1 : ℝ) 1).subset <| range_subset_iff.2 fun x => (h (f x)).2) }
   let t' : Set ℝ := (↑) ∘ h '' t
diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean
@@ -455,7 +455,7 @@ theorem exists_continuous_one_zero_of_isCompact_of_isGδ [RegularSpace X] [Local
   have S x : Summable (fun n ↦ u n * f n x) := Summable.of_nonneg_of_le
       (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1) (fun n ↦ I n x) u_sum
   refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
-  · apply continuous_tsum (fun n ↦ continuous_const.mul (f n).continuous) u_sum (fun n x ↦ ?_)
+  · apply continuous_tsum (fun n ↦ by fun_prop) u_sum (fun n x ↦ ?_)
     simpa [abs_of_nonneg, (u_pos n).le, (f_range n x).1] using I n x
   · apply Subset.antisymm (fun x hx ↦ by simp [g, fs _ hx, hu]) ?_
     apply compl_subset_compl.1
