chore: golf using fun_prop (leanprover-community#34441)

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

Author: grunweg

Mathlib/Analysis/Analytic/Basic.lean

@@ -959,8 +959,7 @@ theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'
     (hf : HasFPowerSeriesWithinOnBall f p s x r) :
     TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop
       (insert x s ∩ EMetric.ball (x : E) r) := by
-  have A : ContinuousOn (fun y : E => y - x) (insert x s ∩ EMetric.ball (x : E) r) :=
-    (continuous_id.sub continuous_const).continuousOn
+  have A : ContinuousOn (fun y : E => y - x) (insert x s ∩ EMetric.ball (x : E) r) := by fun_prop
   convert hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A using 1
   · ext z
     simp

Mathlib/Analysis/Analytic/Inverse.lean

@@ -621,7 +621,7 @@ lemma HasFPowerSeriesAt.eventually_hasSum_of_comp {f : E → F} {g : F → G}
   have : ∀ᶠ y in 𝓝 (0 : E), f (x + y) - f x ∈ EMetric.ball 0 q.radius := by
     have A : ContinuousAt (fun y ↦ f (x + y) - f x) 0 := by
       apply ContinuousAt.sub _ continuousAt_const
-      exact hf.continuousAt.comp_of_eq (continuous_add_left x).continuousAt (by simp)
+      exact hf.continuousAt.comp_of_eq (by fun_prop) (by simp)
     have B : EMetric.ball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by
       simpa using EMetric.ball_mem_nhds _ hq
     exact A.preimage_mem_nhds B

Mathlib/Analysis/CStarAlgebra/Multiplier.lean

@@ -525,11 +525,7 @@ instance [CompleteSpace A] : CompleteSpace 𝓜(𝕜, A) := by
   rw [completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.isUniformInducing]
   apply IsClosed.isComplete
   simp only [range_toProdMulOpposite, Set.setOf_forall]
-  refine isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq ?_ ?_
-  · exact
-      ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp <| continuous_unop.comp continuous_snd).mul
-        continuous_const
-  exact continuous_const.mul ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp continuous_fst)
+  exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq (by fun_prop) (by fun_prop)
 
 variable [StarRing A] [CStarRing A]
 

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -382,7 +382,7 @@ theorem y_le_one {D : ℝ} (x : E) (Dpos : 0 < D) : y D x ≤ 1 := by
         fun _ => zero_le_one
     refine ((w_compact_support E Dpos).convolutionExists_left _ ?_
       (locallyIntegrable_const (1 : ℝ)) x).integrable
-    exact continuous_const.mul ((u_continuous E).comp (continuous_id.const_smul _))
+    exact continuous_const.mul ((u_continuous E).comp (by fun_prop))
   have B : (w D ⋆[lsmul ℝ ℝ, μ] fun _ => (1 : ℝ)) x = 1 := by
     simp only [convolution, mul_one, lsmul_apply, smul_eq_mul, w_integral E Dpos]
   exact A.trans (le_of_eq B)
@@ -395,7 +395,7 @@ theorem y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1)
     have B : LocallyIntegrable (φ : E → ℝ) μ :=
       (locallyIntegrable_const _).indicator measurableSet_closedBall
     have C : Continuous (w D : E → ℝ) :=
-      continuous_const.mul ((u_continuous E).comp (continuous_id.const_smul _))
+      continuous_const.mul ((u_continuous E).comp (by fun_prop))
     exact (F_comp.convolutionExists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) C B x).integrable
   · set z := (D / (1 + D)) • x with hz
     have B : 0 < 1 + D := by linarith

Mathlib/Analysis/Calculus/BumpFunction/InnerProduct.lean

@@ -38,16 +38,14 @@ noncomputable def ContDiffBumpBase.ofInnerProductSpace : ContDiffBumpBase E wher
     apply ContDiffAt.contDiffWithinAt
     rw [← sub_pos] at hR
     rcases eq_or_ne x 0 with rfl | hx
-    · have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) :=
-        (continuousAt_fst.sub continuousAt_snd.norm).div
-          (continuousAt_fst.sub continuousAt_const) hR.ne'
+    · have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) := by
+        fun_prop (disch := positivity)
       have B : ∀ᶠ p in 𝓝 (R, (0 : E)), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1) :=
         A.eventually <| le_mem_nhds <| (one_lt_div hR).2 <| sub_lt_sub_left (by simp) _
       refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦
         smoothTransition.one_of_one_le
-    · refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ ?_ hR.ne')
-      · exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)
-      · exact contDiffAt_fst.sub contDiffAt_const
+    · refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ (by fun_prop) hR.ne')
+      exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)
   eq_one _ hR _ hx := smoothTransition.one_of_one_le <| (one_le_div <| sub_pos.2 hR).2 <|
     sub_le_sub_left hx _
   support R hR := by

Mathlib/Analysis/Calculus/MeanValue.lean

@@ -151,8 +151,7 @@ theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b
       exact (lt_add_iff_pos_right _).2 hr
     exact hx
   intro x hx
-  have : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0 :=
-    continuousWithinAt_const.add (continuousWithinAt_id.mul continuousWithinAt_const)
+  have : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0 := by fun_prop
   convert continuousWithinAt_const.closure_le _ this (Hr x hx) using 1 <;> simp
 
 /-- General fencing theorem for continuous functions with an estimate on the derivative.

Mathlib/Analysis/Calculus/Rademacher.lean

@@ -162,8 +162,7 @@ theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'
       simp only [B, A, _root_.sub_self, smul_eq_mul, mul_zero, zero_mul, norm_zero]
       exact indicator_nonneg (fun y _hy ↦ by positivity) _
   · rw [integrable_indicator_iff K_compact.measurableSet]
-    apply ContinuousOn.integrableOn_compact K_compact
-    exact (Continuous.mul continuous_const hg.norm).continuousOn
+    exact ContinuousOn.integrableOn_compact K_compact (by fun_prop)
   · filter_upwards [hf.ae_lineDifferentiableAt v] with x hx
     exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds
 

Mathlib/Analysis/Complex/CauchyIntegral.lean

@@ -515,8 +515,7 @@ theorem two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_c
   refine mem_closure_iff_nhds.2 fun t ht => ?_
   -- TODO: generalize to any vector space over `ℝ`
   set g : ℝ → ℂ := fun x => w + ofReal x
-  have : Tendsto g (𝓝 0) (𝓝 w) :=
-    (continuous_const.add continuous_ofReal).tendsto' 0 w (add_zero _)
+  have : Tendsto g (𝓝 0) (𝓝 w) := Continuous.tendsto' (by fun_prop) 0 w (add_zero _)
   rcases mem_nhds_iff_exists_Ioo_subset.1 (this <| inter_mem ht <| isOpen_ball.mem_nhds hw) with
     ⟨l, u, hlu₀, hlu_sub⟩
   obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).Nonempty := by

Mathlib/Analysis/Complex/OpenMapping.lean

@@ -154,8 +154,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal
     have h7 := h1.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hrz
     rw [show gray z 0 = g z₀ by simp [gray, ray], ← map_compose] at h7
     refine h7.trans (map_mono ?_)
-    have h10 : Continuous fun t : ℂ => z₀ + t • z :=
-      continuous_const.add (continuous_id'.smul continuous_const)
+    have h10 : Continuous fun t : ℂ => z₀ + t • z := by fun_prop
     simpa using h10.tendsto 0
 
 /-- The *open mapping theorem* for holomorphic functions, global version: if a function `g : E → ℂ`

Mathlib/Analysis/Complex/PhragmenLindelof.lean

@@ -722,8 +722,7 @@ theorem right_half_plane_of_bounded_on_real (hd : DiffContOnCl ℂ f {z | 0 < z.
   -- Taking the limit as `ε → 0`, we obtain the required inequality.
   suffices ∀ᶠ ε : ℝ in 𝓝[<] 0, ‖exp (ε * z) • f z‖ ≤ C by
     refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
-    apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'
-    simp
+    exact Continuous.tendsto' (by fun_prop) _ _ (by simp)
   filter_upwards [self_mem_nhdsWithin] with ε ε₀; change ε < 0 at ε₀
   set g : ℂ → E := fun z => exp (ε * z) • f z; change ‖g z‖ ≤ C
   replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re} :=