merge changes from lean-pr-testing-2964

leanprover-community · Dec 21, 2023 · d72b6e3 · d72b6e3
1 parent 44814f1
commit d72b6e3
Show file tree

Hide file tree

Showing 11 changed files with 25 additions and 38 deletions.
diff --git 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
@@ -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
@@ -811,17 +811,17 @@ 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
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-19
+leanprover/lean4:nightly-2023-12-21
diff --git 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