From d72b6e3b9f26927e9c7ce32d0f016dab9cc4feb3 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 21 Dec 2023 22:24:48 +1100 Subject: [PATCH] merge changes from lean-pr-testing-2964 --- Mathlib/Data/List/Join.lean | 2 +- Mathlib/GroupTheory/Perm/Basic.lean | 28 +++++++--------------- Mathlib/RingTheory/Localization/Basic.lean | 8 +++---- Mathlib/Tactic/Widget/Calc.lean | 2 +- Mathlib/Tactic/Widget/Congrm.lean | 3 ++- Mathlib/Tactic/Widget/Conv.lean | 3 ++- Mathlib/Tactic/Widget/Gcongr.lean | 3 ++- lake-manifest.json | 6 ++--- lakefile.lean | 2 +- lean-toolchain | 2 +- test/matrix.lean | 4 ---- 11 files changed, 25 insertions(+), 38 deletions(-) diff --git a/Mathlib/Data/List/Join.lean b/Mathlib/Data/List/Join.lean index 4dca53b75a0e0..4f1c1ffe1fb39 100644 --- a/Mathlib/Data/List/Join.lean +++ b/Mathlib/Data/List/Join.lean @@ -52,7 +52,7 @@ theorem join_filter_isEmpty_eq_false [DecidablePred fun l : List α => l.isEmpty | [] :: L => by simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil] | (a :: l) :: L => by - simp [join_filter_isEmpty_eq_false (L := L), isEmpty_cons] + simp [join_filter_isEmpty_eq_false (L := L)] #align list.join_filter_empty_eq_ff List.join_filter_isEmpty_eq_false @[simp] diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean index d36e7691affe9..52537e2fe1920 100644 --- a/Mathlib/GroupTheory/Perm/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Basic.lean @@ -570,30 +570,18 @@ theorem swap_eq_one_iff {i j : α} : swap i j = (1 : Perm α) ↔ i = j := swap_eq_refl_iff #align equiv.swap_eq_one_iff Equiv.swap_eq_one_iff -theorem swap_mul_eq_iff {i j : α} {σ : Perm α} : swap i j * σ = σ ↔ i = j := - ⟨fun h => by - -- Porting note: added `_root_.` - have swap_id : swap i j = 1 := mul_right_cancel (_root_.trans h (one_mul σ).symm) - rw [← swap_apply_right i j, swap_id] - rfl, - fun h => by erw [h, swap_self, one_mul]⟩ +theorem swap_mul_eq_iff {i j : α} {σ : Perm α} : swap i j * σ = σ ↔ i = j := by + rw [mul_left_eq_self, swap_eq_one_iff] #align equiv.swap_mul_eq_iff Equiv.swap_mul_eq_iff -theorem mul_swap_eq_iff {i j : α} {σ : Perm α} : σ * swap i j = σ ↔ i = j := - ⟨fun h => by - -- Porting note: added `_root_.` - have swap_id : swap i j = 1 := mul_left_cancel (_root_.trans h (one_mul σ).symm) - rw [← swap_apply_right i j, swap_id] - rfl, - fun h => by erw [h, swap_self, mul_one]⟩ +theorem mul_swap_eq_iff {i j : α} {σ : Perm α} : σ * swap i j = σ ↔ i = j := by + rw [mul_right_eq_self, swap_eq_one_iff] #align equiv.mul_swap_eq_iff Equiv.mul_swap_eq_iff -theorem swap_mul_swap_mul_swap {x y z : α} (hwz : x ≠ y) (hxz : x ≠ z) : - swap y z * swap x y * swap y z = swap z x := - Equiv.ext fun n => by - simp only [swap_apply_def, Perm.mul_apply] - -- Porting note: was `cc` - split_ifs <;> aesop +theorem swap_mul_swap_mul_swap {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) : + swap y z * swap x y * swap y z = swap z x := by + nth_rewrite 2 [← swap_inv] + rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm] #align equiv.swap_mul_swap_mul_swap Equiv.swap_mul_swap_mul_swap end Swap diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean index 53992ef79332c..56bb99a582984 100644 --- a/Mathlib/RingTheory/Localization/Basic.lean +++ b/Mathlib/RingTheory/Localization/Basic.lean @@ -811,8 +811,8 @@ theorem isLocalization_iff_of_algEquiv [Algebra R P] (h : S ≃ₐ[R] P) : #align is_localization.is_localization_iff_of_alg_equiv IsLocalization.isLocalization_iff_of_algEquiv theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) : - IsLocalization M S ↔ - haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra; IsLocalization M P := + IsLocalization M S ↔ haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra; + IsLocalization M P := letI := (h.toRingHom.comp <| algebraMap R S).toAlgebra isLocalization_iff_of_algEquiv M { h with commutes' := fun _ => rfl } #align is_localization.is_localization_iff_of_ring_equiv IsLocalization.isLocalization_iff_of_ringEquiv @@ -820,8 +820,8 @@ theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) : variable (S) theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) : - haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra - IsLocalization (M.map h.toMonoidHom) S := by + haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra; + IsLocalization (M.map h.toMonoidHom) S := by letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra constructor · rintro ⟨_, ⟨y, hy, rfl⟩⟩ diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean index 634be8df3c637..0e2a1c8d4b2cf 100644 --- a/Mathlib/Tactic/Widget/Calc.lean +++ b/Mathlib/Tactic/Widget/Calc.lean @@ -137,6 +137,6 @@ elab_rules : tactic let json := open scoped Std.Json in json% {"replaceRange": $(replaceRange), "isFirst": $(isFirst), "indent": $(indent)} - ProofWidgets.savePanelWidgetInfo proofTerm `CalcPanel (pure json) + Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) proofTerm isFirst := false evalCalc (← `(tactic|calc%$calcstx $stx)) diff --git a/Mathlib/Tactic/Widget/Congrm.lean b/Mathlib/Tactic/Widget/Congrm.lean index abf8365734b0f..9095c828b36ae 100644 --- a/Mathlib/Tactic/Widget/Congrm.lean +++ b/Mathlib/Tactic/Widget/Congrm.lean @@ -51,4 +51,5 @@ open scoped Json in subexpressions in the goal.-/ elab stx:"congrm?" : tactic => do let some replaceRange := (← getFileMap).rangeOfStx? stx | return - savePanelWidgetInfo stx ``CongrmSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) } + Widget.savePanelWidgetInfo CongrmSelectionPanel.javascriptHash + (pure $ json% { replaceRange: $(replaceRange) }) stx diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean index aa268c2bdcdf2..aabc847b6ac06 100644 --- a/Mathlib/Tactic/Widget/Conv.lean +++ b/Mathlib/Tactic/Widget/Conv.lean @@ -133,4 +133,5 @@ open scoped Json in in the goal.-/ elab stx:"conv?" : tactic => do let some replaceRange := (← getFileMap).rangeOfStx? stx | return - savePanelWidgetInfo stx ``ConvSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) } + Widget.savePanelWidgetInfo ConvSelectionPanel.javascriptHash + (pure $ json% { replaceRange: $(replaceRange) }) stx diff --git a/Mathlib/Tactic/Widget/Gcongr.lean b/Mathlib/Tactic/Widget/Gcongr.lean index df7ce0c32a9c9..f4fb3cc4788f6 100644 --- a/Mathlib/Tactic/Widget/Gcongr.lean +++ b/Mathlib/Tactic/Widget/Gcongr.lean @@ -49,4 +49,5 @@ open scoped Json in subexpressions in the goal.-/ elab stx:"gcongr?" : tactic => do let some replaceRange := (← getFileMap).rangeOfStx? stx | return - savePanelWidgetInfo stx ``GCongrSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) } + Widget.savePanelWidgetInfo GCongrSelectionPanel.javascriptHash + (pure $ json% { replaceRange: $(replaceRange) }) stx diff --git a/lake-manifest.json b/lake-manifest.json index bfa77660582b7..770a08b2e6eb6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "49b36f282e56ce9a695923e2df156cd4abf33fc8", + "rev": "4165f2c46b6dffcca0abbacb1cea2dafa1282166", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "bump/v4.5.0", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749", + "rev": "bf61e90de075abfa27f638922e7aafafdce77c44", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.23", + "inputRev": "v0.0.24-pre2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index e4aa94ed240b3..7070f27f49d7d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -29,7 +29,7 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" require std from git "https://github.com/leanprover/std4" @ "bump/v4.5.0" require Qq from git "https://github.com/leanprover-community/quote4" @ "master" require aesop from git "https://github.com/leanprover-community/aesop" @ "master" -require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23" +require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.24-pre2" require Cli from git "https://github.com/leanprover/lean4-cli" @ "main" /-! diff --git a/lean-toolchain b/lean-toolchain index 2dfbd8295af30..ab0fdcb8b0063 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-12-19 +leanprover/lean4:nightly-2023-12-21 diff --git a/test/matrix.lean b/test/matrix.lean index 373088b059c88..5fcf2ebf07e83 100644 --- a/test/matrix.lean +++ b/test/matrix.lean @@ -1,7 +1,3 @@ -/- -manually ported from -https://github.com/leanprover-community/mathlib/blob/4f4a1c875d0baa92ab5d92f3fb1bb258ad9f3e5b/test/matrix.lean --/ import Mathlib.Data.Matrix.Notation import Mathlib.GroupTheory.Perm.Fin import Mathlib.LinearAlgebra.Matrix.Determinant