bump mathlib (#47)

FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean

@@ -24,7 +24,6 @@ import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Nat.Pow
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Data.Nat.Parity
-import Mathlib.Data.Real.ENNReal
 import Mathlib.FieldTheory.Finite.Basic
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.GroupTheory.Coset

FormalBook/Ch02_Bertrand's_postulate.lean

@@ -82,26 +82,20 @@ theorem real_main_inequality {x : ℝ} (n_large : (512 : ℝ) ≤ x) :
     exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4
   refine' ⟨18, 512, by norm_num1, by norm_num1, n_large, _, _⟩
   · have : sqrt (2 * 18) = 6 := (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-    rw [hf, log_nonneg_iff, this]
-    rw [one_le_div] <;> norm_num1
-    apply le_trans _ (le_mul_of_one_le_left _ _) <;> norm_num1
-    apply Real.rpow_le_rpow <;> norm_num1
-    apply rpow_nonneg_of_nonneg; norm_num1
-    apply rpow_pos_of_pos; norm_num1
-    apply hf' 18; norm_num1
+    rw [hf _ (by norm_num1), log_nonneg_iff (by positivity), this, one_le_div (by norm_num1)]
     norm_num1
   · have : sqrt (2 * 512) = 32 :=
       (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-    rw [hf, log_nonpos_iff (hf' _ _), this, div_le_one] <;> norm_num1
-    · conv in 512 => equals 2 ^ 9 => norm_num1
-      conv in 1024 => equals 2 ^ 10 => norm_num1
-      conv in 32 => rw [← Nat.cast_ofNat]
-      rw [rpow_nat_cast, ← pow_mul, ← pow_add]
-      conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
-      rw [← rpow_mul, ← rpow_nat_cast]
-      apply rpow_le_rpow_of_exponent_le
-      all_goals norm_num1
-    · apply rpow_pos_of_pos four_pos
+    rw [hf _ (by norm_num1), log_nonpos_iff (hf' _ (by norm_num1)), this,
+        div_le_one (by positivity)]
+    conv in 512 => equals 2 ^ 9 => norm_num1
+    conv in 2 * 512 => equals 2 ^ 10 => norm_num1
+    conv in 32 => rw [← Nat.cast_ofNat]
+    rw [rpow_nat_cast, ← pow_mul, ← pow_add]
+    conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
+    rw [← rpow_mul, ← rpow_nat_cast]
+    apply rpow_le_rpow_of_exponent_le
+    all_goals norm_num1
 end Bertrand
 
 
@@ -113,17 +107,13 @@ theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) :
     n * (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := by
   rw [← @cast_le ℝ]
   simp only [cast_add, cast_one, cast_mul, cast_pow, ← Real.rpow_nat_cast]
-  have n_pos : 0 < n := (by decide : 0 < 512).trans_le n_large
-  have n2_pos : 1 ≤ 2 * n := mul_pos (by decide) n_pos
-  refine' _root_.trans (mul_le_mul _ _ _ _)
-      (Bertrand.real_main_inequality (by exact_mod_cast n_large))
-  · refine' mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
-    refine' Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast n2_pos) _
-    exact_mod_cast Real.nat_sqrt_le_real_sqrt
-  · exact Real.rpow_le_rpow_of_exponent_le (by norm_num1) (cast_div_le.trans (by norm_cast))
-  · exact Real.rpow_nonneg_of_nonneg (by norm_num1) _
-  · refine' mul_nonneg (Nat.cast_nonneg _) _
-    exact Real.rpow_nonneg_of_nonneg (mul_nonneg zero_le_two (Nat.cast_nonneg _)) _
+  refine' _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))
+  gcongr
+  · have n2_pos : 0 < 2 * n := by positivity
+    exact mod_cast n2_pos
+  · exact_mod_cast Real.nat_sqrt_le_real_sqrt
+  · norm_num1
+  · exact cast_div_le.trans (by norm_cast)
 
 /-- A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime
 factorization of the central binomial coefficent only has factors at most `2 * n / 3 + 1`.

FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean

@@ -62,15 +62,15 @@ def legendre_sym (a : ℤ) : ℤ :=
 Fermat's little theorem: If `a` is nonzero modulo the odd prime `p`, then `a ^ (p - 1) = -1`
 modulo `p`.
 -/
-lemma fermat_little (a : ℤ): (a ≠ (0 : ZMod p)) → a ^ (p - 1) = (-1 : ZMod p) := by
+lemma fermat_little (a : ℤ): (a : ZMod p) ≠ 0 → a ^ (p - 1) = (-1 : ZMod p) := by
   let units_finset := (Finset.univ : Finset (ZMod p)).erase 0
   let image_finset := (units_finset).image (fun x : ZMod p => (a : ZMod p) * x)
   have : units_finset = image_finset := by sorry
   sorry
 
 
 theorem euler_criterion (a : ℤ) :
-  a ≠ (0 : ZMod p) → (legendre_sym p a : ZMod p) = a ^ ((p - 1) / 2) := by
+  (a : ZMod p) ≠ 0 → (legendre_sym p a : ZMod p) = a ^ ((p - 1) / 2) := by
   sorry
 
 lemma product_rule (a b : ℤ) :
@@ -84,7 +84,7 @@ For the statement, see `theorem quadratic_reciprocity_1`.
 
 -- Maybe define the function `r i` = "reduce p i" explicitly ?
 --TODO : This should probably be broken down a little bit first
-lemma lemma_of_Gauss (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) (h_a : a ≠ (0 : ZMod p))
+lemma lemma_of_Gauss (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) (h_a : (a : ZMod p) ≠ 0)
   ( r : ℤ → ℤ ) (h_r : (∀ i, (- (p: ℤ) - 1)/2 ≤ r i ∧ r i ≤ ((p : ℤ) - 1)/2))
   ( H : ∀ i, (r i : ℤ) = (a * i : ZMod p) ) :
    -- TODO: check why this is needed after porting to lean4

FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean

@@ -369,7 +369,7 @@ theorem wedderburn (h: Fintype R): IsField R := by
 
   have : 1 ≤ Fintype.card { x // x ∈ center R } := by
     refine' Fintype.card_pos_iff.mpr _
-    exact One.nonempty
+    exact ⟨1, Subring.one_mem (center R)⟩
   have h_q : |((q : ℤ) - 1)| = q - 1 := by
     norm_num
     exact this

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d8610e1bcb91c013c3d868821c0ef28bf693be07",
+   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f",
+   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.24",
+   "inputRev": "v0.0.25",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -46,10 +46,19 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "95f91f8e66f14c0eecde8da6dbfeff39d44cbd81",
+   "rev": "66439f5ad62664e7dda3c6b6a5fedbfee4112950",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,