From 2e845584e211800b1a017d816fa4a012980b9ae3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 17 Jul 2024 06:06:15 +1000 Subject: [PATCH] chore: bump to v4.10.0-rc2 --- MIL/C03_Logic/S04_Conjunction_and_Iff.lean | 2 +- MIL/C04_Sets_and_Functions/S01_Sets.lean | 2 +- .../S01_Irrational_Roots.lean | 2 +- .../S02_Induction_and_Recursion.lean | 1 - .../S03_Infinitely_Many_Primes.lean | 3 +- MIL/C08_Groups_and_Rings/S01_Groups.lean | 34 ++++++++++--------- MIL/C09_Topology/S02_Metric_Spaces.lean | 6 ++-- .../S02_Measure_Theory.lean | 2 +- lake-manifest.json | 25 +++++++++----- lean-toolchain | 2 +- 10 files changed, 43 insertions(+), 36 deletions(-) diff --git a/MIL/C03_Logic/S04_Conjunction_and_Iff.lean b/MIL/C03_Logic/S04_Conjunction_and_Iff.lean index 68c49f5c..6b6c0324 100644 --- a/MIL/C03_Logic/S04_Conjunction_and_Iff.lean +++ b/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 diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean index 0c3053ce..d953811d 100644 --- a/MIL/C04_Sets_and_Functions/S01_Sets.lean +++ b/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: diff --git a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean index c159d6a9..bc2d593e 100644 --- a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean +++ b/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 diff --git a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean index 3d84fc06..6728fdbe 100644 --- a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean +++ b/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: diff --git a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean b/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean index 5f7d1475..7bcf2123 100644 --- a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean +++ b/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 diff --git a/MIL/C08_Groups_and_Rings/S01_Groups.lean b/MIL/C08_Groups_and_Rings/S01_Groups.lean index e047e3d1..5833d88f 100644 --- a/MIL/C08_Groups_and_Rings/S01_Groups.lean +++ b/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,18 +826,16 @@ 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: @@ -845,14 +843,15 @@ From now on, we assume that our subgroups are normal and disjoint, and we assume 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 diff --git a/MIL/C09_Topology/S02_Metric_Spaces.lean b/MIL/C09_Topology/S02_Metric_Spaces.lean index 33f07fc1..a0e5ab0f 100644 --- a/MIL/C09_Topology/S02_Metric_Spaces.lean +++ b/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 diff --git a/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean b/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean index eaa97eed..7c6e01df 100644 --- a/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean +++ b/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. diff --git a/lake-manifest.json b/lake-manifest.json index 59410e07..d7c1198e 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lean-toolchain b/lean-toolchain index 78f39e21..6a4259fa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.10.0-rc2