bump to nightly-2023-12-14-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/IndicatorFunction.lean

@@ -686,7 +686,7 @@ section CommMonoid
 
 variable [CommMonoid M]
 
-#print Set.prod_mulIndicator_subset_of_eq_one /-
+#print Finset.prod_mulIndicator_subset_of_eq_one /-
 /-- Consider a product of `g i (f i)` over a `finset`.  Suppose `g` is a
 function such as `pow`, which maps a second argument of `1` to
 `1`. Then if `f` is replaced by the corresponding multiplicative indicator
@@ -706,8 +706,8 @@ theorem prod_mulIndicator_subset_of_eq_one [One N] (f : α → N) (g : α → N
   · refine' fun i hi hn => _
     convert hg i
     exact mul_indicator_of_not_mem hn _
-#align set.prod_mul_indicator_subset_of_eq_one Set.prod_mulIndicator_subset_of_eq_one
-#align set.sum_indicator_subset_of_eq_zero Set.sum_indicator_subset_of_eq_zero
+#align set.prod_mul_indicator_subset_of_eq_one Finset.prod_mulIndicator_subset_of_eq_one
+#align set.sum_indicator_subset_of_eq_zero Finset.sum_indicator_subset_of_eq_zero
 -/
 
 /-- Consider a sum of `g i (f i)` over a `finset`. Suppose `g` is a
@@ -717,18 +717,18 @@ function such as multiplication, which maps a second argument of 0 to
 function `h`.)  Then if `f` is replaced by the corresponding indicator
 function, the `finset` may be replaced by a possibly larger `finset`
 without changing the value of the sum. -/
-add_decl_doc Set.sum_indicator_subset_of_eq_zero
+add_decl_doc Finset.sum_indicator_subset_of_eq_zero
 
-#print Set.prod_mulIndicator_subset /-
+#print Finset.prod_mulIndicator_subset /-
 /-- Taking the product of an indicator function over a possibly larger `finset` is the same as
 taking the original function over the original `finset`. -/
 @[to_additive
       "Summing an indicator function over a possibly larger `finset` is the same as summing\nthe original function over the original `finset`."]
 theorem prod_mulIndicator_subset (f : α → M) {s t : Finset α} (h : s ⊆ t) :
     ∏ i in s, f i = ∏ i in t, mulIndicator (↑s) f i :=
   prod_mulIndicator_subset_of_eq_one _ (fun a b => b) h fun _ => rfl
-#align set.prod_mul_indicator_subset Set.prod_mulIndicator_subset
-#align set.sum_indicator_subset Set.sum_indicator_subset
+#align set.prod_mul_indicator_subset Finset.prod_mulIndicator_subset
+#align set.sum_indicator_subset Finset.sum_indicator_subset
 -/
 
 #print Finset.prod_mulIndicator_eq_prod_filter /-
@@ -747,18 +747,18 @@ theorem Finset.prod_mulIndicator_eq_prod_filter (s : Finset ι) (f : ι → α 
 #align finset.sum_indicator_eq_sum_filter Finset.sum_indicator_eq_sum_filter
 -/
 
-#print Set.mulIndicator_finset_prod /-
+#print Finset.mulIndicator_prod /-
 @[to_additive]
-theorem mulIndicator_finset_prod (I : Finset ι) (s : Set α) (f : ι → α → M) :
+theorem mulIndicator_prod (I : Finset ι) (s : Set α) (f : ι → α → M) :
     mulIndicator s (∏ i in I, f i) = ∏ i in I, mulIndicator s (f i) :=
   (mulIndicatorHom M s).map_prod _ _
-#align set.mul_indicator_finset_prod Set.mulIndicator_finset_prod
-#align set.indicator_finset_sum Set.indicator_finset_sum
+#align set.mul_indicator_finset_prod Finset.mulIndicator_prod
+#align set.indicator_finset_sum Finset.indicator_sum
 -/
 
-#print Set.mulIndicator_finset_biUnion /-
+#print Finset.mulIndicator_biUnion /-
 @[to_additive]
-theorem mulIndicator_finset_biUnion {ι} (I : Finset ι) (s : ι → Set α) {f : α → M} :
+theorem mulIndicator_biUnion {ι} (I : Finset ι) (s : ι → Set α) {f : α → M} :
     (∀ i ∈ I, ∀ j ∈ I, i ≠ j → Disjoint (s i) (s j)) →
       mulIndicator (⋃ i ∈ I, s i) f = fun a => ∏ i in I, mulIndicator (s i) f a :=
   by
@@ -774,18 +774,18 @@ theorem mulIndicator_finset_biUnion {ι} (I : Finset ι) (s : ι → Set α) {f
   intro hx a' ha'
   refine' disjoint_left.1 (hI a (Finset.mem_insert_self _ _) a' (Finset.mem_insert_of_mem ha') _) hx
   exact (ne_of_mem_of_not_mem ha' haI).symm
-#align set.mul_indicator_finset_bUnion Set.mulIndicator_finset_biUnion
-#align set.indicator_finset_bUnion Set.indicator_finset_biUnion
+#align set.mul_indicator_finset_bUnion Finset.mulIndicator_biUnion
+#align set.indicator_finset_bUnion Finset.indicator_biUnion
 -/
 
-#print Set.mulIndicator_finset_biUnion_apply /-
+#print Finset.mulIndicator_biUnion_apply /-
 @[to_additive]
-theorem mulIndicator_finset_biUnion_apply {ι} (I : Finset ι) (s : ι → Set α) {f : α → M}
+theorem mulIndicator_biUnion_apply {ι} (I : Finset ι) (s : ι → Set α) {f : α → M}
     (h : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → Disjoint (s i) (s j)) (x : α) :
     mulIndicator (⋃ i ∈ I, s i) f x = ∏ i in I, mulIndicator (s i) f x := by
-  rw [Set.mulIndicator_finset_biUnion I s h]
-#align set.mul_indicator_finset_bUnion_apply Set.mulIndicator_finset_biUnion_apply
-#align set.indicator_finset_bUnion_apply Set.indicator_finset_biUnion_apply
+  rw [Finset.mulIndicator_biUnion I s h]
+#align set.mul_indicator_finset_bUnion_apply Finset.mulIndicator_biUnion_apply
+#align set.indicator_finset_bUnion_apply Finset.indicator_biUnion_apply
 -/
 
 end CommMonoid

Mathbin/Algebra/Star/Basic.lean

@@ -565,11 +565,11 @@ export StarModule (star_smul)
 
 attribute [simp] star_smul
 
-#print StarSemigroup.to_starModule /-
+#print StarMul.toStarModule /-
 /-- A commutative star monoid is a star module over itself via `monoid.to_mul_action`. -/
-instance StarSemigroup.to_starModule [CommMonoid R] [StarMul R] : StarModule R R :=
+instance StarMul.toStarModule [CommMonoid R] [StarMul R] : StarModule R R :=
   ⟨star_mul'⟩
-#align star_semigroup.to_star_module StarSemigroup.to_starModule
+#align star_semigroup.to_star_module StarMul.toStarModule
 -/
 
 namespace RingHomInvPair

Mathbin/Algebra/Support.lean

@@ -499,31 +499,31 @@ theorem support_div [GroupWithZero G₀] (f g : α → G₀) :
 #align function.support_div Function.support_div
 -/
 
-#print Function.mulSupport_prod /-
+#print Finset.mulSupport_prod /-
 @[to_additive]
 theorem mulSupport_prod [CommMonoid M] (s : Finset α) (f : α → β → M) :
     (mulSupport fun x => ∏ i in s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i) :=
   by
   rw [mul_support_subset_iff']
   simp only [mem_Union, not_exists, nmem_mul_support]
   exact fun x => Finset.prod_eq_one
-#align function.mul_support_prod Function.mulSupport_prod
-#align function.support_sum Function.support_sum
+#align function.mul_support_prod Finset.mulSupport_prod
+#align function.support_sum Finset.support_sum
 -/
 
-#print Function.support_prod_subset /-
+#print Finset.support_prod_subset /-
 theorem support_prod_subset [CommMonoidWithZero A] (s : Finset α) (f : α → β → A) :
     (support fun x => ∏ i in s, f i x) ⊆ ⋂ i ∈ s, support (f i) := fun x hx =>
   mem_iInter₂.2 fun i hi H => hx <| Finset.prod_eq_zero hi H
-#align function.support_prod_subset Function.support_prod_subset
+#align function.support_prod_subset Finset.support_prod_subset
 -/
 
-#print Function.support_prod /-
+#print Finset.support_prod /-
 theorem support_prod [CommMonoidWithZero A] [NoZeroDivisors A] [Nontrivial A] (s : Finset α)
     (f : α → β → A) : (support fun x => ∏ i in s, f i x) = ⋂ i ∈ s, support (f i) :=
   Set.ext fun x => by
     simp only [support, Ne.def, Finset.prod_eq_zero_iff, mem_set_of_eq, Set.mem_iInter, not_exists]
-#align function.support_prod Function.support_prod
+#align function.support_prod Finset.support_prod
 -/
 
 #print Function.mulSupport_one_add /-

Mathbin/Analysis/Calculus/Inverse.lean

@@ -472,21 +472,21 @@ protected theorem surjective [CompleteSpace E] (hf : ApproximatesLinearOn f (f'
 #align approximates_linear_on.surjective ApproximatesLinearOn.surjective
 -/
 
-#print ApproximatesLinearOn.toLocalEquiv /-
+#print ApproximatesLinearOn.toPartialEquiv /-
 /-- A map approximating a linear equivalence on a set defines a local equivalence on this set.
 Should not be used outside of this file, because it is superseded by `to_local_homeomorph` below.
 
 This is a first step towards the inverse function. -/
-def toLocalEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
-    (hc : Subsingleton E ∨ c < N⁻¹) : LocalEquiv E F :=
-  (hf.InjOn hc).toLocalEquiv _ _
-#align approximates_linear_on.to_local_equiv ApproximatesLinearOn.toLocalEquiv
+def toPartialEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
+    (hc : Subsingleton E ∨ c < N⁻¹) : PartialEquiv E F :=
+  (hf.InjOn hc).toPartialEquiv _ _
+#align approximates_linear_on.to_local_equiv ApproximatesLinearOn.toPartialEquiv
 -/
 
 #print ApproximatesLinearOn.inverse_continuousOn /-
 /-- The inverse function is continuous on `f '' s`. Use properties of `local_homeomorph` instead. -/
 theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
-    (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toLocalEquiv hc).symm (f '' s) :=
+    (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toPartialEquiv hc).symm (f '' s) :=
   by
   apply continuousOn_iff_continuous_restrict.2
   refine' ((hf.antilipschitz hc).to_rightInvOn' _ (hf.to_local_equiv hc).right_inv').Continuous
@@ -497,7 +497,7 @@ theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F)
 #print ApproximatesLinearOn.to_inv /-
 /-- The inverse function is approximated linearly on `f '' s` by `f'.symm`. -/
 theorem to_inv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
-    ApproximatesLinearOn (hf.toLocalEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s)
+    ApproximatesLinearOn (hf.toPartialEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s)
       (N * (N⁻¹ - c)⁻¹ * c) :=
   by
   intro x hx y hy
@@ -534,7 +534,7 @@ returns a local homeomorph with `to_fun = f` and `source = s`. -/
 def toPartialHomeomorph (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
     (hc : Subsingleton E ∨ c < N⁻¹) (hs : IsOpen s) : PartialHomeomorph E F
     where
-  toLocalEquiv := hf.toLocalEquiv hc
+  toPartialEquiv := hf.toPartialEquiv hc
   open_source := hs
   open_target :=
     hf.open_image f'.toNonlinearRightInverse hs

Mathbin/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -56,11 +56,11 @@ theorem expMapCircle_arg (z : circle) : expMapCircle (arg z) = z :=
 
 namespace circle
 
-#print circle.argLocalEquiv /-
+#print circle.argPartialEquiv /-
 /-- `complex.arg ∘ coe` and `exp_map_circle` define a local equivalence between `circle and `ℝ` with
 `source = set.univ` and `target = set.Ioc (-π) π`. -/
 @[simps (config := { fullyApplied := false })]
-noncomputable def argLocalEquiv : LocalEquiv circle ℝ
+noncomputable def argPartialEquiv : PartialEquiv circle ℝ
     where
   toFun := arg ∘ coe
   invFun := expMapCircle
@@ -70,7 +70,7 @@ noncomputable def argLocalEquiv : LocalEquiv circle ℝ
   map_target' := mapsTo_univ _ _
   left_inv' z _ := expMapCircle_arg z
   right_inv' x hx := arg_expMapCircle hx.1 hx.2
-#align circle.arg_local_equiv circle.argLocalEquiv
+#align circle.arg_local_equiv circle.argPartialEquiv
 -/
 
 #print circle.argEquiv /-
@@ -80,8 +80,8 @@ noncomputable def argEquiv : circle ≃ Ioc (-π) π
     where
   toFun z := ⟨arg z, neg_pi_lt_arg _, arg_le_pi _⟩
   invFun := expMapCircle ∘ coe
-  left_inv z := argLocalEquiv.left_inv trivial
-  right_inv x := Subtype.ext <| argLocalEquiv.right_inv x.2
+  left_inv z := argPartialEquiv.left_inv trivial
+  right_inv x := Subtype.ext <| argPartialEquiv.right_inv x.2
 #align circle.arg_equiv circle.argEquiv
 -/
 
@@ -95,13 +95,13 @@ theorem leftInverse_expMapCircle_arg : LeftInverse expMapCircle (arg ∘ coe) :=
 
 #print invOn_arg_expMapCircle /-
 theorem invOn_arg_expMapCircle : InvOn (arg ∘ coe) expMapCircle (Ioc (-π) π) univ :=
-  circle.argLocalEquiv.symm.InvOn
+  circle.argPartialEquiv.symm.InvOn
 #align inv_on_arg_exp_map_circle invOn_arg_expMapCircle
 -/
 
 #print surjOn_expMapCircle_neg_pi_pi /-
 theorem surjOn_expMapCircle_neg_pi_pi : SurjOn expMapCircle (Ioc (-π) π) univ :=
-  circle.argLocalEquiv.symm.SurjOn
+  circle.argPartialEquiv.symm.SurjOn
 #align surj_on_exp_map_circle_neg_pi_pi surjOn_expMapCircle_neg_pi_pi
 -/
 

Mathbin/Control/Random.lean

@@ -79,20 +79,16 @@ local infixl:41 " .. " => Set.Icc
 
 open Stream'
 
-#print BoundedRandom /-
 /-- `bounded_random α` gives us machinery to generate values of type `α` between certain bounds -/
 class BoundedRandom (α : Type u) [Preorder α] where
   randomR : ∀ (g) [RandomGen g] (x y : α), x ≤ y → RandG g (x .. y)
-#align bounded_random BoundedRandom
--/
+#align bounded_random BoundedRandomₓ
 
-#print Random /-
-/- ./././Mathport/Syntax/Translate/Command.lean:394:30: infer kinds are unsupported in Lean 4: #[`Random] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:394:30: infer kinds are unsupported in Lean 4: #[`Randomₓ] [] -/
 /-- `random α` gives us machinery to generate values of type `α` -/
 class Random (α : Type u) where
-  Random : ∀ (g : Type) [RandomGen g], RandG g α
-#align random Random
--/
+  Randomₓ : ∀ (g : Type) [RandomGen g], RandG g α
+#align random Randomₓ
 
 /-- shift_31_left = 2^31; multiplying by it shifts the binary
 representation of a number left by 31 bits, dividing by it shifts it
@@ -121,7 +117,7 @@ section Random
 
 variable [Random α]
 
-export Random (Random)
+export Random (Randomₓ)
 
 /-- Generate a random value of type `α`. -/
 def random : RandG g α :=
@@ -300,7 +296,8 @@ instance intBoundedRandom : BoundedRandom ℤ
               (le_of_eq <| Int.ofNat_natAbs_eq_of_nonneg (Int.sub_nonneg_of_le hxy))⟩
 #align int_bounded_random intBoundedRandom
 
-instance finRandom (n : ℕ) [NeZero n] : Random (Fin n) where Random g inst := @Fin.random g inst _ _
+instance finRandom (n : ℕ) [NeZero n] : Random (Fin n)
+    where Randomₓ g inst := @Fin.random g inst _ _
 #align fin_random finRandom
 
 instance finBoundedRandom (n : ℕ) : BoundedRandom (Fin n)
@@ -326,7 +323,7 @@ theorem bool_ofNat_mem_Icc_of_mem_Icc_toNat (x y : Bool) (n : ℕ) :
 #align bool_of_nat_mem_Icc_of_mem_Icc_to_nat bool_ofNat_mem_Icc_of_mem_Icc_toNat
 
 instance : Random Bool
-    where Random g inst :=
+    where Randomₓ g inst :=
     (Bool.ofNat ∘ Subtype.val) <$> @BoundedRandom.randomR ℕ _ _ g inst 0 1 (Nat.zero_le _)
 
 instance : BoundedRandom Bool
@@ -354,7 +351,7 @@ def Std.BitVec.randomR {n : ℕ} (x y : Std.BitVec n) (h : x ≤ y) : RandG g (x
 open Nat
 
 instance randomBitvec (n : ℕ) : Random (Std.BitVec n)
-    where Random _ inst := @Std.BitVec.random _ inst n
+    where Randomₓ _ inst := @Std.BitVec.random _ inst n
 #align random_bitvec randomBitvec
 
 instance boundedRandomBitvec (n : ℕ) : BoundedRandom (Std.BitVec n)

Mathbin/Geometry/Euclidean/Circumcenter.lean

@@ -725,7 +725,7 @@ theorem sum_centroidWeightsWithCircumcenter {n : ℕ} {fs : Finset (Fin (n + 1))
     ∑ i, centroidWeightsWithCircumcenter fs i = 1 :=
   by
   simp_rw [sum_points_with_circumcenter, centroid_weights_with_circumcenter, add_zero, ←
-    fs.sum_centroid_weights_eq_one_of_nonempty ℝ h, Set.sum_indicator_subset _ fs.subset_univ]
+    fs.sum_centroid_weights_eq_one_of_nonempty ℝ h, Finset.sum_indicator_subset _ fs.subset_univ]
   rcongr
 #align affine.simplex.sum_centroid_weights_with_circumcenter Affine.Simplex.sum_centroidWeightsWithCircumcenter
 -/
@@ -742,7 +742,7 @@ theorem centroid_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : S
   simp_rw [centroid_def, affine_combination_apply, weighted_vsub_of_point_apply,
     sum_points_with_circumcenter, centroid_weights_with_circumcenter,
     points_with_circumcenter_point, zero_smul, add_zero, centroid_weights,
-    Set.sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (card fs : ℝ)⁻¹)
+    Finset.sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (card fs : ℝ)⁻¹)
       (fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun i =>
       zero_smul ℝ _,
     Set.indicator_apply]