bump to v4.20.1

Author: mo271

FormalConjectures/ErdosProblems/304.lean

@@ -44,7 +44,7 @@ lemma unitFractionExpressible_of_zero {a b : ℕ} (h : a = 0 ∨ b = 0) :
   rintro _ s rfl hs h
   rw [eq_comm, Finset.sum_eq_zero_iff_of_nonneg (fun i hi ↦ by positivity)] at h
   simp only [inv_eq_zero, Nat.cast_eq_zero] at h
-  rw [Finset.card_eq_zero, Finset.eq_empty_iff_forall_not_mem]
+  rw [Finset.card_eq_zero, Finset.eq_empty_iff_forall_notMem]
   intro i hi
   linarith [h i hi, hs i hi]
 
@@ -121,7 +121,7 @@ lemma dvd_of_smallestCollection_eq_one {a b : ℕ}
 lemma smallestCollection_two_fifteen : smallestCollection 2 15 = 2 := by
   have h : 2 ∈ unitFractionExpressible 2 15 := by
     use {10, 30}
-    norm_num [Finset.card_insert_of_not_mem, Finset.card_singleton]
+    norm_num [Finset.card_insert_of_notMem, Finset.card_singleton]
   have : smallestCollection 2 15 ≤ 2 := Nat.sInf_le h
   have : 0 < smallestCollection 2 15 := smallestCollection_pos (by simp) (by simp) ⟨_, h⟩
   have : smallestCollection 2 15 ≠ 1 := by

FormalConjectures/ForMathlib/Combinatorics/AP/Basic.lean

@@ -67,7 +67,7 @@ theorem Set.isAPOfLengthWith_pair {α : Type*} [DecidableEq α] [AddCommGroup α
     {a b : α} (hab : a ≠ b) :
     Set.IsAPOfLengthWith {a, b} 2 a (b - a) := by
   simp [IsAPOfLengthWith]
-  rw [Finset.card_insert_of_not_mem (by simpa only [Finset.mem_singleton])]
+  rw [Finset.card_insert_of_notMem (by simpa only [Finset.mem_singleton])]
   simp
   refine Set.ext fun x => ⟨fun h ↦ ?_, fun ⟨n, ⟨_, _⟩⟩ ↦ by interval_cases n <;> simp_all⟩
   cases h with

FormalConjectures/ForMathlib/Test/Computability/TuringMachine.lean

@@ -45,7 +45,7 @@ match l with
 instance : alwaysHaltingMachine.IsHalting where
   halts := by
     simp_rw (config := { singlePass := true })
-      [BusyBeaver.eval, Turing.eval, Part.map_Dom, step, alwaysHaltingMachine, Option.map_none',
+      [BusyBeaver.eval, Turing.eval, Part.map_Dom, step, alwaysHaltingMachine, Option.map_none,
       Part.dom_iff_mem, PFun.mem_fix_iff, Part.mem_some_iff]
     use default
     aesop

FormalConjectures/Paper/Kurepa.lean

@@ -89,7 +89,7 @@ theorem kurepa_conjecture.variant.gcd (n : ℕ) : 2 < n → (n !).gcd (! n) = 2
 theorem kurepa_conjecture.gcd_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0)
     ↔ (∀ n, 2 < n → (n)!.gcd (!n) = 2) := by
   refine ⟨fun h n hn ↦ match n with | S + 1 => gcd_eq_iff.2 ?_,
-    fun h n hn _ ↦ n.not_dvd_of_pos_of_lt (by omega) hn <| h n hn ▸ n.dvd_gcd
+    fun h n hn _ ↦ Nat.not_dvd_of_pos_of_lt (by omega) hn <| h n hn ▸ n.dvd_gcd
       (n.dvd_factorial hn.pos le_rfl) (dvd_of_mod_eq_zero ‹_›)⟩
   refine ⟨Nat.factorial_dvd_factorial hn.le, ?_, fun c hc h_dvd ↦ ?_⟩
   · match S with

FormalConjectures/Wikipedia/Conway99Graph.lean

@@ -25,7 +25,12 @@ import FormalConjectures.Util.ProblemImports
 Conway's 99-graph problem
 -/
 --TODO(firsching): Consider using SimpleGraph.IsSRGWith to formulate the conjecture.
+
+open SimpleGraph
+
 variable {V : Type} {G : SimpleGraph V}
+
+
 @[category undergraduate, AMS 5]
 lemma completeGraphIsClique (s : Finset V) : (⊤ : SimpleGraph V).IsClique s :=
   Pairwise.set_pairwise (fun _ _ a ↦ a) _
@@ -104,7 +109,7 @@ example : NonEdgesAreDiagonals Conway9 := by
   have ⟨x1, x2⟩ := x
   have ⟨y1, y2⟩ := y
   simp only [Conway9, SimpleGraph.completeGraph_eq_top,
-    SimpleGraph.boxProd_adj, SimpleGraph.top_adj, SimpleGraph.boxProd_neighborFinset]
+    SimpleGraph.boxProd_adj, SimpleGraph.top_adj, SimpleGraph.neighborFinset_boxProd]
   fin_cases x1 <;> fin_cases x2 <;> fin_cases y1 <;> fin_cases y2 <;> decide
 
 @[category API, AMS 5]

FormalConjectures/Wikipedia/PebblingNumberConjecture.lean

@@ -93,7 +93,7 @@ The pebbling number of the complete graph on `n` vertices is `n`.
 -/
 @[category API, AMS 5]
 theorem PebblingNumber_completeGraph [Fintype V] :
-    PebblingNumber (completeGraph V) = Fintype.card V := by
+    PebblingNumber (SimpleGraph.completeGraph V) = Fintype.card V := by
   refine IsLeast.csInf_eq ⟨fun D hD v => ?_, fun a ha => not_lt.1 fun ha_lt => ?_⟩
   · by_cases h : ∃ w, 2 ≤ D w
     · obtain ⟨w, hw⟩ := h

FormalConjectures/Wikipedia/RegularPrimes.lean

@@ -32,15 +32,10 @@ noncomputable section
 
 variable (p : ℕ)
 
-/-- TODO: remove this once mathlib is updated as it seems that in this version of mathlib
-we need to do this manually. -/
-instance [hp : Fact p.Prime]  : NumberField (CyclotomicField ⟨p, hp.out.pos⟩ ℚ) :=
-  IsCyclotomicExtension.numberField {⟨p, hp.out.pos⟩} ℚ _
-
 /-- A natural prime number `p` is regular if `p` is coprime with the order of the class group
 of the `p`-th cyclotomic field. -/
 def IsRegularPrime [hp : Fact p.Prime] : Prop :=
-  p.Coprime <| Fintype.card <| ClassGroup (𝓞 <| CyclotomicField ⟨p, hp.out.pos⟩ ℚ)
+  p.Coprime <| Fintype.card <| ClassGroup (𝓞 <| CyclotomicField p  ℚ)
 
 @[category undergraduate, AMS 11]
 example : ¬ @IsRegularPrime 37 (by decide) := by

FormalConjectures/Wikipedia/UnionClosed.lean

@@ -155,7 +155,7 @@ theorem union_closed.variants.sharpness [Fintype n] (c : ℝ) (hc : 1 / 2 < c) :
   obtain hn | hn := isEmpty_or_nonempty n
   · specialize h ∅
     simp only [ne_eq, card_empty, CharP.cast_eq_zero, mul_zero, filter_empty, le_refl,
-      IsEmpty.exists_iff, imp_false, not_forall, not_mem_empty, imp_self, implies_true,
+      IsEmpty.exists_iff, imp_false, not_forall, notMem_empty, imp_self, implies_true,
       not_true_eq_false, exists_const, Decidable.not_not] at h
     have : ∅ ∈ (∅ : Finset (Finset n)) := by simp [h]
     simp at this

docbuild/lakefile.toml

@@ -7,11 +7,11 @@ packagesDir = "../.lake/packages"
 name = "formal_conjectures"
 path = "../"
 
-# using fork here, because it contains a backported fix. Can be dropped after bump to v4.20.0
 [[require]]
 name = "doc-gen4"
-git = "https://github.com/mo271/doc-gen4"
-rev = "b760b91540bcf92c2ab6ac2bc28207e090769da8"
+scope = "leanprover"
+name = "doc-gen4"
+rev = "v4.20.1"
 
 [[lean_exe]]
 name = "overwrite_index"

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c44e0c8ee63ca166450922a373c7409c5d26b00b",
+   "rev": "5c0c94b3f563ed756b48b9439788c53b0d56a897",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.19.0",
+   "inputRev": "v4.20.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "77e08eddc486491d7b9e470926b3dbe50319451a",
+   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e6a9f0f5ee3ccf7443a0070f92b62f8db12ae82b",
+   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c4919189477c3221e6a204008998b0d724f49904",
+   "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.57",
+   "inputRev": "v0.0.60",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5d50b08dedd7d69b3d9b3176e0d58a23af228884",
+   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa4f7f15d97591a9cf3aa7724ba371c7fc6dda02",
+   "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f5d04a9c4973d401c8c92500711518f7c656f034",
+   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "02dbd02bc00ec4916e99b04b2245b30200e200d0",
+   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",