From ee3cdfe13bb9ccd3bdd988904bfd797753eb1348 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Thu, 4 Jan 2024 19:59:49 +0100 Subject: [PATCH] :up_arrow: Upgrade mathlib --- Rubin.lean | 4 +--- Rubin/LocallyDense.lean | 2 +- Rubin/Period.lean | 20 +++++++++++--------- Rubin/Support.lean | 22 ++++++++++++---------- lake-manifest.json | 12 ++++++------ lean-toolchain | 2 +- 6 files changed, 32 insertions(+), 30 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index 4f7c01f..af069ca 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -463,7 +463,6 @@ by apply ge_antisymm { apply Period.notfix_le_period' - · exact n_pos · apply Period.period_pos' · exact Set.nonempty_of_mem p_in_U · exact exp_ne_zero @@ -2101,8 +2100,7 @@ by exact RubinSpace.lim_mk α F theorem RubinSpace.lim_continuous : Continuous (RubinSpace.lim (G := G) (α := α)) := by - -- TODO: rename to continuous_iff when upgrading mathlib - apply (RegularSupportBasis.isBasis G α).continuous + rw [(RegularSupportBasis.isBasis G α).continuous_iff] intro S S_in_basis apply TopologicalSpace.isOpen_generateFrom_of_mem rw [RubinFilterBasis.mem_iff] diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean index 4f0eeb1..be49e61 100644 --- a/Rubin/LocallyDense.lean +++ b/Rubin/LocallyDense.lean @@ -171,7 +171,7 @@ where lemma disjoint_nbhd [T2Space α] {g : G} {x : α} (x_moved: g • x ≠ x) : ∃ U: Set α, IsOpen U ∧ x ∈ U ∧ Disjoint U (g •'' U) := by - have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 (g • x) x x_moved + have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 x_moved let U := (g⁻¹ •'' V) ∩ W use U constructor diff --git a/Rubin/Period.lean b/Rubin/Period.lean index 983a1b4..b895624 100644 --- a/Rubin/Period.lean +++ b/Rubin/Period.lean @@ -19,13 +19,15 @@ theorem period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0) (gmp_eq_p : g ^ m • p = p) : 0 < Rubin.Period.period p g ∧ Rubin.Period.period p g ≤ m := by constructor - · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith; - rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith; - exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩ + · by_contra h' + have period_zero : Rubin.Period.period p g = 0 := by linarith + rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, _⟩ | h + · linarith + · exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩ exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩ #align period_le_fix Rubin.Period.period_le_fix -theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0) +theorem notfix_le_period {p : α} {g : G} {n : ℕ} (period_pos : Rubin.Period.period p g > 0) (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) : n ≤ Rubin.Period.period p g := by by_contra period_le @@ -34,10 +36,10 @@ theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0) (Nat.sInf_mem (Nat.nonempty_of_pos_sInf period_pos)).2 #align notfix_le_period Rubin.Period.notfix_le_period -theorem notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0) +theorem notfix_le_period' {p : α} {g : G} {n : ℕ} (period_pos : 0 < Rubin.Period.period p g) (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ Rubin.Period.period p g := - Rubin.Period.notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) => + Rubin.Period.notfix_le_period period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) => pmoves (⟨i, i_lt_n⟩ : Fin n) i_pos #align notfix_le_period' Rubin.Period.notfix_le_period' @@ -65,7 +67,7 @@ theorem moves_within_period' {z : ℤ} (g : G) (x : α) : 0 < z → z < period x g → g^z • x ≠ x := by intro n_pos n_lt_period - rw [<-Int.ofNat_natAbs_eq_of_nonneg _ (Int.le_of_lt n_pos)] + rw [<-Int.natAbs_of_nonneg (Int.le_of_lt n_pos)] rw [zpow_ofNat] apply moves_within_period · rw [<-Int.natAbs_zero] @@ -86,7 +88,7 @@ theorem periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup (exp_ne_zero : Monoid.exponent H ≠ 0) : (Rubin.Period.periods U H).Nonempty ∧ BddAbove (Rubin.Period.periods U H) ∧ - ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p := + ∃ (m : ℕ), m > 0 ∧ ∀ (p : α) (g : H), g ^ m • p = p := by rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩ have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by @@ -135,7 +137,7 @@ theorem zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty) Rubin.Period.period (p : α) (g : G) ≤ sSup (Rubin.Period.periods U H) := by rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with - ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ + ⟨_periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ intro p g have period_in_periods : Rubin.Period.period (p : α) (g : G) ∈ Rubin.Period.periods U H := by use p; use g diff --git a/Rubin/Support.lean b/Rubin/Support.lean index aa880f2..d707bae 100644 --- a/Rubin/Support.lean +++ b/Rubin/Support.lean @@ -387,16 +387,18 @@ variable [ContinuousConstSMul G α] theorem support_isOpen (g : G) [T2Space α]: IsOpen (Support α g) := by apply isOpen_iff_forall_mem_open.mpr intro x xmoved - rcases T2Space.t2 (g • x) x xmoved with ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩ - exact - ⟨V ∩ (g⁻¹ •'' U), fun y yW => - Disjoint.ne_of_mem - disjoint_U_V - (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW)) - (Set.mem_of_mem_inter_left yW), - IsOpen.inter open_V (smulImage_isOpen g⁻¹ open_U), - ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩ - ⟩ + let ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩ := T2Space.t2 xmoved + + refine ⟨ + V ∩ (g⁻¹ •'' U), + ?subset, + IsOpen.inter open_V (smulImage_isOpen g⁻¹ open_U), + ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩ + ⟩ + intro y ⟨yV, yU⟩ + apply Disjoint.ne_of_mem disjoint_U_V _ yV + rw [mem_inv_smulImage] at yU + exact yU end Continuous diff --git a/lake-manifest.json b/lake-manifest.json index f5e56e8..d18678d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0", + "rev": "d8610e1bcb91c013c3d868821c0ef28bf693be07", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c", + "rev": "1c88406514a636d241903e2e288d21dc6d861e01", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf", + "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749", + "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.23", + "inputRev": "v0.0.24", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "c0f7586a3e77660ff51b9156783aaf8eab9506de", + "rev": "95f91f8e66f14c0eecde8da6dbfeff39d44cbd81", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 91ccf6a..3f21e50 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.4.0-rc1 +leanprover/lean4:v4.5.0-rc1