chore: bump to v4.10.0-rc2

MIL/C03_Logic/S04_Conjunction_and_Iff.lean

@@ -1,7 +1,7 @@
 -- BOTH:
 import MIL.Common
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Prime.Basic
 
 namespace C03S04
 

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -1,6 +1,6 @@
 -- BOTH:
 import Mathlib.Data.Set.Lattice
-import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Prime.Basic
 import MIL.Common
 
 /- TEXT:

MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean

@@ -1,6 +1,6 @@
 import MIL.Common
 import Mathlib.Data.Nat.Factorization.Basic
-import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Prime.Basic
 /- OMIT:
 -- fix this.
 -- import Mathlib.Data.Real.Irrational

MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean

@@ -1,5 +1,4 @@
 import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Algebra.BigOperators.Basic
 import MIL.Common
 
 /- TEXT:

MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

@@ -1,5 +1,4 @@
-import Mathlib.Data.Nat.Prime
-import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Data.Nat.Prime.Basic
 import MIL.Common
 
 open BigOperators

MIL/C08_Groups_and_Rings/S01_Groups.lean

@@ -433,7 +433,7 @@ open scoped Classical
 open Fintype
 -- EXAMPLES:
 
-example {G : Type*} [Group G] [Fintype G] (G' : Subgroup G) : card G' ∣ card G :=
+example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G :=
   ⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩
 
 -- BOTH:
@@ -451,7 +451,7 @@ so do not use ``exact?`` too quickly.)
 BOTH: -/
 -- QUOTE:
 lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} [Fintype H] :
-    H = ⊥ ↔ card H = 1 := by
+    H = ⊥ ↔ Nat.card H = 1 := by
   suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
     simpa [eq_bot_iff_forall, card_eq_one_iff]
 /- EXAMPLES:
@@ -469,12 +469,12 @@ SOLUTIONS: -/
 -- BOTH:
 
 lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G) [Fintype H] [Fintype K]
-    (h : (card H).Coprime (card K)) : H ⊓ K = ⊥ := by
+    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
 /- EXAMPLES:
   sorry
 SOLUTIONS: -/
-  have D₁ : card (H ⊓ K : Subgroup G) ∣ card H := card_dvd_of_le inf_le_left
-  have D₂ : card (H ⊓ K : Subgroup G) ∣ card K := card_dvd_of_le inf_le_right
+  have D₁ : Nat.card (H ⊓ K : Subgroup G) ∣ Nat.card H := card_dvd_of_le inf_le_left
+  have D₂ : Nat.card (H ⊓ K : Subgroup G) ∣ Nat.card K := card_dvd_of_le inf_le_right
   exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂)
 -- QUOTE.
 
@@ -826,33 +826,32 @@ open MonoidHom
 #check Subgroup.index_mul_card
 #check Nat.eq_of_mul_eq_mul_right
 
--- The following line is working around a Lean bug that will be fixed very soon.
-attribute [-instance] Subtype.instInhabited
-
-lemma aux_card_eq [Fintype G] (h' : card G = card H * card K) : card (G ⧸ H) = card K := by
+lemma aux_card_eq [Fintype G] (h' : Nat.card G = Nat.card H * Nat.card K) :
+    Nat.card (G ⧸ H) = Nat.card K := by
 /- EXAMPLES:
   sorry
 SOLUTIONS: -/
   have := calc
-    card (G ⧸ H) * card H = card G := by rw [← H.index_eq_card, H.index_mul_card]
-    _                     = card K * card H := by rw [h', mul_comm]
+    Nat.card (G ⧸ H) * Nat.card H = Nat.card G := by rw [← H.index_eq_card, H.index_mul_card]
+    _                             = Nat.card K * Nat.card H := by rw [h', mul_comm]
 
-  exact Nat.eq_of_mul_eq_mul_right card_pos this
+  exact Nat.eq_of_mul_eq_mul_right Nat.card_pos this
 -- QUOTE.
 
 /- TEXT:
 From now on, we assume that our subgroups are normal and disjoint, and we assume the cardinality
 condition. Now we construct the first building block of the desired isomorphism.
 BOTH: -/
 -- QUOTE:
-variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K)
+variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K)
+  (h' : Nat.card G = Nat.card H * Nat.card K)
 
 #check bijective_iff_injective_and_card
 #check ker_eq_bot_iff
 #check restrict
 #check ker_restrict
 
-def iso₁ [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K) : K ≃* G ⧸ H := by
+def iso₁ [Fintype G] (h : Disjoint H K) (h' : Nat.card G = Nat.card H * Nat.card K) : K ≃* G ⧸ H := by
 /- EXAMPLES:
   sorry
 SOLUTIONS: -/
@@ -862,6 +861,7 @@ SOLUTIONS: -/
   · rw [← ker_eq_bot_iff, (QuotientGroup.mk' H).ker_restrict K]
     simp [h]
   · symm
+    simp only [card_eq_nat_card]
     exact aux_card_eq h'
 -- QUOTE.
 
@@ -880,7 +880,9 @@ SOLUTIONS: -/
   constructor
   · rw [← ker_eq_bot_iff, ker_prod]
     simp [h.symm.eq_bot]
-  · rw [card_prod, aux_card_eq h', aux_card_eq (mul_comm (card H) _▸ h'), h']
+  · rw [card_prod]
+    simp only [card_eq_nat_card]
+    rw [aux_card_eq h', aux_card_eq (mul_comm (Nat.card H) _▸ h'), h']
 -- QUOTE.
 
 /- TEXT:
@@ -894,7 +896,7 @@ def finalIso : G ≃* H × K :=
 /- EXAMPLES:
   sorry
 SOLUTIONS: -/
-  (iso₂ h h').trans ((iso₁ h.symm (mul_comm (card H) _ ▸ h')).prodCongr (iso₁ h h')).symm
+  (iso₂ h h').trans ((iso₁ h.symm (mul_comm (Nat.card H) _ ▸ h')).prodCongr (iso₁ h h')).symm
 
 end
 end QuotientGroup

MIL/C09_Topology/S02_Metric_Spaces.lean

@@ -590,7 +590,7 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : 
     have I :=
       calc
         closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) :=
-          (incl n).trans (inter_subset_left _ _)
+          (incl n).trans Set.inter_subset_left
         _ ⊆ closedBall (c n) (B n) := closedBall_subset_closedBall (rB n)
 
     exact I A
@@ -604,7 +604,7 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : 
     intro n
     refine' Nat.le_induction _ fun m hnm h ↦ _
     · exact Subset.rfl
-    · exact (incl m).trans ((Set.inter_subset_left _ _).trans h)
+    · exact (incl m).trans (Set.inter_subset_left.trans h)
   have yball : ∀ n, y ∈ closedBall (c n) (r n) := by
     intro n
     refine' isClosed_ball.mem_of_tendsto ylim _
@@ -614,7 +614,7 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : 
   · suffices ∀ n, y ∈ f n by rwa [Set.mem_iInter]
     intro n
     have : closedBall (c (n + 1)) (r (n + 1)) ⊆ f n :=
-      Subset.trans (incl n) (inter_subset_right _ _)
+      Subset.trans (incl n) Set.inter_subset_right
     exact this (yball (n + 1))
   calc
     dist y x ≤ r 0 := yball 0

MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean

@@ -100,6 +100,6 @@ but Mathlib introduces special notation for saying that a property holds
 almost everywhere.
 EXAMPLES: -/
 -- QUOTE:
-example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in μ.ae, P x :=
+example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in ae μ, P x :=
   Iff.rfl
 -- QUOTE.

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "60d622c124cebcecc000853cdae93f4251f4beb5",
+   "scope": "leanprover-community",
+   "rev": "937cd3219c0beffa7b623d2905707d1304da259e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +14,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "bbb5ab510fd407350094422ee230c15ab7323769",
+   "scope": "leanprover-community",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "8932a3d688d2bbf500429c4c888de4181086aad5",
+   "scope": "",
+   "rev": "52249e2d76c16ba8e12bf348fa61fffe7ab3913e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.10.0-rc2