bump toolchain and Mathlib to v4.21.0 (#602)

Co-authored-by: Paul Lezeau <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>

Author: 3 people

FormalConjectures/Arxiv/0911.2077/Conjecture6_3.lean

@@ -50,7 +50,7 @@ theorem arxiv.id0911_2077.conjecture6_3
       le_trans (le_of_lt (Set.mem_Ioo.mp h_p).right) (by linarith)
     1 - Φ ((1 / 2 - p) * sqrt (2 * k : ℝ≥0) / σ)
       + (1 / 2) * ((2 * k).choose k) * σ ^ (2 * k)
-      ≤ ((PMF.binomial (.ofReal p : ℝ≥0∞) hp' (2 * k)).toMeasure (Set.Ici k)).toReal := by
+      ≤ ((PMF.binomial (.ofReal p : ℝ≥0∞) hp' (2 * k)).toMeasure (Set.Ici ⟨k, by omega⟩)).toReal := by
   sorry
 
 end Arxiv.«0911.2077»

FormalConjectures/ErdosProblems/306.lean

@@ -32,8 +32,8 @@ each the product of two distinct primes, such that $\frac{a}{b}=\frac{1}{n_1}+\c
 @[category research open, AMS 11]
 theorem erdos_306 : (∀ (q : ℚ), 0 < q → Squarefree q.den →
     ∃ k : ℕ, ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ StrictMono n ∧
-    (∀ i ∈ Finset.Icc 1 k, ω (n i) = 2 ∧ Ω (n i) = 2) ∧
-    q = ∑ i ∈ Finset.Icc 1 k, (1 : ℚ) / (n i)) ↔ answer(sorry) := by
+    (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 2 ∧ Ω (n i) = 2) ∧
+    q = ∑ i ∈ Finset.Icc 1 (Fin.last k), (1 : ℚ) / (n i)) ↔ answer(sorry) := by
   sorry
 
 /--
@@ -42,7 +42,8 @@ product of three distinct primes.
 -/
 @[category research solved, AMS 11]
 theorem erdos_306.variant.integer_three_primes (m : ℕ) (h : 0 < m) :
-    ∃ k : ℕ, ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ ∀ i, i < k → n i < n (i + 1) ∧
-    (∀ i ∈ Finset.Icc 1 k, ω (n i) = 3 ∧ Ω (n i) = 3) ∧
-    m = ∑ i ∈ Finset.Icc 1 k, (1 : ℚ) / (n i) := by
+    ∃ k : ℕ, ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧
+    ∀ i, (hik : i < k) → n ⟨i, by omega⟩ < n ⟨(i + 1), by omega⟩ ∧
+    (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 3 ∧ Ω (n i) = 3) ∧
+    m = ∑ i ∈ Finset.Icc 1 (Fin.last k), (1 : ℚ) / (n i) := by
   sorry

FormalConjectures/ErdosProblems/392.lean

@@ -40,8 +40,8 @@ $$
 -/
 @[category research solved, AMS 11]
 theorem erdos_392 (A : ℕ → ℕ) (h : ∀ n > 0,
-    IsLeast { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧ Monotone a ∧ a t ≤ n ^ 2) }
-      (A n)) :
+    IsLeast { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧
+      Monotone a ∧ a (Fin.last t) ≤ n ^ 2) } (A n)) :
     ((fun (n : ℕ) => (A n - n / 2 + n / (2 * Real.log n) : ℝ)) =o[atTop] fun n => n / Real.log n)
   := by
   sorry
@@ -55,8 +55,8 @@ $$
 @[category research solved, AMS 11]
 theorem erdos_392.variants.lower (A : ℕ → ℕ)
     (hA : ∀ n > 0, IsLeast
-      { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧ Monotone a ∧ a t ≤ n) }
-      (A n)) :
+      { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧
+        Monotone a ∧ a (Fin.last t) ≤ n) } (A n)) :
     (fun (n : ℕ) => (A n - n + n / Real.log n : ℝ)) =o[atTop] fun n => n / Real.log n := by
   sorry
 

FormalConjectures/ErdosProblems/786.lean

@@ -73,8 +73,9 @@ theorem erdos_786.parts.i.example (A : Set ℕ) (hA : A = { n | n % 4 = 2 }) :
 consecutive primes.
 -/
 def consecutivePrimes {k : ℕ} (p : Fin k.succ → ℕ) :=
+    -- TODO(firsching): clarify quantifier scope here.
     ∀ i, (p i).Prime ∧ StrictMono p ∧
-      ∀ i < k, ∀ m ∈ Set.Ioo (p i) (p (i + 1)), ¬m.Prime
+    ∀ i : Fin k, ∀ m ∈ Set.Ioo (p i.castSucc) (p i.succ), ¬m.Prime
 
 -- Reworded slightly from the link.
 /--
@@ -95,8 +96,8 @@ theorem erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε ≤ 1) :
       ∀ᶠ (p : Fin (k + 2) → ℕ) in atTop, consecutivePrimes p ∧
         ∑ i ∈ Finset.univ.filter (· < Fin.last _), (1 : ℝ) / p i < 1 ∧
           1 < ∑ i, (1 : ℝ) / p i →
-    { n | ∃! i < k, p i ∣ n }.HasDensity (1 / Real.exp 1 - ε) ∧
-      { n | ∃! i < k, p i ∣ n }.IsMulCardSet := by
+    { n | ∃! (i : Fin (k + 2)), i < k → p i ∣ n }.HasDensity (1 / Real.exp 1 - ε) ∧
+      { n | ∃! (i : Fin (k + 2)), i < k → p i ∣ n }.IsMulCardSet := by
   sorry
 
 end Erdos786

FormalConjectures/ForMathlib/Analysis/SpecialFunctions/NthRoot.lean

@@ -26,11 +26,6 @@ The trap this avoids is that using `rpow`, `(-8 : ℝ) ^ (1/3 : ℝ) = 1`.
 This is being upstreamed to Mathlib in leanprover-community/mathlib4#26935.
 -/
 
-theorem SignType.pow_odd (s : SignType) (n : ℕ) (hn : Odd n) : s ^ n = s := by
-  obtain ⟨k, rfl⟩ := hn
-  rw [pow_add, pow_one, pow_mul, sq]
-  cases s <;> simp
-
 namespace Real
 
 noncomputable def nthRoot (n : ℕ) (r : ℝ) : ℝ :=

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -14,9 +14,8 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
-import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Bipartite
 import Mathlib.Combinatorics.SimpleGraph.Acyclic
-import Mathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Combinatorics.SimpleGraph.Bipartite
 import Mathlib.Combinatorics.SimpleGraph.Matching
 import Mathlib.Data.Real.Archimedean
 

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Definitions.lean

@@ -15,6 +15,7 @@ limitations under the License.
 -/
 
 import Mathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
 
 /-
 Dominating sets and domination numbers

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Domination.lean

@@ -25,13 +25,26 @@ namespace HartshorneConjecture
 
 open HartshorneConjecture
 
+universe u
+
 open CategoryTheory Limits MvPolynomial AlgebraicGeometry
 
-variable (S : Scheme)
+variable (S : Scheme.{u})
 
 namespace AlgebraicGeometry.Scheme
 
-attribute [local instance] CategoryTheory.Types.instConcreteCategory
+attribute [local instance] CategoryTheory.Types.instConcreteCategory Types.instFunLike
+
+-- TODO(lezeau): explain/investigate why the following two instances are needed.
+
+local instance (X : TopologicalSpace.Opens S) :
+    ((Opens.grothendieckTopology S).over X).WEqualsLocallyBijective (Type u) :=
+  CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHomObjForget
+    ((Opens.grothendieckTopology S).over X)
+
+local instance (X : TopologicalSpace.Opens S) :
+    ((Opens.grothendieckTopology S).over X).WEqualsLocallyBijective (AddCommGrp.{u}):=
+  inferInstance
 
 /--
 A vector bundle over a scheme `S` is a locally free `𝓞_S`-module of finite rank.

FormalConjectures/Paper/HartshorneConjecture.lean

@@ -26,7 +26,6 @@ import FormalConjectures.ForMathlib.Combinatorics.AP.Basic
 import FormalConjectures.ForMathlib.Combinatorics.Additive.Basis
 import FormalConjectures.ForMathlib.Combinatorics.Additive.Convolution
 import FormalConjectures.ForMathlib.Combinatorics.Basic
-import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Bipartite
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Coloring
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.DiamExtra
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions