bump to nightly-2023-06-26-13

mathlib commit leanprover-community/mathlib@fdc286c

Mathbin/Algebra/BigOperators/Intervals.lean

@@ -252,7 +252,7 @@ theorem prod_range_add_one_eq_factorial : ∀ n : ℕ, ∏ x in range n, (x + 1)
 #align finset.prod_range_add_one_eq_factorial Finset.prod_range_add_one_eq_factorial
 -/
 
-section GaussSum
+section gaussSum
 
 #print Finset.sum_range_id_mul_two /-
 /-- Gauss' summation formula -/
@@ -274,7 +274,7 @@ theorem sum_range_id (n : ℕ) : ∑ i in range n, i = n * (n - 1) / 2 := by
 #align finset.sum_range_id Finset.sum_range_id
 -/
 
-end GaussSum
+end gaussSum
 
 end Generic
 

Mathbin/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -37,7 +37,7 @@ open Finset Fintype Function Real
 
 open scoped BigOperators
 
-namespace SzemerediRegularity
+namespace szemeredi_regularity
 
 #print SzemerediRegularity.stepBound /-
 /-- Auxiliary function for Szemerédi's regularity lemma. Blowing up a partition of size `n` during
@@ -67,9 +67,9 @@ theorem stepBound_pos_iff {n : ℕ} : 0 < stepBound n ↔ 0 < n :=
 alias step_bound_pos_iff ↔ _ step_bound_pos
 #align szemeredi_regularity.step_bound_pos SzemerediRegularity.stepBound_pos
 
-end SzemerediRegularity
+end szemeredi_regularity
 
-open SzemerediRegularity
+open szemeredi_regularity
 
 variable {α : Type _} [DecidableEq α] [Fintype α] {P : Finpartition (univ : Finset α)}
   {u : Finset α} {ε : ℝ}
@@ -131,7 +131,7 @@ end Tactic
 
 attribute [local positivity] tactic.positivity_szemeredi_regularity
 
-namespace SzemerediRegularity
+namespace szemeredi_regularity
 
 #print SzemerediRegularity.m_pos /-
 theorem m_pos [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) : 0 < m := by
@@ -331,11 +331,11 @@ theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜)
 #align szemeredi_regularity.add_div_le_sum_sq_div_card SzemerediRegularity.add_div_le_sum_sq_div_card
 -/
 
-end SzemerediRegularity
+end szemeredi_regularity
 
 namespace Tactic
 
-open Positivity SzemerediRegularity
+open Positivity szemeredi_regularity
 
 /-- Extension for the `positivity` tactic: `szemeredi_regularity.initial_bound` and
 `szemeredi_regularity.bound` are always positive. -/

Mathbin/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -46,7 +46,7 @@ open scoped BigOperators Classical
 
 attribute [local positivity] tactic.positivity_szemeredi_regularity
 
-namespace SzemerediRegularity
+namespace szemeredi_regularity
 
 variable {α : Type _} [Fintype α] {P : Finpartition (univ : Finset α)} (hP : P.IsEquipartition)
   (G : SimpleGraph α) (ε : ℝ) {U : Finset α} (hU : U ∈ P.parts) (V : Finset α)
@@ -617,5 +617,5 @@ theorem edgeDensity_chunk_uniform [Nonempty α] (hPα : P.parts.card * 16 ^ P.pa
 #align szemeredi_regularity.edge_density_chunk_uniform SzemerediRegularity.edgeDensity_chunk_uniform
 -/
 
-end SzemerediRegularity
+end szemeredi_regularity
 

Mathbin/Combinatorics/SimpleGraph/Regularity/Increment.lean

@@ -39,7 +39,7 @@ Once ported to mathlib4, this file will be a great golfing ground for Heather's
 -/
 
 
-open Finset Fintype SimpleGraph SzemerediRegularity
+open Finset Fintype SimpleGraph szemeredi_regularity
 
 open scoped BigOperators Classical
 
@@ -50,8 +50,9 @@ variable {α : Type _} [Fintype α] {P : Finpartition (univ : Finset α)} (hP :
 
 local notation "m" => (card α / stepBound P.parts.card : ℕ)
 
-namespace SzemerediRegularity
+namespace szemeredi_regularity
 
+#print SzemerediRegularity.increment /-
 /-- The **increment partition** in Szemerédi's Regularity Lemma.
 
 If an equipartition is *not* uniform, then the increment partition is a (much bigger) equipartition
@@ -61,11 +62,13 @@ not-too-big uniform equipartition. -/
 noncomputable def increment : Finpartition (univ : Finset α) :=
   P.bind fun U => chunk hP G ε
 #align szemeredi_regularity.increment SzemerediRegularity.increment
+-/
 
 open Finpartition Finpartition.IsEquipartition
 
 variable {hP G ε}
 
+#print SzemerediRegularity.card_increment /-
 /-- The increment partition has a prescribed (very big) size in terms of the original partition. -/
 theorem card_increment (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) (hPG : ¬P.IsUniform G ε) :
     (increment hP G ε).parts.card = stepBound P.parts.card :=
@@ -82,7 +85,9 @@ theorem card_increment (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) (hP
   congr
   rw [filter_card_add_filter_neg_card_eq_card, card_attach]
 #align szemeredi_regularity.card_increment SzemerediRegularity.card_increment
+-/
 
+#print SzemerediRegularity.increment_isEquipartition /-
 theorem increment_isEquipartition (hP : P.IsEquipartition) (G : SimpleGraph α) (ε : ℝ) :
     (increment hP G ε).IsEquipartition :=
   by
@@ -92,6 +97,7 @@ theorem increment_isEquipartition (hP : P.IsEquipartition) (G : SimpleGraph α)
   obtain ⟨U, hU, hA⟩ := hA
   exact card_eq_of_mem_parts_chunk hA
 #align szemeredi_regularity.increment_is_equipartition SzemerediRegularity.increment_isEquipartition
+-/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 private theorem distinct_pairs_increment :
@@ -119,6 +125,7 @@ private noncomputable def pair_contrib (G : SimpleGraph α) (ε : ℝ) (hP : P.I
   ∑ i in (chunk hP G ε (mem_offDiag.1 x.2).1).parts ×ˢ (chunk hP G ε (mem_offDiag.1 x.2).2.1).parts,
     G.edgeDensity i.fst i.snd ^ 2
 
+#print SzemerediRegularity.offDiag_pairs_le_increment_energy /-
 theorem offDiag_pairs_le_increment_energy :
     ∑ x in P.parts.offDiag.attach, pairContrib G ε hP x / (increment hP G ε).parts.card ^ 2 ≤
       (increment hP G ε).energy G :=
@@ -142,7 +149,9 @@ theorem offDiag_pairs_le_increment_energy :
           P.disjoint.elim_finset hs.2.1 ht.2.1 b (Finpartition.le _ huv₁.2 hb) <|
             Finpartition.le _ huv₂.2 hb)
 #align szemeredi_regularity.off_diag_pairs_le_increment_energy SzemerediRegularity.offDiag_pairs_le_increment_energy
+-/
 
+#print SzemerediRegularity.pairContrib_lower_bound /-
 theorem pairContrib_lower_bound [Nonempty α] (x : { i // i ∈ P.parts.offDiag }) (hε₁ : ε ≤ 1)
     (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) (hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5) :
     (↑(G.edgeDensity x.1.1 x.1.2) ^ 2 - ε ^ 5 / 25 +
@@ -156,7 +165,9 @@ theorem pairContrib_lower_bound [Nonempty α] (x : { i // i ∈ P.parts.offDiag
     exact edge_density_chunk_uniform hPα hPε _ _
   · exact edge_density_chunk_not_uniform hPα hPε hε₁ (mem_off_diag.1 x.2).2.2 h
 #align szemeredi_regularity.pair_contrib_lower_bound SzemerediRegularity.pairContrib_lower_bound
+-/
 
+#print SzemerediRegularity.uniform_add_nonuniform_eq_offDiag_pairs /-
 theorem uniform_add_nonuniform_eq_offDiag_pairs [Nonempty α] (hε₁ : ε ≤ 1) (hP₇ : 7 ≤ P.parts.card)
     (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) (hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5)
     (hPG : ¬P.IsUniform G ε) :
@@ -211,7 +222,9 @@ theorem uniform_add_nonuniform_eq_offDiag_pairs [Nonempty α] (hε₁ : ε ≤ 1
     div_le_iff (show (0 : ℝ) < 1 / 3 - 1 / 25 - 1 / 4 by norm_num)]
   exact le_trans (show _ ≤ (7 : ℝ) by norm_num) (by exact_mod_cast hP₇)
 #align szemeredi_regularity.uniform_add_nonuniform_eq_off_diag_pairs SzemerediRegularity.uniform_add_nonuniform_eq_offDiag_pairs
+-/
 
+#print SzemerediRegularity.energy_increment /-
 /-- The increment partition has energy greater than the original one by a known fixed amount. -/
 theorem energy_increment [Nonempty α] (hP : P.IsEquipartition) (hP₇ : 7 ≤ P.parts.card)
     (hε : 100 < 4 ^ P.parts.card * ε ^ 5) (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α)
@@ -224,6 +237,7 @@ theorem energy_increment [Nonempty α] (hP : P.IsEquipartition) (hP₇ : 7 ≤ P
   exact h.trans (by exact_mod_cast off_diag_pairs_le_increment_energy)
   positivity
 #align szemeredi_regularity.energy_increment SzemerediRegularity.energy_increment
+-/
 
-end SzemerediRegularity
+end szemeredi_regularity
 

Mathbin/Combinatorics/SimpleGraph/Regularity/Lemma.lean

@@ -73,6 +73,7 @@ open scoped Classical
 
 variable {α : Type _} [Fintype α] (G : SimpleGraph α) {ε : ℝ} {l : ℕ}
 
+#print szemeredi_regularity /-
 /-- Effective **Szemerédi Regularity Lemma**: For any sufficiently large graph, there is an
 `ε`-uniform equipartition of bounded size (where the bound does not depend on the graph). -/
 theorem szemeredi_regularity (hε : 0 < ε) (hl : l ≤ card α) :
@@ -166,4 +167,5 @@ theorem szemeredi_regularity (hε : 0 < ε) (hl : l ≤ card α) :
   · rw [Nat.cast_succ, mul_add, mul_one]
     exact add_le_add_right hP₄ _
 #align szemeredi_regularity szemeredi_regularity
+-/
 

Mathbin/NumberTheory/LegendreSymbol/GaussSum.lean

@@ -70,11 +70,14 @@ variable {R' : Type v} [CommRing R']
 -/
 
 
+#print gaussSum /-
 /-- Definition of the Gauss sum associated to a multiplicative and an additive character. -/
 def gaussSum (χ : MulChar R R') (ψ : AddChar R R') : R' :=
   ∑ a, χ a * ψ a
 #align gauss_sum gaussSum
+-/
 
+#print gaussSum_mulShift /-
 /-- Replacing `ψ` by `mul_shift ψ a` and multiplying the Gauss sum by `χ a` does not change it. -/
 theorem gaussSum_mulShift (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
     χ a * gaussSum χ (mulShift ψ a) = gaussSum χ ψ :=
@@ -83,6 +86,7 @@ theorem gaussSum_mulShift (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
   simp_rw [← mul_assoc, ← map_mul]
   exact Fintype.sum_bijective _ a.mul_left_bijective _ _ fun x => rfl
 #align gauss_sum_mul_shift gaussSum_mulShift
+-/
 
 end GaussSumDef
 
@@ -110,6 +114,7 @@ private theorem gauss_sum_mul_aux {χ : MulChar R R'} (hχ : IsNontrivial χ) (
     refine' (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x => _).symm
     rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel hb, one_mul, mul_sub, mul_one]
 
+#print gaussSum_mul_gaussSum_eq_card /-
 /-- We have `gauss_sum χ ψ * gauss_sum χ⁻¹ ψ⁻¹ = fintype.card R`
 when `χ` is nontrivial and `ψ` is primitive (and `R` is a field). -/
 theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : IsNontrivial χ) {ψ : AddChar R R'}
@@ -125,7 +130,9 @@ theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : IsNontrivial χ
   rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
   simp only [Finset.mem_univ, map_one, one_mul, if_true]
 #align gauss_sum_mul_gauss_sum_eq_card gaussSum_mul_gaussSum_eq_card
+-/
 
+#print gaussSum_sq /-
 /-- When `χ` is a nontrivial quadratic character, then the square of `gauss_sum χ ψ`
 is `χ(-1)` times the cardinality of `R`. -/
 theorem gaussSum_sq {χ : MulChar R R'} (hχ₁ : IsNontrivial χ) (hχ₂ : IsQuadratic χ)
@@ -136,6 +143,7 @@ theorem gaussSum_sq {χ : MulChar R R'} (hχ₁ : IsNontrivial χ) (hχ₂ : IsQ
   rw [mul_comm, ← gaussSum_mulShift _ _ (-1 : Rˣ), inv_mul_shift]
   rfl
 #align gauss_sum_sq gaussSum_sq
+-/
 
 end GaussSumProd
 
@@ -151,6 +159,7 @@ variable {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R']
 -- We assume that the target ring `R'` has prime characteristic `p`.
 variable (p : ℕ) [fp : Fact p.Prime] [hch : CharP R' p]
 
+#print gaussSum_frob /-
 /-- When `R'` has prime characteristic `p`, then the `p`th power of the Gauss sum
 of `χ` and `ψ` is the Gauss sum of `χ^p` and `ψ^p`. -/
 theorem gaussSum_frob (χ : MulChar R R') (ψ : AddChar R R') :
@@ -160,7 +169,9 @@ theorem gaussSum_frob (χ : MulChar R R') (ψ : AddChar R R') :
   simp_rw [pow_apply' χ fp.1.Pos, map_mul, frobenius_def]
   rfl
 #align gauss_sum_frob gaussSum_frob
+-/
 
+#print MulChar.IsQuadratic.gaussSum_frob /-
 /-- For a quadratic character `χ` and when the characteristic `p` of the target ring
 is a unit in the source ring, the `p`th power of the Gauss sum of`χ` and `ψ` is
 `χ p` times the original Gauss sum. -/
@@ -170,7 +181,9 @@ theorem MulChar.IsQuadratic.gaussSum_frob (hp : IsUnit (p : R)) {χ : MulChar R
     hp.unit_spec, ← pow_two, ← pow_apply' _ (by norm_num : 0 < 2), hχ.sq_eq_one, ← hp.unit_spec,
     one_apply_coe, one_mul]
 #align mul_char.is_quadratic.gauss_sum_frob MulChar.IsQuadratic.gaussSum_frob
+-/
 
+#print MulChar.IsQuadratic.gaussSum_frob_iter /-
 /-- For a quadratic character `χ` and when the characteristic `p` of the target ring
 is a unit in the source ring and `n` is a natural number, the `p^n`th power of the Gauss
 sum of`χ` and `ψ` is `χ (p^n)` times the original Gauss sum. -/
@@ -183,6 +196,7 @@ theorem MulChar.IsQuadratic.gaussSum_frob_iter (n : ℕ) (hp : IsUnit (p : R)) {
     rw [pow_succ, mul_comm p, pow_mul, ih, mul_pow, hχ.gauss_sum_frob _ hp, ← mul_assoc, pow_succ,
       mul_comm (p : R), map_mul, ← pow_apply' χ fp.1.Pos (p ^ n), hχ.pow_char p]
 #align mul_char.is_quadratic.gauss_sum_frob_iter MulChar.IsQuadratic.gaussSum_frob_iter
+-/
 
 end gaussSum_frob
 
@@ -195,6 +209,7 @@ section GaussSumValues
 
 variable {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R']
 
+#print Char.card_pow_char_pow /-
 /-- If the square of the Gauss sum of a quadratic character is `χ(-1) * #R`,
 then we get, for all `n : ℕ`, the relation `(χ(-1) * #R) ^ (p^n/2) = χ(p^n)`,
 where `p` is the (odd) characteristic of the target ring `R'`.
@@ -213,7 +228,9 @@ theorem Char.card_pow_char_pow {χ : MulChar R R'} (hχ : IsQuadratic χ) (ψ :
   rw [← hχ.gauss_sum_frob_iter p n hp ψ, ← pow_mul, mul_comm, ← pow_succ,
     Nat.two_mul_div_two_add_one_of_odd (fp.1.eq_two_or_odd'.resolve_left hp').pow]
 #align char.card_pow_char_pow Char.card_pow_char_pow
+-/
 
+#print Char.card_pow_card /-
 /-- When `F` and `F'` are finite fields and `χ : F → F'` is a nontrivial quadratic character,
 then `(χ(-1) * #F)^(#F'/2) = χ(#F')`. -/
 theorem Char.card_pow_card {F : Type _} [Field F] [Fintype F] {F' : Type _} [Field F'] [Fintype F']
@@ -236,6 +253,7 @@ theorem Char.card_pow_card {F : Type _} [Field F] [Fintype F] {F' : Type _} [Fie
     Char.card_pow_char_pow (hχ₂.comp _) ψ.char (ringChar FF') n' hch₁ (hchar ▸ hch₂)
       (gaussSum_sq (hχ₁.comp <| RingHom.injective _) (hχ₂.comp _) ψ.prim)
 #align char.card_pow_card Char.card_pow_card
+-/
 
 end GaussSumValues
 
@@ -257,6 +275,7 @@ in this way, the result is reduced to `card_pow_char_pow`.
 
 open ZMod
 
+#print FiniteField.two_pow_card /-
 /-- For every finite field `F` of odd characteristic, we have `2^(#F/2) = χ₈(#F)` in `F`. -/
 theorem FiniteField.two_pow_card {F : Type _} [Fintype F] [Field F] (hF : ringChar F ≠ 2) :
     (2 : F) ^ (Fintype.card F / 2) = χ₈ (Fintype.card F) :=
@@ -331,6 +350,7 @@ theorem FiniteField.two_pow_card {F : Type _} [Fintype F] [Field F] (hF : ringCh
   simp only [map_pow, map_bit0, map_one, map_intCast]
   convert h; norm_num
 #align finite_field.two_pow_card FiniteField.two_pow_card
+-/
 
 end GaussSumTwo
 

Mathbin/NumberTheory/LegendreSymbol/MulCharacter.lean

@@ -101,18 +101,14 @@ variable {R : Type u} [CommMonoid R]
 -- The target
 variable {R' : Type v} [CommMonoidWithZero R']
 
-#print MulChar.coeToFun /-
 instance coeToFun : CoeFun (MulChar R R') fun _ => R → R' :=
   ⟨fun χ => χ.toFun⟩
 #align mul_char.coe_to_fun MulChar.coeToFun
--/
 
-#print MulChar.Simps.apply /-
 /-- See note [custom simps projection] -/
 protected def Simps.apply (χ : MulChar R R') : R → R' :=
   χ
 #align mul_char.simps.apply MulChar.Simps.apply
--/
 
 initialize_simps_projections MulChar (to_monoid_hom_to_fun → apply, -toMonoidHom)
 
@@ -139,19 +135,15 @@ noncomputable def trivial : MulChar R R'
 
 end trivial
 
-#print MulChar.coe_coe /-
 @[simp]
 theorem coe_coe (χ : MulChar R R') : (χ.toMonoidHom : R → R') = χ :=
   rfl
 #align mul_char.coe_coe MulChar.coe_coe
--/
 
-#print MulChar.toFun_eq_coe /-
 @[simp]
 theorem toFun_eq_coe (χ : MulChar R R') : χ.toFun = χ :=
   rfl
 #align mul_char.to_fun_eq_coe MulChar.toFun_eq_coe
--/
 
 #print MulChar.coe_mk /-
 @[simp]

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "22d5505a8913bdb291ee4e0895d2f430a03f53e3",
+    "rev": "3b322644acf968b954d1d2be2e632ea5ff600260",
     "name": "lean3port",
-    "inputRev?": "22d5505a8913bdb291ee4e0895d2f430a03f53e3"}},
+    "inputRev?": "3b322644acf968b954d1d2be2e632ea5ff600260"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "d8a7e7efffd126a7eaa13610cc0d07a93b905a51",
+    "rev": "5775c8521eb0918aff275c9e598ad2c2f187f5de",
     "name": "mathlib",
-    "inputRev?": "d8a7e7efffd126a7eaa13610cc0d07a93b905a51"}},
+    "inputRev?": "5775c8521eb0918aff275c9e598ad2c2f187f5de"}},
   {"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-06-26-11"
+def tag : String := "nightly-2023-06-26-13"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"22d5505a8913bdb291ee4e0895d2f430a03f53e3"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3b322644acf968b954d1d2be2e632ea5ff600260"
 
 @[default_target]
 lean_lib Mathbin where