chore: fix non-terminal simps followed by fun_prop (leanprover-community#30048)

In most cases, these can be `dsimp; fun_prop` instead (which shows more clearly what is going on).
In two cases where `simp` was actually necessary, squeeze it.
Extracted from leanprover-community#28962, but hopefully also makes sense on its own.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: grunweg

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

@@ -142,7 +142,7 @@ noncomputable def realContinuousMapOfNNReal (φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥
 @[fun_prop]
 lemma continuous_realContinuousMapOfNNReal (φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A)
     (hφ : Continuous φ) : Continuous φ.realContinuousMapOfNNReal := by
-  simp [realContinuousMapOfNNReal]
+  dsimp [realContinuousMapOfNNReal]
   fun_prop
 
 end IsTopologicalRing
@@ -328,7 +328,7 @@ noncomputable def realContinuousMapZeroOfNNReal (φ : C(X, ℝ≥0)₀ →⋆ₙ
 @[fun_prop]
 lemma continuous_realContinuousMapZeroOfNNReal (φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A)
     (hφ : Continuous φ) : Continuous φ.realContinuousMapZeroOfNNReal := by
-  simp [realContinuousMapZeroOfNNReal]
+  dsimp [realContinuousMapZeroOfNNReal]
   fun_prop
 
 end IsTopologicalRing
@@ -444,7 +444,7 @@ lemma NonUnitalStarAlgHomClass.map_cfcₙ (φ : F) (f : R → R) (a : A)
     · simp [cfcₙHom_id]
     · congr
   all_goals
-    simp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]
+    dsimp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]
     fun_prop
 
 /-- Non-unital star algebra homomorphisms commute with the non-unital continuous functional
@@ -492,7 +492,7 @@ lemma StarAlgHomClass.map_cfc (φ : F) (f : R → R) (a : A)
     · simp [cfcHom_id]
     · congr
   all_goals
-    simp [ContinuousMap.compStarAlgHom']
+    dsimp [ContinuousMap.compStarAlgHom']
     fun_prop
 
 /-- Star algebra homomorphisms commute with the continuous functional calculus.

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -625,7 +625,7 @@ variable {n : MeasurableSpace β} in
 lemma Finset.stronglyMeasurable_prod_apply {ι : Type*} {f : ι → α → β → M} {g : α → β}
     {s : Finset ι} (hf : ∀ i ∈ s, StronglyMeasurable ↿(f i)) (hg : Measurable g) :
     StronglyMeasurable fun a ↦ (∏ i ∈ s, f i a) (g a) := by
-  simp; fun_prop (discharger := assumption)
+  simp only [Finset.prod_apply]; fun_prop (discharger := assumption)
 
 end CommMonoid
 

Mathlib/MeasureTheory/Group/Arithmetic.lean

@@ -120,7 +120,7 @@ theorem Measurable.mul [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable
 /-- Compositional version of `Measurable.add` for use by `fun_prop`. -/]
 lemma Measurable.mul' [MeasurableMul₂ M] {f g : α → β → M} {h : α → β} (hf : Measurable ↿f)
     (hg : Measurable ↿g) (hh : Measurable h) : Measurable fun a ↦ (f a * g a) (h a) := by
-  simp; fun_prop
+  dsimp; fun_prop
 
 @[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
 theorem AEMeasurable.mul' [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
@@ -272,7 +272,7 @@ theorem Measurable.div [MeasurableDiv₂ G] (hf : Measurable f) (hg : Measurable
 @[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
 lemma Measurable.div' [MeasurableDiv₂ G] {f g : α → β → G} {h : α → β} (hf : Measurable ↿f)
     (hg : Measurable ↿g) (hh : Measurable h) : Measurable fun a ↦ (f a / g a) (h a) := by
-  simp; fun_prop
+  dsimp; fun_prop
 
 @[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
 theorem AEMeasurable.div' [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
@@ -600,7 +600,7 @@ theorem Measurable.smul [MeasurableSMul₂ M X] (hf : Measurable f) (hg : Measur
 /-- Compositional version of `Measurable.vadd` for use by `fun_prop`. -/]
 lemma Measurable.smul' [MeasurableSMul₂ M X] {f : α → β → M} {g : α → β → X} {h : α → β}
     (hf : Measurable ↿f) (hg : Measurable ↿g) (hh : Measurable h) :
-    Measurable fun a ↦ (f a • g a) (h a) := by simp; fun_prop
+    Measurable fun a ↦ (f a • g a) (h a) := by dsimp; fun_prop
 
 @[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
 theorem AEMeasurable.smul [MeasurableSMul₂ M X] {μ : Measure α} (hf : AEMeasurable f μ)
@@ -918,7 +918,8 @@ theorem Finset.measurable_prod (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f
 /-- Compositional version of `Finset.measurable_sum` for use by `fun_prop`. -/]
 lemma Finset.measurable_prod_apply {f : ι → α → β → M} {g : α → β} {s : Finset ι}
     (hf : ∀ i ∈ s, Measurable ↿(f i)) (hg : Measurable g) :
-    Measurable fun a ↦ (∏ i ∈ s, f i a) (g a) := by simp; fun_prop (discharger := assumption)
+    Measurable fun a ↦ (∏ i ∈ s, f i a) (g a) := by
+  simp only [prod_apply]; fun_prop (discharger := assumption)
 
 @[deprecated (since := "2025-05-30")]
 alias Finset.measurable_sum' := Finset.measurable_sum_apply

Mathlib/MeasureTheory/Measure/WithDensity.lean

@@ -740,7 +740,7 @@ theorem mconv_withDensity_eq_mlconvolution₀ {f g : G → ℝ≥0∞}
     lintegral_lintegral_swap]
   · simp only [Pi.mul_apply, mul_inv_cancel_left, mlconvolution_def]
     conv in (∫⁻ _ , _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]
-  all_goals first | fun_prop | simp; fun_prop
+  all_goals first | fun_prop | dsimp; fun_prop
 
 @[to_additive]
 theorem mconv_withDensity_eq_mlconvolution {f g : G → ℝ≥0∞}

Mathlib/Topology/Homeomorph/Lemmas.lean

@@ -204,7 +204,7 @@ def sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
     (Π (st : S ⊕ T), A st) ≃ₜ (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t)) where
   __ := Equiv.sumPiEquivProdPi _
   continuous_toFun := .prodMk (by fun_prop) (by fun_prop)
-  continuous_invFun := continuous_pi <| by rintro (s | t) <;> simp <;> fun_prop
+  continuous_invFun := continuous_pi <| by rintro (s | t) <;> dsimp <;> fun_prop
 
 /-- The product `Π t : α, f t` of a family of topological spaces is homeomorphic to the
 space `f ⬝` when `α` only contains `⬝`.