bump to nightly-2023-09-28-06

mathlib commit leanprover-community/mathlib@ce64cd3

Mathbin/Data/Set/Basic.lean

@@ -4092,8 +4092,10 @@ theorem subset_right_of_subset_union (h : s ⊆ t ∪ u) (hab : Disjoint s t) :
 
 end Disjoint
 
+#print Prop.compl_singleton /-
 @[simp]
 theorem Prop.compl_singleton (p : Prop) : ({p}ᶜ : Set Prop) = {¬p} :=
   ext fun q => by simpa [@Iff.comm q] using not_iff
 #align Prop.compl_singleton Prop.compl_singleton
+-/
 

Mathbin/Data/Set/Image.lean

@@ -231,13 +231,17 @@ theorem nonempty_of_nonempty_preimage {s : Set β} {f : α → β} (hf : (f ⁻
 #align set.nonempty_of_nonempty_preimage Set.nonempty_of_nonempty_preimage
 -/
 
+#print Set.preimage_singleton_true /-
 @[simp]
 theorem preimage_singleton_true (p : α → Prop) : p ⁻¹' {True} = {a | p a} := by ext; simp
 #align set.preimage_singleton_true Set.preimage_singleton_true
+-/
 
+#print Set.preimage_singleton_false /-
 @[simp]
 theorem preimage_singleton_false (p : α → Prop) : p ⁻¹' {False} = {a | ¬p a} := by ext; simp
 #align set.preimage_singleton_false Set.preimage_singleton_false
+-/
 
 #print Set.preimage_subtype_coe_eq_compl /-
 theorem preimage_subtype_coe_eq_compl {α : Type _} {s u v : Set α} (hsuv : s ⊆ u ∪ v)
@@ -1714,9 +1718,11 @@ theorem LeftInverse.preimage_preimage {g : β → α} (h : LeftInverse g f) (s :
 #align function.left_inverse.preimage_preimage Function.LeftInverse.preimage_preimage
 -/
 
+#print Function.Involutive.preimage /-
 protected theorem Involutive.preimage {f : α → α} (hf : Involutive f) : Involutive (preimage f) :=
   hf.RightInverse.preimage_preimage
 #align function.involutive.preimage Function.Involutive.preimage
+-/
 
 end Function
 

Mathbin/MeasureTheory/Function/UniformIntegrable.lean

@@ -1110,9 +1110,9 @@ theorem uniformIntegrable_iff [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ 
 #align measure_theory.uniform_integrable_iff MeasureTheory.uniformIntegrable_iff
 -/
 
-#print MeasureTheory.uniformIntegrable_average /-
+#print MeasureTheory.uniformIntegrable_average_real /-
 /-- The averaging of a uniformly integrable sequence is also uniformly integrable. -/
-theorem uniformIntegrable_average (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf : UniformIntegrable f p μ) :
+theorem uniformIntegrable_average_real (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf : UniformIntegrable f p μ) :
     UniformIntegrable (fun n => (∑ i in Finset.range n, f i) / n) p μ :=
   by
   obtain ⟨hf₁, hf₂, hf₃⟩ := hf
@@ -1164,7 +1164,7 @@ theorem uniformIntegrable_average (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf :
         ENNReal.inv_mul_cancel _ (ENNReal.nat_ne_top _), one_mul]
       · exact le_rfl
       all_goals simpa only [Ne.def, Nat.cast_eq_zero]
-#align measure_theory.uniform_integrable_average MeasureTheory.uniformIntegrable_average
+#align measure_theory.uniform_integrable_average MeasureTheory.uniformIntegrable_average_real
 -/
 
 end UniformIntegrable

Mathbin/MeasureTheory/MeasurableSpace.lean

@@ -230,16 +230,20 @@ theorem le_map_comap : m ≤ (m.comap g).map g :=
 
 end Functors
 
+#print MeasurableSpace.map_const /-
 @[simp]
 theorem map_const {m} (b : β) : MeasurableSpace.map (fun a : α => b) m = ⊤ :=
   eq_top_iff.2 <| by rintro s hs;
     by_cases b ∈ s <;> change MeasurableSet (preimage _ _) <;> simp [*]
 #align measurable_space.map_const MeasurableSpace.map_const
+-/
 
+#print MeasurableSpace.comap_const /-
 @[simp]
 theorem comap_const {m} (b : β) : MeasurableSpace.comap (fun a : α => b) m = ⊥ :=
   eq_bot_iff.2 <| by rintro _ ⟨s, -, rfl⟩; by_cases b ∈ s <;> simp [*]
 #align measurable_space.comap_const MeasurableSpace.comap_const
+-/
 
 #print MeasurableSpace.comap_generateFrom /-
 theorem comap_generateFrom {f : α → β} {s : Set (Set β)} :
@@ -476,9 +480,11 @@ instance : MeasurableSpace PUnit :=
 instance : MeasurableSpace Bool :=
   ⊤
 
-instance Prop.measurableSpace : MeasurableSpace Prop :=
+#print Prop.instMeasurableSpace /-
+instance Prop.instMeasurableSpace : MeasurableSpace Prop :=
   ⊤
-#align Prop.measurable_space Prop.measurableSpace
+#align Prop.measurable_space Prop.instMeasurableSpace
+-/
 
 instance : MeasurableSpace ℕ :=
   ⊤
@@ -498,9 +504,11 @@ instance : MeasurableSingletonClass PUnit :=
 instance : MeasurableSingletonClass Bool :=
   ⟨fun _ => trivial⟩
 
-instance Prop.measurableSingletonClass : MeasurableSingletonClass Prop :=
+#print Prop.instMeasurableSingletonClass /-
+instance Prop.instMeasurableSingletonClass : MeasurableSingletonClass Prop :=
   ⟨fun _ => trivial⟩
-#align Prop.measurable_singleton_class Prop.measurableSingletonClass
+#align Prop.measurable_singleton_class Prop.instMeasurableSingletonClass
+-/
 
 instance : MeasurableSingletonClass ℕ :=
   ⟨fun _ => trivial⟩
@@ -567,6 +575,7 @@ theorem measurable_to_bool {f : α → Bool} (h : MeasurableSet (f ⁻¹' {true}
 #align measurable_to_bool measurable_to_bool
 -/
 
+#print measurable_to_prop /-
 theorem measurable_to_prop {f : α → Prop} (h : MeasurableSet (f ⁻¹' {True})) : Measurable f :=
   by
   refine' measurable_to_countable' fun x => _
@@ -576,6 +585,7 @@ theorem measurable_to_prop {f : α → Prop} (h : MeasurableSet (f ⁻¹' {True}
     simpa only [hx, ← preimage_compl, Prop.compl_singleton, not_true,
       preimage_singleton_false] using h.compl
 #align measurable_to_prop measurable_to_prop
+-/
 
 #print measurable_findGreatest' /-
 theorem measurable_findGreatest' {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N : ℕ}
@@ -1273,16 +1283,20 @@ variable {p : α → Prop}
 
 variable [MeasurableSpace α]
 
+#print measurableSet_setOf /-
 @[simp]
 theorem measurableSet_setOf : MeasurableSet {a | p a} ↔ Measurable p :=
   ⟨fun h => measurable_to_prop <| by simpa only [preimage_singleton_true], fun h => by
     simpa using h (measurable_set_singleton True)⟩
 #align measurable_set_set_of measurableSet_setOf
+-/
 
+#print measurable_mem /-
 @[simp]
 theorem measurable_mem : Measurable (· ∈ s) ↔ MeasurableSet s :=
   measurableSet_setOf.symm
 #align measurable_mem measurable_mem
+-/
 
 alias ⟨_, Measurable.setOf⟩ := measurableSet_setOf
 #align measurable.set_of Measurable.setOf
@@ -1296,6 +1310,7 @@ end Constructions
 
 namespace MeasurableSpace
 
+#print MeasurableSpace.generateFrom_singleton /-
 /-- The sigma-algebra generated by a single set `s` is `{∅, s, sᶜ, univ}`. -/
 @[simp]
 theorem generateFrom_singleton (s : Set α) : generateFrom {s} = MeasurableSpace.comap (· ∈ s) ⊤ :=
@@ -1306,6 +1321,7 @@ theorem generateFrom_singleton (s : Set α) : generateFrom {s} = MeasurableSpace
   rintro _ ⟨u, -, rfl⟩
   exact (show MeasurableSet s from generate_measurable.basic _ <| mem_singleton s).Mem trivial
 #align measurable_space.generate_from_singleton MeasurableSpace.generateFrom_singleton
+-/
 
 end MeasurableSpace
 
@@ -1646,10 +1662,12 @@ theorem measurableSet_image (e : α ≃ᵐ β) {s : Set α} : MeasurableSet (e '
 #align measurable_equiv.measurable_set_image MeasurableEquiv.measurableSet_image
 -/
 
+#print MeasurableEquiv.map_eq /-
 @[simp]
 theorem map_eq (e : α ≃ᵐ β) : MeasurableSpace.map e ‹_› = ‹_› :=
   e.Measurable.le_map.antisymm' fun s => e.measurableSet_preimage.1
 #align measurable_equiv.map_eq MeasurableEquiv.map_eq
+-/
 
 #print MeasurableEquiv.measurableEmbedding /-
 /-- A measurable equivalence is a measurable embedding. -/
@@ -1962,6 +1980,7 @@ def sumCompl {s : Set α} [DecidablePred s] (hs : MeasurableSet s) : Sum s (sᶜ
 #align measurable_equiv.sum_compl MeasurableEquiv.sumCompl
 -/
 
+#print MeasurableEquiv.ofInvolutive /-
 /-- Convert a measurable involutive function `f` to a measurable permutation with
 `to_fun = inv_fun = f`. See also `function.involutive.to_perm`. -/
 @[simps toEquiv]
@@ -1970,31 +1989,39 @@ def ofInvolutive (f : α → α) (hf : Involutive f) (hf' : Measurable f) : α 
     measurable_to_fun := hf'
     measurable_inv_fun := hf' }
 #align measurable_equiv.of_involutive MeasurableEquiv.ofInvolutive
+-/
 
+#print MeasurableEquiv.ofInvolutive_apply /-
 @[simp]
 theorem ofInvolutive_apply (f : α → α) (hf : Involutive f) (hf' : Measurable f) (a : α) :
     ofInvolutive f hf hf' a = f a :=
   rfl
 #align measurable_equiv.of_involutive_apply MeasurableEquiv.ofInvolutive_apply
+-/
 
+#print MeasurableEquiv.ofInvolutive_symm /-
 @[simp]
 theorem ofInvolutive_symm (f : α → α) (hf : Involutive f) (hf' : Measurable f) :
     (ofInvolutive f hf hf').symm = ofInvolutive f hf hf' :=
   rfl
 #align measurable_equiv.of_involutive_symm MeasurableEquiv.ofInvolutive_symm
+-/
 
 end MeasurableEquiv
 
 namespace MeasurableEmbedding
 
 variable [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {g : β → α}
 
+#print MeasurableEmbedding.comap_eq /-
 @[simp]
 theorem comap_eq (hf : MeasurableEmbedding f) : MeasurableSpace.comap f ‹_› = ‹_› :=
   hf.Measurable.comap_le.antisymm fun s h =>
     ⟨_, hf.measurableSet_image' h, hf.Injective.preimage_image _⟩
 #align measurable_embedding.comap_eq MeasurableEmbedding.comap_eq
+-/
 
+#print MeasurableEmbedding.iff_comap_eq /-
 theorem iff_comap_eq :
     MeasurableEmbedding f ↔
       Injective f ∧ MeasurableSpace.comap f ‹_› = ‹_› ∧ MeasurableSet (range f) :=
@@ -2006,6 +2033,7 @@ theorem iff_comap_eq :
         rintro _ ⟨s, hs, rfl⟩
         simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2 }⟩
 #align measurable_embedding.iff_comap_eq MeasurableEmbedding.iff_comap_eq
+-/
 
 #print MeasurableEmbedding.equivImage /-
 /-- A set is equivalent to its image under a function `f` as measurable spaces,
@@ -2110,6 +2138,7 @@ noncomputable def schroederBernstein {f : α → β} {g : β → α} (hf : Measu
 
 end MeasurableEmbedding
 
+#print MeasurableSpace.comap_compl /-
 theorem MeasurableSpace.comap_compl {m' : MeasurableSpace β} [BooleanAlgebra β]
     (h : Measurable (compl : β → β)) (f : α → β) :
     MeasurableSpace.comap (fun a => f aᶜ) inferInstance = MeasurableSpace.comap f inferInstance :=
@@ -2118,12 +2147,15 @@ theorem MeasurableSpace.comap_compl {m' : MeasurableSpace β} [BooleanAlgebra β
   congr
   exact (MeasurableEquiv.ofInvolutive _ compl_involutive h).MeasurableEmbedding.comap_eq
 #align measurable_space.comap_compl MeasurableSpace.comap_compl
+-/
 
+#print MeasurableSpace.comap_not /-
 @[simp]
 theorem MeasurableSpace.comap_not (p : α → Prop) :
     MeasurableSpace.comap (fun a => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance :=
   MeasurableSpace.comap_compl (fun _ _ => trivial) _
 #align measurable_space.comap_not MeasurableSpace.comap_not
+-/
 
 section CountablyGenerated
 

Mathbin/Order/BoundedOrder.lean

@@ -289,15 +289,13 @@ theorem OrderTop.ext_top {α} {hA : PartialOrder α} (A : OrderTop α) {hB : Par
 #align order_top.ext_top OrderTop.ext_top
 -/
 
-#print OrderTop.ext /-
 theorem OrderTop.ext {α} [PartialOrder α] {A B : OrderTop α} : A = B :=
   by
   have tt := OrderTop.ext_top A B fun _ _ => Iff.rfl
   cases' A with _ ha; cases' B with _ hb
   congr
   exact le_antisymm (hb _) (ha _)
 #align order_top.ext OrderTop.ext
--/
 
 #print OrderBot /-
 /-- An order is an `order_bot` if it has a least element.
@@ -562,15 +560,13 @@ theorem OrderBot.ext_bot {α} {hA : PartialOrder α} (A : OrderBot α) {hB : Par
 #align order_bot.ext_bot OrderBot.ext_bot
 -/
 
-#print OrderBot.ext /-
 theorem OrderBot.ext {α} [PartialOrder α] {A B : OrderBot α} : A = B :=
   by
   have tt := OrderBot.ext_bot A B fun _ _ => Iff.rfl
   cases' A with a ha; cases' B with b hb
   congr
   exact le_antisymm (ha _) (hb _)
 #align order_bot.ext OrderBot.ext
--/
 
 section SemilatticeSupTop
 
@@ -678,7 +674,6 @@ class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α
 instance (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ :=
   { OrderDual.orderTop α, OrderDual.orderBot α with }
 
-#print BoundedOrder.ext /-
 theorem BoundedOrder.ext {α} [PartialOrder α] {A B : BoundedOrder α} : A = B :=
   by
   have ht : @BoundedOrder.toOrderTop α _ A = @BoundedOrder.toOrderTop α _ B := OrderTop.ext
@@ -691,7 +686,6 @@ theorem BoundedOrder.ext {α} [PartialOrder α] {A B : BoundedOrder α} : A = B
   · exact h.symm
   · exact h'.symm
 #align bounded_order.ext BoundedOrder.ext
--/
 
 section Logic
 

Mathbin/Probability/StrongLaw.lean

@@ -769,12 +769,12 @@ theorem strong_law_aux7 :
 
 end StrongLawNonneg
 
-#print ProbabilityTheory.strong_law_ae /-
+#print ProbabilityTheory.strong_law_ae_real /-
 /-- *Strong law of large numbers*, almost sure version: if `X n` is a sequence of independent
 identically distributed integrable real-valued random variables, then `∑ i in range n, X i / n`
 converges almost surely to `𝔼[X 0]`. We give here the strong version, due to Etemadi, that only
 requires pairwise independence. -/
-theorem strong_law_ae (X : ℕ → Ω → ℝ) (hint : Integrable (X 0))
+theorem strong_law_ae_real (X : ℕ → Ω → ℝ) (hint : Integrable (X 0))
     (hindep : Pairwise fun i j => IndepFun (X i) (X j)) (hident : ∀ i, IdentDistrib (X i) (X 0)) :
     ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i in range n, X i ω) / n) atTop (𝓝 𝔼[X 0]) :=
   by
@@ -794,7 +794,7 @@ theorem strong_law_ae (X : ℕ → Ω → ℝ) (hint : Integrable (X 0))
   convert hωpos.sub hωneg
   · simp only [← sub_div, ← sum_sub_distrib, max_zero_sub_max_neg_zero_eq_self]
   · simp only [← integral_sub hint.pos_part hint.neg_part, max_zero_sub_max_neg_zero_eq_self]
-#align probability_theory.strong_law_ae ProbabilityTheory.strong_law_ae
+#align probability_theory.strong_law_ae ProbabilityTheory.strong_law_ae_real
 -/
 
 end StrongLawAe

Mathbin/Topology/MetricSpace/Lipschitz.lean

@@ -372,11 +372,11 @@ theorem edist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f)
 #align lipschitz_with.edist_iterate_succ_le_geometric LipschitzWith.edist_iterate_succ_le_geometric
 -/
 
-#print LipschitzWith.mul /-
-protected theorem mul {f g : Function.End α} {Kf Kg} (hf : LipschitzWith Kf f)
+#print LipschitzWith.mul_end /-
+protected theorem mul_end {f g : Function.End α} {Kf Kg} (hf : LipschitzWith Kf f)
     (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f * g : Function.End α) :=
   hf.comp hg
-#align lipschitz_with.mul LipschitzWith.mul
+#align lipschitz_with.mul LipschitzWith.mul_end
 -/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
@@ -390,12 +390,12 @@ protected theorem list_prod (f : ι → Function.End α) (K : ι → ℝ≥0)
 #align lipschitz_with.list_prod LipschitzWith.list_prod
 -/
 
-#print LipschitzWith.pow /-
-protected theorem pow {f : Function.End α} {K} (h : LipschitzWith K f) :
+#print LipschitzWith.pow_end /-
+protected theorem pow_end {f : Function.End α} {K} (h : LipschitzWith K f) :
     ∀ n : ℕ, LipschitzWith (K ^ n) (f ^ n : Function.End α)
   | 0 => by simpa only [pow_zero] using LipschitzWith.id
   | n + 1 => by rw [pow_succ, pow_succ]; exact h.mul (pow n)
-#align lipschitz_with.pow LipschitzWith.pow
+#align lipschitz_with.pow LipschitzWith.pow_end
 -/
 
 end Emetric