[Merged by Bors] - feat: adaptations for leanprover/lean4#2964

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]

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

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))

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

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

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

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",

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"
 
 /-!

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-19
+leanprover/lean4:nightly-2023-12-21