chore(Archive): small golfs (leanprover-community#34688)

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

Author: grunweg

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -76,7 +76,7 @@ theorem disc_eq_regionBetween :
 
 /-- The disc is a `MeasurableSet`. -/
 theorem measurableSet_disc : MeasurableSet (disc r) := by
-  apply measurableSet_lt <;> apply Continuous.measurable <;> continuity
+  apply measurableSet_lt <;> fun_prop
 
 /-- **Area of a Circle**: The area of a disc with radius `r` is `π * r ^ 2`. -/
 theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
@@ -99,11 +99,10 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
   have hderiv : ∀ x ∈ Ioo (-r : ℝ) r, HasDerivAt F (2 * f x) x := by
     rintro x ⟨hx1, hx2⟩
     convert
-      ((hasDerivAt_const x ((r : ℝ) ^ 2)).fun_mul
-            ((hasDerivAt_arcsin _ _).comp x
-              ((hasDerivAt_const x (r : ℝ)⁻¹).fun_mul (hasDerivAt_id' x)))).fun_add
-        ((hasDerivAt_id' x).fun_mul
-          ((((hasDerivAt_id' x).fun_pow 2).const_sub ((r : ℝ) ^ 2)).sqrt _))
+      ((hasDerivAt_const x ((r : ℝ) ^ 2)).mul
+          ((hasDerivAt_arcsin _ _).comp x
+            ((hasDerivAt_const x (r : ℝ)⁻¹).mul (hasDerivAt_id' x)))).add
+        ((hasDerivAt_id' x).mul ((((hasDerivAt_id' x).fun_pow 2).const_sub ((r : ℝ) ^ 2)).sqrt _))
       using 1
     · have h₁ : (r : ℝ) ^ 2 - x ^ 2 > 0 := sub_pos_of_lt (sq_lt_sq' hx1 hx2)
       have h : sqrt ((r : ℝ) ^ 2 - x ^ 2) ^ 3 =
@@ -125,7 +124,7 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
   calc
     ∫ x in -r..r, 2 * f x = F r - F (-r) :=
       integral_eq_sub_of_hasDerivAt_of_le (neg_le_self r.2) (by fun_prop) hderiv
-        (continuous_const.mul hf).continuousOn.intervalIntegrable
+        (ContinuousOn.intervalIntegrable (by fun_prop))
     _ = NNReal.pi * (r : ℝ) ^ 2 := by
       norm_num [F, inv_mul_cancel₀ hlt.ne', ← mul_div_assoc, mul_comm π]
 

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -130,14 +130,10 @@ lemma volume_needleSpace : ℙ (needleSpace d) = ENNReal.ofReal (d * π) := by
 
 lemma measurable_needleCrossesIndicator : Measurable (needleCrossesIndicator l) := by
   unfold needleCrossesIndicator
-  refine Measurable.indicator measurable_const (IsClosed.measurableSet (IsClosed.and ?l ?r))
-  all_goals simp only [tsub_le_iff_right, zero_add, ← neg_le_iff_add_nonneg']
-  case' l => refine isClosed_le continuous_fst ?_
-  case' r => refine isClosed_le (Continuous.neg continuous_fst) ?_
-  all_goals
-    refine Continuous.mul (Continuous.mul ?_ continuous_const) continuous_const
-    simp_rw [← Function.comp_apply (f := Real.sin) (g := Prod.snd),
-      Continuous.comp Real.continuous_sin continuous_snd]
+  refine Measurable.indicator measurable_const (IsClosed.measurableSet (IsClosed.and ?_ ?_)) <;>
+    simp only [tsub_le_iff_right, zero_add, ← neg_le_iff_add_nonneg']
+  · exact isClosed_le continuous_fst (by fun_prop)
+  · exact isClosed_le continuous_fst.neg (by fun_prop)
 
 lemma stronglyMeasurable_needleCrossesIndicator :
     MeasureTheory.StronglyMeasurable (needleCrossesIndicator l) := by
@@ -274,8 +270,7 @@ the integral lemmas below.
 -/
 lemma intervalIntegrable_min_const_sin_mul (a b : ℝ) :
     IntervalIntegrable (fun (θ : ℝ) => min d (θ.sin * l)) ℙ a b := by
-  apply Continuous.intervalIntegrable
-  exact Continuous.min continuous_const (Continuous.mul Real.continuous_sin continuous_const)
+  apply Continuous.intervalIntegrable (by fun_prop)
 
 /--
 This equality is useful since `θ.sin` is increasing in `0..π / 2` (but not in `0..π`).