bump to nightly-2023-12-22-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Analysis/Calculus/Fderiv/RestrictScalars.lean

@@ -105,10 +105,10 @@ theorem Differentiable.restrictScalars (h : Differentiable 𝕜' f) : Differenti
 #align differentiable.restrict_scalars Differentiable.restrictScalars
 -/
 
-#print hasFDerivWithinAt_of_restrictScalars /-
-theorem hasFDerivWithinAt_of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x)
+#print HasFDerivWithinAt.of_restrictScalars /-
+theorem HasFDerivWithinAt.of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x)
     (H : f'.restrictScalars 𝕜 = g') : HasFDerivWithinAt f f' s x := by rw [← H] at h ; exact h
-#align has_fderiv_within_at_of_restrict_scalars hasFDerivWithinAt_of_restrictScalars
+#align has_fderiv_within_at_of_restrict_scalars HasFDerivWithinAt.of_restrictScalars
 -/
 
 #print hasFDerivAt_of_restrictScalars /-
@@ -134,7 +134,7 @@ theorem differentiableWithinAt_iff_restrictScalars (hf : DifferentiableWithinAt
   · rintro ⟨g', hg'⟩
     exact ⟨g', hs.eq (hg'.restrict_scalars 𝕜) hf.has_fderiv_within_at⟩
   · rintro ⟨f', hf'⟩
-    exact ⟨f', hasFDerivWithinAt_of_restrictScalars 𝕜 hf.has_fderiv_within_at hf'⟩
+    exact ⟨f', HasFDerivWithinAt.of_restrictScalars 𝕜 hf.has_fderiv_within_at hf'⟩
 #align differentiable_within_at_iff_restrict_scalars differentiableWithinAt_iff_restrictScalars
 -/
 

Mathbin/Analysis/Convex/Hull.lean

@@ -44,7 +44,7 @@ variable (𝕜) [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜
 #print convexHull /-
 /-- The convex hull of a set `s` is the minimal convex set that includes `s`. -/
 def convexHull : ClosureOperator (Set E) :=
-  ClosureOperator.mk₃ (fun s => ⋂ (t : Set E) (hst : s ⊆ t) (ht : Convex 𝕜 t), t) (Convex 𝕜)
+  ClosureOperator.ofPred (fun s => ⋂ (t : Set E) (hst : s ⊆ t) (ht : Convex 𝕜 t), t) (Convex 𝕜)
     (fun s =>
       Set.subset_iInter fun t => Set.subset_iInter fun hst => Set.subset_iInter fun ht => hst)
     (fun s => convex_iInter fun t => convex_iInter fun ht => convex_iInter id) fun s t hst ht =>
@@ -62,7 +62,7 @@ theorem subset_convexHull : s ⊆ convexHull 𝕜 s :=
 
 #print convex_convexHull /-
 theorem convex_convexHull : Convex 𝕜 (convexHull 𝕜 s) :=
-  ClosureOperator.closure_mem_mk₃ s
+  ClosureOperator.closure_mem_ofPred s
 #align convex_convex_hull convex_convexHull
 -/
 
@@ -82,7 +82,7 @@ theorem mem_convexHull_iff : x ∈ convexHull 𝕜 s ↔ ∀ t, s ⊆ t → Conv
 
 #print convexHull_min /-
 theorem convexHull_min (hst : s ⊆ t) (ht : Convex 𝕜 t) : convexHull 𝕜 s ⊆ t :=
-  ClosureOperator.closure_le_mk₃_iff (show s ≤ t from hst) ht
+  ClosureOperator.closure_le_ofPred_iff (show s ≤ t from hst) ht
 #align convex_hull_min convexHull_min
 -/
 
@@ -101,7 +101,7 @@ theorem convexHull_mono (hst : s ⊆ t) : convexHull 𝕜 s ⊆ convexHull 𝕜
 
 #print Convex.convexHull_eq /-
 theorem Convex.convexHull_eq (hs : Convex 𝕜 s) : convexHull 𝕜 s = s :=
-  ClosureOperator.mem_mk₃_closed hs
+  ClosureOperator.ofPred_isClosed hs
 #align convex.convex_hull_eq Convex.convexHull_eq
 -/
 

Mathbin/Analysis/MellinTransform.lean

@@ -312,7 +312,7 @@ theorem mellin_convergent_zero_of_isBigO {b : ℝ} {f : ℝ → ℝ}
     · show has_finite_integral (fun t => d * t ^ (s - b - 1)) _
       refine' (integrable.has_finite_integral _).const_mul _
       rw [← integrable_on, ← integrableOn_Ioc_iff_integrableOn_Ioo, ←
-        intervalIntegrable_iff_integrable_Ioc_of_le hε.le]
+        intervalIntegrable_iff_integrableOn_Ioc_of_le hε.le]
       exact intervalIntegral.intervalIntegrable_rpow' (by linarith)
     · refine' (ae_restrict_iff' measurableSet_Ioo).mpr (eventually_of_forall fun t ht => _)
       rw [mul_comm, norm_mul]
@@ -566,7 +566,7 @@ theorem hasMellin_one_Ioc {s : ℂ} (hs : 0 < re s) :
   simp_rw [HasMellin, mellin, MellinConvergent, ← indicator_smul, integrable_on,
     integrable_indicator_iff aux3, smul_eq_mul, integral_indicator aux3, mul_one, integrable_on,
     measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]
-  rw [← integrable_on, ← intervalIntegrable_iff_integrable_Ioc_of_le zero_le_one]
+  rw [← integrable_on, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
   refine' ⟨intervalIntegral.intervalIntegrable_cpow' aux1, _⟩
   rw [← intervalIntegral.integral_of_le zero_le_one, integral_cpow (Or.inl aux1), sub_add_cancel,
     of_real_zero, of_real_one, one_cpow, zero_cpow aux2, sub_zero]

Mathbin/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -83,7 +83,7 @@ theorem GammaIntegral_convergent {s : ℝ} (h : 0 < s) :
   constructor
   · rw [← integrableOn_Icc_iff_integrableOn_Ioc]
     refine' integrable_on.continuous_on_mul continuous_on_id.neg.exp _ is_compact_Icc
-    refine' (intervalIntegrable_iff_integrable_Icc_of_le zero_le_one).mp _
+    refine' (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp _
     exact interval_integrable_rpow' (by linarith)
   · refine' integrable_of_isBigO_exp_neg one_half_pos _ (Gamma_integrand_is_o _).IsBigO
     refine' continuous_on_id.neg.exp.mul (continuous_on_id.rpow_const _)
@@ -192,7 +192,7 @@ theorem tendsto_partialGamma {s : ℂ} (hs : 0 < s.re) :
 private theorem Gamma_integrand_interval_integrable (s : ℂ) {X : ℝ} (hs : 0 < s.re) (hX : 0 ≤ X) :
     IntervalIntegrable (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) volume 0 X :=
   by
-  rw [intervalIntegrable_iff_integrable_Ioc_of_le hX]
+  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hX]
   exact integrable_on.mono_set (Gamma_integral_convergent hs) Ioc_subset_Ioi_self
 
 private theorem Gamma_integrand_deriv_integrable_A {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
@@ -209,7 +209,7 @@ private theorem Gamma_integrand_deriv_integrable_B {s : ℂ} (hs : 0 < s.re) {Y
     (fun x => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) =
       (fun x => s * ((-x).exp * x ^ (s - 1)) : ℝ → ℂ) :=
     by ext1; ring
-  rw [this, intervalIntegrable_iff_integrable_Ioc_of_le hY]
+  rw [this, intervalIntegrable_iff_integrableOn_Ioc_of_le hY]
   constructor
   · refine' (continuous_on_const.mul _).AEStronglyMeasurable measurableSet_Ioc
     apply (continuous_of_real.comp continuous_neg.exp).ContinuousOn.mul

Mathbin/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -358,7 +358,7 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) :
     intro n
     rw [integrable_indicator_iff (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)), integrable_on,
       measure.restrict_restrict_of_subset Ioc_subset_Ioi_self, ← integrable_on, ←
-      intervalIntegrable_iff_integrable_Ioc_of_le (by positivity : (0 : ℝ) ≤ n)]
+      intervalIntegrable_iff_integrableOn_Ioc_of_le (by positivity : (0 : ℝ) ≤ n)]
     apply IntervalIntegrable.continuousOn_mul
     · refine' intervalIntegral.intervalIntegrable_cpow' _
       rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]

Mathbin/Analysis/SpecialFunctions/Gaussian.lean

@@ -85,7 +85,7 @@ theorem integrableOn_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (h
   constructor
   · rw [← integrableOn_Icc_iff_integrableOn_Ioc]
     refine' integrable_on.mul_continuous_on _ _ is_compact_Icc
-    · refine' (intervalIntegrable_iff_integrable_Icc_of_le zero_le_one).mp _
+    · refine' (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp _
       exact intervalIntegral.intervalIntegrable_rpow' hs
     · exact (continuous_exp.comp (continuous_const.mul (continuous_pow 2))).ContinuousOn
   · have B : (0 : ℝ) < 1 / 2 := by norm_num

Mathbin/Analysis/SpecialFunctions/Integrals.lean

@@ -132,13 +132,13 @@ theorem intervalIntegrable_cpow {r : ℂ} (h : 0 ≤ r.re ∨ (0 : ℝ) ∉ [a,
   rcases le_or_lt 0 c with (hc | hc)
   · -- case `0 ≤ c`: integrand is identically 1
     have : IntervalIntegrable (fun x => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
-    rw [intervalIntegrable_iff_integrable_Ioc_of_le hc] at this ⊢
+    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc] at this ⊢
     refine' integrable_on.congr_fun this (fun x hx => _) measurableSet_Ioc
     dsimp only
     rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
   · -- case `c < 0`: integrand is identically constant, *except* at `x = 0` if `r ≠ 0`.
     apply IntervalIntegrable.symm
-    rw [intervalIntegrable_iff_integrable_Ioc_of_le hc.le]
+    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le]
     have : Ioc c 0 = Ioo c 0 ∪ {(0 : ℝ)} :=
       by
       rw [← Ioo_union_Icc_eq_Ioc hc (le_refl 0), ← Icc_def]

Mathbin/Analysis/SpecialFunctions/JapaneseBracket.lean

@@ -118,7 +118,7 @@ theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ
     exact hr.le
   refine' lt_of_le_of_lt (set_lintegral_mono (by measurability) (by measurability) h_int) _
   refine' integrable_on.set_lintegral_lt_top _
-  rw [← intervalIntegrable_iff_integrable_Ioc_of_le zero_le_one]
+  rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
   apply intervalIntegral.intervalIntegrable_rpow'
   rwa [neg_lt_neg_iff, inv_mul_lt_iff' hr, one_mul]
 #align finite_integral_rpow_sub_one_pow_aux finite_integral_rpow_sub_one_pow_aux

Mathbin/CategoryTheory/Sites/Closed.lean

@@ -204,12 +204,12 @@ def closureOperator (X : C) : ClosureOperator (Sieve X) :=
 #align category_theory.grothendieck_topology.closure_operator CategoryTheory.GrothendieckTopology.closureOperator
 -/
 
-#print CategoryTheory.GrothendieckTopology.closed_iff_closed /-
+#print CategoryTheory.GrothendieckTopology.closureOperator_isClosed /-
 @[simp]
-theorem closed_iff_closed {X : C} (S : Sieve X) :
+theorem closureOperator_isClosed {X : C} (S : Sieve X) :
     S ∈ (J₁.ClosureOperator X).closed ↔ J₁.IsClosed S :=
   (J₁.isClosed_iff_close_eq_self S).symm
-#align category_theory.grothendieck_topology.closed_iff_closed CategoryTheory.GrothendieckTopology.closed_iff_closed
+#align category_theory.grothendieck_topology.closed_iff_closed CategoryTheory.GrothendieckTopology.closureOperator_isClosed
 -/
 
 end GrothendieckTopology

Mathbin/Computability/TmToPartrec.lean

@@ -361,9 +361,9 @@ theorem exists_code {n} {f : Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) :
       show ∀ x, pure x = [x] from fun _ => rfl] at hf ⊢
     refine' Part.ext fun x => _
     simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.map_eq_map, Part.bind_some,
-      exists_prop, eval, List.headI, pred_eval, Part.map_some, Bool.false_eq_decide_iff,
+      exists_prop, eval, List.headI, pred_eval, Part.map_some, false_eq_decide_iff,
       Part.mem_bind_iff, List.length, Part.mem_map_iff, Nat.mem_rfind, List.tail,
-      Bool.true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]
+      true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]
     constructor
     · rintro ⟨v', h1, rfl⟩
       suffices

Mathbin/Data/Bool/Basic.lean

@@ -72,18 +72,18 @@ theorem of_decide_iff {p : Prop} [Decidable p] : decide p ↔ p :=
 #align bool.of_to_bool_iff Bool.of_decide_iff
 -/
 
-#print Bool.true_eq_decide_iff /-
+#print true_eq_decide_iff /-
 @[simp]
 theorem true_eq_decide_iff {p : Prop} [Decidable p] : true = decide p ↔ p :=
   eq_comm.trans of_decide_iff
-#align bool.tt_eq_to_bool_iff Bool.true_eq_decide_iff
+#align bool.tt_eq_to_bool_iff true_eq_decide_iff
 -/
 
-#print Bool.false_eq_decide_iff /-
+#print false_eq_decide_iff /-
 @[simp]
 theorem false_eq_decide_iff {p : Prop} [Decidable p] : false = decide p ↔ ¬p :=
   eq_comm.trans (Bool.decide_false_iff _)
-#align bool.ff_eq_to_bool_iff Bool.false_eq_decide_iff
+#align bool.ff_eq_to_bool_iff false_eq_decide_iff
 -/
 
 #print Bool.decide_not /-

Mathbin/MeasureTheory/Integral/DivergenceTheorem.lean

@@ -428,7 +428,7 @@ theorem integral_eq_of_hasDerivWithinAt_off_countable_of_le (f f' : ℝ → E) {
       · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le
       · exact (volume_preserving_fun_unique (Fin 1) ℝ).symm _
       · intro x; rw [Fin.sum_univ_one, hF', e_symm, Pi.single_eq_same, one_smul]
-      · rw [intervalIntegrable_iff_integrable_Ioc_of_le hle] at Hi 
+      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi 
         exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm
     _ = f b - f a := by
       simp only [Fin.sum_univ_one, e_symm]

Mathbin/MeasureTheory/Integral/ExpDecay.lean

@@ -55,7 +55,7 @@ theorem integrable_of_isBigO_exp_neg {f : ℝ → ℝ} {a b : ℝ} (h0 : 0 < b)
   -- show integrable on `(a, v]` from continuity
   have int_left : integrable_on f (Ioc a v) :=
     by
-    rw [← intervalIntegrable_iff_integrable_Ioc_of_le (le_max_left a r)]
+    rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (le_max_left a r)]
     have u : Icc a v ⊆ Ici a := Icc_subset_Ici_self
     exact (h1.mono u).intervalIntegrable_of_Icc (le_max_left a r)
   suffices integrable_on f (Ioi v)

Mathbin/MeasureTheory/Integral/FundThmCalculus.lean

@@ -1211,11 +1211,11 @@ theorem sub_le_integral_of_hasDeriv_right_of_le_Ico (hab : a ≤ b) (hcont : Con
       _ = ∫ w in a..x, (G' w).toReal :=
         by
         apply integral_add_adjacent_intervals
-        · rw [intervalIntegrable_iff_integrable_Ioc_of_le ht.2.1]
+        · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le ht.2.1]
           exact
             integrable_on.mono_set G'int
               (Ioc_subset_Icc_self.trans (Icc_subset_Icc le_rfl ht.2.2.le))
-        · rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x.1.le]
+        · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x.1.le]
           apply integrable_on.mono_set G'int
           refine' Ioc_subset_Icc_self.trans (Icc_subset_Icc ht.2.1 (h'x.2.trans (min_le_right _ _)))
   -- now that we know that `s` contains `[a, b]`, we get the desired result by applying this to `b`.
@@ -1306,7 +1306,7 @@ theorem integral_eq_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : Continu
   exact
     integral_eq_sub_of_has_deriv_right_of_le_real hab (g.continuous.comp_continuous_on hcont)
       (fun x hx => g.has_fderiv_at.comp_has_deriv_within_at x (hderiv x hx))
-      (g.integrable_comp ((intervalIntegrable_iff_integrable_Icc_of_le hab).1 f'int))
+      (g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab).1 f'int))
 #align interval_integral.integral_eq_sub_of_has_deriv_right_of_le intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
 -/
 

Mathbin/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -830,7 +830,7 @@ theorem integral_Ioi_of_hasDerivAt_of_tendsto (hcont : ContinuousOn f (Ici a))
   apply
     intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
       fun y hy => hderiv y hy.1
-  rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
+  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
   exact f'int.mono (fun y hy => hy.1) le_rfl
 #align measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
 -/
@@ -872,7 +872,7 @@ theorem integrableOn_Ioi_deriv_of_nonneg (hcont : ContinuousOn g (Ici a))
       apply
         intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
           fun y hy => hderiv y hy.1
-      rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
+      rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
       exact
         intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
           (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1

Mathbin/MeasureTheory/Integral/IntervalIntegral.lean

@@ -97,11 +97,11 @@ theorem IntervalIntegrable.def (h : IntervalIntegrable f μ a b) : IntegrableOn
 #align interval_integrable.def IntervalIntegrable.def
 -/
 
-#print intervalIntegrable_iff_integrable_Ioc_of_le /-
-theorem intervalIntegrable_iff_integrable_Ioc_of_le (hab : a ≤ b) :
+#print intervalIntegrable_iff_integrableOn_Ioc_of_le /-
+theorem intervalIntegrable_iff_integrableOn_Ioc_of_le (hab : a ≤ b) :
     IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ := by
   rw [intervalIntegrable_iff, uIoc_of_le hab]
-#align interval_integrable_iff_integrable_Ioc_of_le intervalIntegrable_iff_integrable_Ioc_of_le
+#align interval_integrable_iff_integrable_Ioc_of_le intervalIntegrable_iff_integrableOn_Ioc_of_le
 -/
 
 #print intervalIntegrable_iff' /-
@@ -111,11 +111,11 @@ theorem intervalIntegrable_iff' [NoAtoms μ] :
 #align interval_integrable_iff' intervalIntegrable_iff'
 -/
 
-#print intervalIntegrable_iff_integrable_Icc_of_le /-
-theorem intervalIntegrable_iff_integrable_Icc_of_le {f : ℝ → E} {a b : ℝ} (hab : a ≤ b)
+#print intervalIntegrable_iff_integrableOn_Icc_of_le /-
+theorem intervalIntegrable_iff_integrableOn_Icc_of_le {f : ℝ → E} {a b : ℝ} (hab : a ≤ b)
     {μ : Measure ℝ} [NoAtoms μ] : IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ := by
-  rw [intervalIntegrable_iff_integrable_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc]
-#align interval_integrable_iff_integrable_Icc_of_le intervalIntegrable_iff_integrable_Icc_of_le
+  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc]
+#align interval_integrable_iff_integrable_Icc_of_le intervalIntegrable_iff_integrableOn_Icc_of_le
 -/
 
 #print MeasureTheory.Integrable.intervalIntegrable /-
@@ -1505,7 +1505,7 @@ theorem continuousOn_primitive [NoAtoms μ] (h_int : IntegrableOn f (Icc a b) μ
     rw [continuousOn_congr this]
     intro x₀ hx₀
     refine' continuous_within_at_primitive (measure_singleton x₀) _
-    simp only [intervalIntegrable_iff_integrable_Ioc_of_le, min_eq_left, max_eq_right, h]
+    simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, min_eq_left, max_eq_right, h]
     exact h_int.mono Ioc_subset_Icc_self le_rfl
   · rw [Icc_eq_empty h]
     exact continuousOn_empty _

Mathbin/ModelTheory/Substructures.lean

@@ -328,7 +328,7 @@ open Set
 /-- A substructure `S` includes `closure L s` if and only if it includes `s`. -/
 @[simp]
 theorem closure_le : closure L s ≤ S ↔ s ⊆ S :=
-  (closure L).closure_le_closed_iff_le s S.closed
+  (closure L).closure_le_iff s S.closed
 #align first_order.language.substructure.closure_le FirstOrder.Language.Substructure.closure_le
 -/