bump to nightly-2023-08-10-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Algebra/Quandle.lean

@@ -408,10 +408,12 @@ variable {S₁ : Type _} {S₂ : Type _} {S₃ : Type _} [Shelf S₁] [Shelf S
 instance : CoeFun (S₁ →◃ S₂) fun _ => S₁ → S₂ :=
   ⟨ShelfHom.toFun⟩
 
+#print ShelfHom.toFun_eq_coe /-
 @[simp]
 theorem toFun_eq_coe (f : S₁ →◃ S₂) : f.toFun = f :=
   rfl
 #align shelf_hom.to_fun_eq_coe ShelfHom.toFun_eq_coe
+-/
 
 #print ShelfHom.map_act /-
 @[simp]

Mathbin/Data/Complex/Basic.lean

@@ -1400,7 +1400,6 @@ theorem eq_re_ofReal_le {r : ℝ} {z : ℂ} (hz : (r : ℂ) ≤ z) : z = z.re :=
 #align complex.eq_re_of_real_le Complex.eq_re_ofReal_le
 -/
 
-#print Complex.strictOrderedCommRing /-
 /-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a strictly ordered ring.
 -/
 protected def strictOrderedCommRing : StrictOrderedCommRing ℂ :=
@@ -1411,11 +1410,9 @@ protected def strictOrderedCommRing : StrictOrderedCommRing ℂ :=
     mul_pos := fun z w hz hw => by
       simp [lt_def, mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1] }
 #align complex.strict_ordered_comm_ring Complex.strictOrderedCommRing
--/
 
 scoped[ComplexOrder] attribute [instance] Complex.strictOrderedCommRing
 
-#print Complex.starOrderedRing /-
 /-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a star ordered ring.
 (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
 -/
@@ -1435,7 +1432,6 @@ protected def starOrderedRing : StarOrderedRing ℂ :=
     · obtain ⟨s, rfl⟩ := h
       simp only [← norm_sq_eq_conj_mul_self, norm_sq_nonneg, zero_le_real, star_def]
 #align complex.star_ordered_ring Complex.starOrderedRing
--/
 
 scoped[ComplexOrder] attribute [instance] Complex.starOrderedRing
 

Mathbin/Data/Complex/Module.lean

@@ -152,11 +152,9 @@ section
 
 open scoped ComplexOrder
 
-#print Complex.orderedSMul /-
 protected theorem orderedSMul : OrderedSMul ℝ ℂ :=
   OrderedSMul.mk' fun a b r hab hr => ⟨by simp [hr, hab.1.le], by simp [hab.2]⟩
 #align complex.ordered_smul Complex.orderedSMul
--/
 
 scoped[ComplexOrder] attribute [instance] Complex.orderedSMul
 

Mathbin/LinearAlgebra/Matrix/Diagonal.lean

@@ -94,7 +94,7 @@ theorem range_diagonal [DecidableEq m] (w : m → K) :
 #align matrix.range_diagonal Matrix.range_diagonal
 -/
 
-#print Matrix.rank_diagonal /-
+#print LinearMap.rank_diagonal /-
 theorem rank_diagonal [DecidableEq m] [DecidableEq K] (w : m → K) :
     rank (diagonal w).toLin' = Fintype.card { i // w i ≠ 0 } :=
   by
@@ -105,7 +105,7 @@ theorem rank_diagonal [DecidableEq m] [DecidableEq K] (w : m → K) :
   rw [rank, range_diagonal, B₁, ← @rank_fun' K]
   apply LinearEquiv.rank_eq
   apply B₂
-#align matrix.rank_diagonal Matrix.rank_diagonal
+#align matrix.rank_diagonal LinearMap.rank_diagonal
 -/
 
 end Field

Mathbin/Probability/Martingale/Convergence.lean

@@ -196,10 +196,8 @@ theorem Submartingale.upcrossings_ae_lt_top' [IsFiniteMeasure μ] (hf : Submarti
       refine' lintegral_mono fun ω => _
       rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]
       by_cases hnonneg : 0 ≤ f n ω - a
-      ·
-        rw [LatticeOrderedCommGroup.pos_of_nonneg _ hnonneg, Real.norm_eq_abs,
-          abs_of_nonneg hnonneg]
-      · rw [LatticeOrderedCommGroup.pos_of_nonpos _ (not_le.1 hnonneg).le]
+      · rw [LatticeOrderedGroup.pos_of_nonneg _ hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
+      · rw [LatticeOrderedGroup.pos_of_nonpos _ (not_le.1 hnonneg).le]
         exact norm_nonneg _
       · simp only [Ne.def, ENNReal.coe_ne_top, not_false_iff]
     · simp only [hab, Ne.def, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]

Mathbin/Probability/Martingale/Upcrossing.lean

@@ -879,13 +879,13 @@ theorem crossing_pos_eq (hab : a < b) :
     refine' ⟨fun h => _, fun h => _⟩
     ·
       rwa [← sub_le_sub_iff_right a, ←
-        LatticeOrderedCommGroup.pos_eq_self_of_pos_pos (lt_of_lt_of_le hab' h)]
+        LatticeOrderedGroup.pos_eq_self_of_pos_pos (lt_of_lt_of_le hab' h)]
     · rw [← sub_le_sub_iff_right a] at h 
-      rwa [LatticeOrderedCommGroup.pos_of_nonneg _ (le_trans hab'.le h)]
+      rwa [LatticeOrderedGroup.pos_of_nonneg _ (le_trans hab'.le h)]
   have hf' : ∀ ω i, (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a :=
     by
     intro ω i
-    rw [LatticeOrderedCommGroup.pos_nonpos_iff, sub_nonpos]
+    rw [LatticeOrderedGroup.pos_nonpos_iff, sub_nonpos]
   induction' n with k ih
   · refine' ⟨rfl, _⟩
     simp only [lower_crossing_time_zero, hitting, Set.mem_Icc, Set.mem_Iic]
@@ -938,8 +938,8 @@ theorem mul_integral_upcrossingsBefore_le_integral_pos_part_aux [IsFiniteMeasure
   refine'
     le_trans (le_of_eq _)
       (integral_mul_upcrossings_before_le_integral (hf.sub_martingale (martingale_const _ _ _)).Pos
-        (fun ω => LatticeOrderedCommGroup.pos_nonneg _)
-        (fun ω => LatticeOrderedCommGroup.pos_nonneg _) (sub_pos.2 hab))
+        (fun ω => LatticeOrderedGroup.pos_nonneg _) (fun ω => LatticeOrderedGroup.pos_nonneg _)
+        (sub_pos.2 hab))
   simp_rw [sub_zero, ← upcrossings_before_pos_eq hab]
   rfl
 #align measure_theory.mul_integral_upcrossings_before_le_integral_pos_part_aux MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux
@@ -959,7 +959,7 @@ theorem Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part [IsFin
   · rw [not_lt, ← sub_nonpos] at hab 
     exact
       le_trans (mul_nonpos_of_nonpos_of_nonneg hab (integral_nonneg fun ω => Nat.cast_nonneg _))
-        (integral_nonneg fun ω => LatticeOrderedCommGroup.pos_nonneg _)
+        (integral_nonneg fun ω => LatticeOrderedGroup.pos_nonneg _)
 #align measure_theory.submartingale.mul_integral_upcrossings_before_le_integral_pos_part MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part
 -/
 
@@ -1110,7 +1110,7 @@ theorem Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part [IsFiniteM
       intro N
       rw [of_real_integral_eq_lintegral_of_real]
       · exact (hf.sub_martingale (martingale_const _ _ _)).Pos.Integrable _
-      · exact eventually_of_forall fun ω => LatticeOrderedCommGroup.pos_nonneg _
+      · exact eventually_of_forall fun ω => LatticeOrderedGroup.pos_nonneg _
     rw [lintegral_supr']
     · simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]
       intro N

Mathbin/Probability/StrongLaw.lean

@@ -637,7 +637,7 @@ theorem strong_law_aux2 {c : ℝ} (c_one : 1 < c) :
   apply Asymptotics.isLittleO_iff.2 fun ε εpos => _
   obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists
   filter_upwards [hω i] with n hn
-  simp only [Real.norm_eq_abs, LatticeOrderedCommGroup.abs_abs, Nat.abs_cast]
+  simp only [Real.norm_eq_abs, LatticeOrderedGroup.abs_abs, Nat.abs_cast]
   exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))
 #align probability_theory.strong_law_aux2 ProbabilityTheory.strong_law_aux2
 -/

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "0ebb88163badde5b820d016c0d0d54cc120dfcf3",
+    "rev": "99776ef2e96168a7c84fc705ee5f342b9165be7b",
     "name": "lean3port",
-    "inputRev?": "0ebb88163badde5b820d016c0d0d54cc120dfcf3"}},
+    "inputRev?": "99776ef2e96168a7c84fc705ee5f342b9165be7b"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "2d11c668314a5b2e55f34f7b65964118fcb1ff9f",
+    "rev": "f330b65348432a6e7dc2c49403394517886f8c32",
     "name": "mathlib",
-    "inputRev?": "2d11c668314a5b2e55f34f7b65964118fcb1ff9f"}},
+    "inputRev?": "f330b65348432a6e7dc2c49403394517886f8c32"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-08-10-07"
+def tag : String := "nightly-2023-08-10-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0ebb88163badde5b820d016c0d0d54cc120dfcf3"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"99776ef2e96168a7c84fc705ee5f342b9165be7b"
 
 @[default_target]
 lean_lib Mathbin where