Merge pull request #16716 from leanprover-community/bump/nightly-2024…

…-09-11

chore: adaptations for nightly-2024-09-11

Mathlib/Algebra/CharZero/Defs.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Algebra.NeZero
 import Mathlib.Logic.Function.Basic
 
 /-!

Mathlib/Algebra/Field/Defs.lean

@@ -45,8 +45,8 @@ field, division ring, skew field, skew-field, skewfield
 
 assert_not_imported Mathlib.Tactic.Common
 
--- `NeZero` should not be needed in the basic algebraic hierarchy.
-assert_not_exists NeZero
+-- `NeZero` theory should not be needed in the basic algebraic hierarchy
+assert_not_imported Mathlib.Algebra.NeZero
 
 assert_not_exists MonoidHom
 

Mathlib/Algebra/Group/Hom/Basic.lean

@@ -14,7 +14,7 @@ import Mathlib.Algebra.Group.Hom.Defs
 
 -- `NeZero` cannot be additivised, hence its theory should be developed outside of the
 -- `Algebra.Group` folder.
-assert_not_exists NeZero
+assert_not_imported Mathlib.Algebra.NeZero
 
 variable {α β M N P : Type*}
 

Mathlib/Algebra/Group/ZeroOne.lean

@@ -6,17 +6,10 @@ Authors: Gabriel Ebner, Mario Carneiro
 import Mathlib.Tactic.ToAdditive
 
 /-!
-## Classes for `Zero` and `One`
--/
-
-class Zero.{u} (α : Type u) where
-  zero : α
+## Typeclass `One`
 
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
-instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
+`Zero` has already been defined in Lean.
+-/
 
 universe u
 

Mathlib/Algebra/NeZero.lean

@@ -10,32 +10,12 @@ import Mathlib.Order.Defs
 /-!
 # `NeZero` typeclass
 
-We create a typeclass `NeZero n` which carries around the fact that `(n : R) ≠ 0`.
+We give basic facts about the `NeZero n` typeclass.
 
-## Main declarations
-
-* `NeZero`: `n ≠ 0` as a typeclass.
 -/
 
 variable {R : Type*} [Zero R]
 
-/-- A type-class version of `n ≠ 0`. -/
-class NeZero (n : R) : Prop where
-  /-- The proposition that `n` is not zero. -/
-  out : n ≠ 0
-
-theorem NeZero.ne (n : R) [h : NeZero n] : n ≠ 0 :=
-  h.out
-
-theorem NeZero.ne' (n : R) [h : NeZero n] : 0 ≠ n :=
-  h.out.symm
-
-theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
-  ⟨fun h ↦ h.out, NeZero.mk⟩
-
-@[simp] lemma neZero_zero_iff_false {α : Type*} [Zero α] : NeZero (0 : α) ↔ False :=
-  ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩
-
 theorem not_neZero {n : R} : ¬NeZero n ↔ n = 0 := by simp [neZero_iff]
 
 theorem eq_zero_or_neZero (a : R) : a = 0 ∨ NeZero a :=
@@ -77,10 +57,6 @@ namespace NeZero
 
 variable {M : Type*} {x : M}
 
-instance succ {n : ℕ} : NeZero (n + 1) := ⟨n.succ_ne_zero⟩
-
 theorem of_pos [Preorder M] [Zero M] (h : 0 < x) : NeZero x := ⟨ne_of_gt h⟩
 
 end NeZero
-
-lemma Nat.pos_of_neZero (n : ℕ) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)

Mathlib/Algebra/Order/Floor.lean

@@ -1025,7 +1025,7 @@ theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
     obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
     · rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
     · rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
-      simp [hl, zero_mod]
+      simp [hl]
   obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
   · exact this (ofNat_nonneg m₀)
   let q := ⌈↑m₀ / (n : k)⌉

Mathlib/Algebra/Order/Group/Defs.lean

@@ -21,9 +21,9 @@ The reason is that we did not want to change existing names in the library.
 -/
 
 /-
-`NeZero` should not be needed at this point in the ordered algebraic hierarchy.
+`NeZero` theory should not be needed at this point in the ordered algebraic hierarchy.
 -/
-assert_not_exists NeZero
+assert_not_imported Mathlib.Algebra.NeZero
 
 open Function
 

Mathlib/Algebra/Order/ZeroLEOne.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import Mathlib.Order.Basic
-import Mathlib.Algebra.NeZero
 
 /-!
 # Typeclass expressing `0 ≤ 1`.

Mathlib/Computability/PartrecCode.lean

@@ -624,8 +624,8 @@ theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c
     iterate 4 exact h
     · -- pair cf cg
       simp? [Seq.seq, Option.bind_eq_some] at h ⊢ says
-        simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some,
-          Option.map_eq_some', exists_exists_and_eq_and] at h ⊢
+        simp only [Seq.seq, Option.map_eq_map, Option.bind_map, Function.comp_apply,
+          Option.mem_def, Option.bind_eq_some, Option.map_eq_some'] at h ⊢
       exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)
     · -- comp cf cg
       simp? [Bind.bind, Option.bind_eq_some] at h ⊢ says
@@ -900,7 +900,7 @@ private theorem hG : Primrec G := by
       Primrec.fst
 
 private theorem evaln_map (k c n) :
-    ((((List.range k)[n]?).map (evaln k c)).bind fun b => b) = evaln k c n := by
+    ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n := by
   by_cases kn : n < k
   · simp [List.getElem?_range kn]
   · rw [List.getElem?_len_le]

Mathlib/Data/Fin/Basic.lean

@@ -1516,16 +1516,6 @@ protected theorem zero_mul' [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by
 
 end Mul
 
-open Qq in
-instance toExpr (n : ℕ) : Lean.ToExpr (Fin n) where
-  toTypeExpr := q(Fin $n)
-  toExpr := match n with
-    | 0 => finZeroElim
-    | k + 1 => fun i => show Q(Fin $n) from
-      have i : Q(Nat) := Lean.mkRawNatLit i -- raw literal to avoid ofNat-double-wrapping
-      have : Q(NeZero $n) := haveI : $n =Q $k + 1 := ⟨⟩; by exact q(NeZero.succ)
-      q(OfNat.ofNat $i)
-
 end Fin
 
 set_option linter.style.longFile 1700

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -778,7 +778,7 @@ theorem insertNth_apply_succAbove (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i
     generalize hk : castPred ((succAbove i) j) H₁ = k
     rw [castPred_succAbove _ _ hlt] at hk; cases hk
     intro; rfl
-  · generalize_proofs H₁ H₂; revert H₂
+  · generalize_proofs H₀ H₁ H₂; revert H₂
     generalize hk : pred (succAbove i j) H₁ = k
     erw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk; cases hk
     intro; rfl

Mathlib/Data/Nat/Bitwise.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.Ring.Nat
 import Mathlib.Order.Basic
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Common
+import Mathlib.Algebra.NeZero
 
 /-!
 # Bitwise operations on natural numbers

Mathlib/Data/Nat/Cast/NeZero.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Mathlib.Data.Nat.Cast.Defs
-import Mathlib.Algebra.NeZero
 
 /-!
 # Lemmas about nonzero elements of an `AddMonoidWithOne`

Mathlib/Data/Option/Basic.lean

@@ -137,10 +137,6 @@ variable {p : α → Prop} (f : ∀ a : α, p a → β) (x : Option α)
 theorem pbind_eq_bind (f : α → Option β) (x : Option α) : (x.pbind fun a _ ↦ f a) = x.bind f := by
   cases x <;> simp only [pbind, none_bind', some_bind']
 
-theorem map_bind {α β γ} (f : β → γ) (x : Option α) (g : α → Option β) :
-    Option.map f (x >>= g) = x >>= fun a ↦ Option.map f (g a) := by
-  simp only [← map_eq_map, ← bind_pure_comp, LawfulMonad.bind_assoc]
-
 theorem map_bind' (f : β → γ) (x : Option α) (g : α → Option β) :
     Option.map f (x.bind g) = x.bind fun a ↦ Option.map f (g a) := by cases x <;> simp
 

Mathlib/Data/PNat/Defs.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Neil Strickland
 -/
-import Mathlib.Algebra.NeZero
 import Mathlib.Data.Nat.Defs
 import Mathlib.Order.Basic
 import Mathlib.Order.TypeTags

Mathlib/Data/Rat/Lemmas.lean

@@ -53,7 +53,7 @@ theorem num_mk (n d : ℤ) : (n /. d).num = d.sign * n / n.gcd d := by
   have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
     rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]
   rcases d with ((_ | _) | _) <;>
-  rw [← Int.div_eq_ediv_of_dvd] <;>
+  rw [← Int.tdiv_eq_ediv_of_dvd] <;>
   simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd,
     Int.zero_ediv, Int.ofNat_dvd_left, Nat.gcd_dvd_left, this]
 
@@ -195,7 +195,7 @@ theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprim
 theorem intCast_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n := by
   by_cases hn : n = 0
   · subst hn
-    simp only [Int.cast_zero, Int.zero_div, zero_div, Int.ediv_zero]
+    simp only [Int.cast_zero, Int.zero_tdiv, zero_div, Int.ediv_zero]
   · have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
     simp only [Int.ediv_self hn, Int.cast_one, Ne, not_false_iff, div_self this]
 

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -179,7 +179,7 @@ theorem normalize : PythagoreanTriple (x / Int.gcd x y) (y / Int.gcd x y) (z / I
     have hz : z = 0 := by
       simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
         or_self_iff] using h
-    simp only [hx, hy, hz, Int.zero_div]
+    simp only [hx, hy, hz]
     exact zero
   rcases h.gcd_dvd with ⟨z0, rfl⟩
   obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ :

Mathlib/Tactic/NormNum/DivMod.lean

@@ -147,8 +147,8 @@ theorem isInt_dvd_true : {a b : ℤ} → {a' b' c : ℤ} →
   | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨_, rfl⟩
 
 theorem isInt_dvd_false : {a b : ℤ} → {a' b' : ℤ} →
-    IsInt a a' → IsInt b b' → Int.mod b' a' != 0 → ¬a ∣ b
-  | _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, e => mt Int.mod_eq_zero_of_dvd (by simpa using e)
+    IsInt a a' → IsInt b b' → Int.emod b' a' != 0 → ¬a ∣ b
+  | _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, e => mt Int.emod_eq_zero_of_dvd (by simpa using e)
 
 /-- The `norm_num` extension which identifies expressions of the form `(a : ℤ) ∣ b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
@@ -167,7 +167,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
     haveI' : Int.mul $na $c =Q $nb := ⟨⟩
     return .isTrue q(isInt_dvd_true $pa $pb (.refl $nb))
   else
-    have : Q(Int.mod $nb $na != 0) := (q(Eq.refl true) : Expr)
+    have : Q(Int.emod $nb $na != 0) := (q(Eq.refl true) : Expr)
     return .isFalse q(isInt_dvd_false $pa $pb $this)
 
 end Mathlib.Meta.NormNum

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "41bb40b762bf2665779c020ceb45f4b7430baa4b",
+   "rev": "707ae20491b28d6f56bf441f590f360e442b79a7",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -60,6 +60,16 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a6fffcf1f54cacd41e34b1fbee35627306da714c",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "mathlib",
  "lakeDir": ".lake"}

lakefile.lean

@@ -12,7 +12,8 @@ require "leanprover-community" / "Qq" @ git "master"
 require "leanprover-community" / "aesop" @ git "master"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.42"
 require "leanprover-community" / "importGraph" @ git "main"
-require "siddhartha-gadgil" / "LeanSearchClient" @ git "main"
+require LeanSearchClient from git
+  "https://github.com/leanprover-community/LeanSearchClient.git" @ "main"
 
 /-!
 ## Options for building mathlib

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-09-10
+leanprover/lean4:nightly-2024-09-11