diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 1445f42fcefef..dfdf4c6a4850e 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -256,10 +256,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index aa0743cccb046..5bcb0aef7b5f8 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -16,6 +16,7 @@ on:
       - 'nolints'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+  merge_group:
 
 name: continuous integration
 
@@ -262,10 +263,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 3f38af34d832a..186b741d46a99 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -242,10 +242,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
index a65d2cab1d28a..07c0ecb93f7b0 100644
--- a/.github/workflows/build_fork.yml
+++ b/.github/workflows/build_fork.yml
@@ -260,10 +260,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
diff --git a/.github/workflows/mk_build_yml.sh b/.github/workflows/mk_build_yml.sh
index e41f33b2205e0..96cf301b33a26 100755
--- a/.github/workflows/mk_build_yml.sh
+++ b/.github/workflows/mk_build_yml.sh
@@ -28,6 +28,7 @@ on:
       - 'nolints'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+  merge_group:
 
 name: continuous integration
 EOF
diff --git a/Archive.lean b/Archive.lean
index 2315f50c1c1c5..e78b6b119b265 100644
--- a/Archive.lean
+++ b/Archive.lean
@@ -1,4 +1,7 @@
 import Archive.Arithcc
+import Archive.Examples.IfNormalization.Result
+import Archive.Examples.IfNormalization.Statement
+import Archive.Examples.IfNormalization.WithoutAesop
 import Archive.Examples.MersennePrimes
 import Archive.Examples.PropEncodable
 import Archive.Imo.Imo1959Q1
diff --git a/Archive/Examples/IfNormalization/Result.lean b/Archive/Examples/IfNormalization/Result.lean
new file mode 100644
index 0000000000000..423cc8bde76fd
--- /dev/null
+++ b/Archive/Examples/IfNormalization/Result.lean
@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2023 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Archive.Examples.IfNormalization.Statement
+import Mathlib.Data.List.AList
+import Mathlib.Tactic.Recall
+
+/-!
+# A solution to the if normalization challenge in Lean.
+
+See `Statement.lean` for background.
+-/
+
+set_option autoImplicit true
+
+macro "◾" : tactic => `(tactic| aesop)
+macro "◾" : term => `(term| by aesop)
+
+namespace IfExpr
+
+/-!
+We add some local simp lemmas so we can unfold the definitions of the normalization condition.
+-/
+attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
+  List.disjoint
+
+/-!
+Adding these lemmas to the simp set allows Lean to handle the termination proof automatically.
+-/
+attribute [local simp] Nat.lt_add_one_iff le_add_of_le_right
+
+/-!
+Some further simp lemmas for handling if-then-else statements.
+-/
+attribute [local simp] apply_ite ite_eq_iff'
+
+-- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
+-- rather than finding it by typeclass search.
+-- See https://github.com/leanprover/lean4/pull/2816
+@[simp] theorem decide_eq_true_eq {i : Decidable p} : (@decide p i = true) = p :=
+  _root_.decide_eq_true_eq
+
+
+/-!
+Simp lemmas for `eval`.
+We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we know the shape of `i`.
+-/
+@[simp] theorem eval_lit : (lit b).eval f  = b := rfl
+@[simp] theorem eval_var : (var i).eval f  = f i := rfl
+@[simp] theorem eval_ite_lit :
+    (ite (.lit b) t e).eval f = bif b then t.eval f else e.eval f := rfl
+@[simp] theorem eval_ite_var :
+    (ite (.var i) t e).eval f = bif f i then t.eval f else e.eval f := rfl
+@[simp] theorem eval_ite_ite :
+    (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
+  cases h : eval f a <;> simp_all [eval]
+
+/-- Custom size function for if-expressions, used for proving termination. -/
+@[simp] def normSize : IfExpr → Nat
+  | lit _ => 0
+  | var _ => 1
+  | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
+
+/-- Normalizes the expression at the same time as assigning all variables in
+`e` to the literal booleans given by `l` -/
+def normalize (l : AList (fun _ : ℕ => Bool)) :
+    (e : IfExpr) → { e' : IfExpr //
+        (∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
+        ∧ e'.normalized
+        ∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
+  | lit b => ⟨lit b, ◾⟩
+  | var v =>
+    match h : l.lookup v with
+    | none => ⟨var v, ◾⟩
+    | some b => ⟨lit b, ◾⟩
+  | .ite (lit true)   t e => have t' := normalize l t; ⟨t'.1, ◾⟩
+  | .ite (lit false)  t e => have e' := normalize l e; ⟨e'.1, ◾⟩
+  | .ite (.ite a b c) t e => have i' := normalize l (.ite a (.ite b t e) (.ite c t e)); ⟨i'.1, ◾⟩
+  | .ite (var v)      t e =>
+    match h : l.lookup v with
+    | none =>
+      have ⟨t', ht₁, ht₂, ht₃⟩ := normalize (l.insert v true) t
+      have ⟨e', he₁, he₂, he₃⟩ := normalize (l.insert v false) e
+      ⟨if t' = e' then t' else .ite (var v) t' e', by
+        refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
+        · -- eval = eval
+          simp
+          cases hfv : f v
+          · simp_all
+            congr
+            ext w
+            by_cases w = v <;> ◾
+          · simp [h, ht₁]
+            congr
+            ext w
+            by_cases w = v <;> ◾
+        · -- normalized
+          have := ht₃ v
+          have := he₃ v
+          ◾
+        · -- lookup = none
+          have := ht₃ w
+          have := he₃ w
+          by_cases w = v <;> ◾⟩
+    | some b =>
+      have i' := normalize l (.ite (lit b) t e); ⟨i'.1, ◾⟩
+  termination_by normalize e => e.normSize
+  decreasing_by { decreasing_with simp (config := { arith := true }) [Zero.zero]; done }
+
+/-
+We recall the statement of the if-normalization problem.
+
+We want a function from if-expressions to if-expressions,
+that outputs normalized if-expressions and preserves meaning.
+-/
+recall IfNormalization :=
+  { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }
+
+example : IfNormalization :=
+  ⟨_, fun e => ⟨(IfExpr.normalize ∅ e).2.2.1, by simp [(IfExpr.normalize ∅ e).2.1]⟩⟩
diff --git a/Archive/Examples/IfNormalization/Statement.lean b/Archive/Examples/IfNormalization/Statement.lean
new file mode 100644
index 0000000000000..944efe6ae7c26
--- /dev/null
+++ b/Archive/Examples/IfNormalization/Statement.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+/-!
+# If normalization
+
+Rustan Leino, Stephan Merz, and Natarajan Shankar have recently been discussing challenge problems
+to compare proof assistants.
+(See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rustan's.20challenge)
+
+Their first suggestion was "if-normalization".
+
+This file contains a Lean formulation of the problem. See `Result.lean` for a Lean solution.
+-/
+
+/-- An if-expression is either boolean literal, a numbered variable,
+or an if-then-else expression where each subexpression is an if-expression. -/
+inductive IfExpr
+  | lit : Bool → IfExpr
+  | var : Nat → IfExpr
+  | ite : IfExpr → IfExpr → IfExpr → IfExpr
+deriving DecidableEq, Repr
+
+namespace IfExpr
+
+/--
+An if-expression has a "nested if" if it contains
+an if-then-else where the "if" is itself an if-then-else.
+-/
+def hasNestedIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite (ite _ _ _) _ _ => true
+  | ite _ t e => t.hasNestedIf || e.hasNestedIf
+
+/--
+An if-expression has a "constant if" if it contains
+an if-then-else where the "if" is itself a literal.
+-/
+def hasConstantIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite (lit _) _ _ => true
+  | ite i t e => i.hasConstantIf || t.hasConstantIf || e.hasConstantIf
+
+/--
+An if-expression has a "redundant if" if it contains
+an if-then-else where the then and else clauses are identical.
+-/
+def hasRedundantIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite i t e => t == e || i.hasRedundantIf || t.hasRedundantIf || e.hasRedundantIf
+
+/--
+All the variables appearing in an if-expressions, read left to right, without removing duplicates.
+-/
+def vars : IfExpr → List Nat
+  | lit _ => []
+  | var i => [i]
+  | ite i t e => i.vars ++ t.vars ++ e.vars
+
+/--
+A helper function to specify that two lists are disjoint.
+-/
+def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool
+  | [], _ => true
+  | x::xs, ys => x ∉ ys && xs.disjoint ys
+
+/--
+An if expression evaluates each variable at most once if for each if-then-else
+the variables in the if clause are disjoint from the variables in the then clause, and
+the variables in the if clause are disjoint from the variables in the else clause.
+-/
+def disjoint : IfExpr → Bool
+  | lit _ => true
+  | var _ => true
+  | ite i t e =>
+      i.vars.disjoint t.vars && i.vars.disjoint e.vars && i.disjoint && t.disjoint && e.disjoint
+
+/--
+An if expression is "normalized" if it has not nested, constant, or redundant ifs,
+and it evaluates each variable at most once.
+-/
+def normalized (e : IfExpr) : Bool :=
+  !e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint
+
+/--
+The evaluation of an if expresssion at some assignment of variables.
+-/
+def eval (f : Nat → Bool) : IfExpr → Bool
+  | lit b => b
+  | var i => f i
+  | ite i t e => bif i.eval f then t.eval f else e.eval f
+
+end IfExpr
+
+/--
+This is the statement of the if normalization problem.
+
+We require a function from that transforms if expressions to normalized if expressions,
+preserving all evaluations.
+-/
+def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }
diff --git a/Archive/Examples/IfNormalization/WithoutAesop.lean b/Archive/Examples/IfNormalization/WithoutAesop.lean
new file mode 100644
index 0000000000000..254ac3b982785
--- /dev/null
+++ b/Archive/Examples/IfNormalization/WithoutAesop.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2023 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Scott Morrison
+-/
+import Archive.Examples.IfNormalization.Statement
+import Mathlib.Data.List.AList
+
+/-!
+# A variant of Chris Hughes' solution for the if normalization challenge.
+
+In this variant we eschew the use of `aesop`, and instead write out the proofs.
+
+(In order to avoid duplicated names with `Result.lean`,
+we put primes on the declarations in the file.)
+-/
+
+set_option autoImplicit true
+
+namespace IfExpr
+
+attribute [local simp] eval normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
+  List.disjoint max_add_add_right max_mul_mul_left Nat.lt_add_one_iff le_add_of_le_right
+
+-- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
+-- rather than finding it by typeclass search.
+-- See https://github.com/leanprover/lean4/pull/2816
+@[simp] theorem decide_eq_true_eq' {i : Decidable p} : (@decide p i = true) = p :=
+  _root_.decide_eq_true_eq
+
+theorem eval_ite_ite' :
+    (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
+  cases h : eval f a <;> simp_all
+
+/-- Custom size function for if-expressions, used for proving termination. -/
+@[simp] def normSize' : IfExpr → ℕ
+  | lit _ => 0
+  | var _ => 1
+  | .ite i t e => 2 * normSize' i + max (normSize' t) (normSize' e) + 1
+
+/-- Normalizes the expression at the same time as assigning all variables in
+`e` to the literal booleans given by `l` -/
+def normalize' (l : AList (fun _ : ℕ => Bool)) :
+    (e : IfExpr) → { e' : IfExpr //
+        (∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
+        ∧ e'.normalized
+        ∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
+  | lit b => ⟨lit b, by simp⟩
+  | var v =>
+    match h : l.lookup v with
+    | none => ⟨var v, by simp_all⟩
+    | some b => ⟨lit b, by simp_all⟩
+  | .ite (lit true) t e =>
+    have ⟨t', ht'⟩ := normalize' l t
+    ⟨t', by simp_all⟩
+  | .ite (lit false) t e =>
+    have ⟨e', he'⟩ := normalize' l e
+    ⟨e', by simp_all⟩
+  | .ite (.ite a b c) d e =>
+    have ⟨t', ht₁, ht₂⟩ := normalize' l (.ite a (.ite b d e) (.ite c d e))
+    ⟨t', fun f => by rw [ht₁, eval_ite_ite'], ht₂⟩
+  | .ite (var v) t e =>
+    match h : l.lookup v with
+    | none =>
+      have ⟨t', ht₁, ht₂, ht₃⟩ := normalize' (l.insert v true) t
+      have ⟨e', he₁, he₂, he₃⟩ := normalize' (l.insert v false) e
+      ⟨if t' = e' then t' else .ite (var v) t' e', by
+        refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
+        · simp only [eval, apply_ite, ite_eq_iff']
+          cases hfv : f v
+          · simp (config := {contextual := true}) only [cond_false, h, he₁]
+            refine ⟨fun _ => ?_, fun _ => ?_⟩
+            · congr
+              ext w
+              by_cases w = v <;> rename_i x
+              · substs h
+                simp_all
+              · simp_all
+            · congr
+              ext w
+              by_cases w = v <;> rename_i x
+              · substs h
+                simp_all
+              · simp_all
+          · simp only [cond_true, h, ht₁]
+            refine ⟨fun _ => ?_, fun _ => ?_⟩
+            · congr
+              ext w
+              by_cases w = v <;> rename_i x
+              · substs h
+                simp_all
+              · simp_all
+            · congr
+              ext w
+              by_cases w = v <;> rename_i x
+              · substs h
+                simp_all
+              · simp_all
+        · have := ht₃ v
+          have := he₃ v
+          simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
+              Bool.not_eq_true', AList.lookup_insert]
+          obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
+          split <;> rename_i h'
+          · subst h'
+            simp_all
+          · simp_all? says simp_all only [ne_eq, hasNestedIf, Bool.or_self, hasConstantIf,
+              and_self, hasRedundantIf, Bool.or_false, beq_eq_false_iff_ne, not_false_eq_true,
+              disjoint, List.disjoint, Bool.and_true, Bool.and_eq_true, decide_eq_true_eq',
+              true_and]
+            constructor <;> assumption
+        · have := ht₃ w
+          have := he₃ w
+          by_cases w = v
+          · subst h; simp_all
+          · simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
+              Bool.not_eq_true', not_false_eq_true, AList.lookup_insert_ne]
+            obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
+            split at b <;> rename_i h'
+            · subst h'; simp_all
+            · simp_all only [ne_eq, vars, List.singleton_append, List.cons_append,
+                Bool.not_eq_true, List.mem_cons, List.mem_append, false_or]
+              cases b <;> simp_all⟩
+    | some b =>
+      have ⟨e', he'⟩ := normalize' l (.ite (lit b) t e)
+      ⟨e', by simp_all⟩
+  termination_by normalize' e => e.normSize'
+
+example : IfNormalization :=
+  ⟨fun e => (normalize' ∅ e).1,
+   fun e => ⟨(normalize' ∅ e).2.2.1, by simp [(normalize' ∅ e).2.1]⟩⟩
diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index 11db242cb6ec0..753ff78903ad4 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -342,6 +342,10 @@ theorem prod_insert_one [DecidableEq α] (h : f a = 1) : ∏ x in insert a s, f
 #align finset.prod_insert_one Finset.prod_insert_one
 #align finset.sum_insert_zero Finset.sum_insert_zero
 
+@[to_additive]
+theorem prod_insert_div {M : Type*} [CommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} :
+    (∏ x in insert a s, f x) / f a = ∏ x in s, f x := by simp [ha]
+
 @[to_additive (attr := simp)]
 theorem prod_singleton (f : α → β) (a : α) : ∏ x in singleton a, f x = f a :=
   Eq.trans fold_singleton <| mul_one _
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
index 501ec65e11821..7181855ce1ce4 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -587,6 +587,12 @@ theorem coe_mul_rpow (x y : ℝ≥0) (z : ℝ) : ((x : ℝ≥0∞) * y) ^ z = (x
   mul_rpow_of_ne_top coe_ne_top coe_ne_top z
 #align ennreal.coe_mul_rpow ENNReal.coe_mul_rpow
 
+theorem prod_coe_rpow {ι} (s : Finset ι) (f : ι → ℝ≥0) (r : ℝ) :
+    ∏ i in s, (f i : ℝ≥0∞) ^ r = ((∏ i in s, f i : ℝ≥0) : ℝ≥0∞) ^ r := by
+  induction s using Finset.induction
+  case empty => simp
+  case insert i s hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]
+
 theorem mul_rpow_of_ne_zero {x y : ℝ≥0∞} (hx : x ≠ 0) (hy : y ≠ 0) (z : ℝ) :
     (x * y) ^ z = x ^ z * y ^ z := by simp [*, mul_rpow_eq_ite]
 #align ennreal.mul_rpow_of_ne_zero ENNReal.mul_rpow_of_ne_zero
@@ -595,6 +601,21 @@ theorem mul_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x * y)
   simp [hz.not_lt, mul_rpow_eq_ite]
 #align ennreal.mul_rpow_of_nonneg ENNReal.mul_rpow_of_nonneg
 
+theorem prod_rpow_of_ne_top {ι} {s : Finset ι} {f : ι → ℝ≥0∞} (hf : ∀ i ∈ s, f i ≠ ∞) (r : ℝ) :
+    ∏ i in s, f i ^ r = (∏ i in s, f i) ^ r := by
+  induction s using Finset.induction
+  case empty => simp
+  case insert i s hi ih =>
+    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
+    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
+    apply prod_lt_top h2f |>.ne
+
+theorem prod_rpow_of_nonneg {ι} {s : Finset ι} {f : ι → ℝ≥0∞} {r : ℝ} (hr : 0 ≤ r) :
+    ∏ i in s, f i ^ r = (∏ i in s, f i) ^ r := by
+  induction s using Finset.induction
+  case empty => simp
+  case insert i s hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
+
 theorem inv_rpow (x : ℝ≥0∞) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹ := by
   rcases eq_or_ne y 0 with (rfl | hy); · simp only [rpow_zero, inv_one]
   replace hy := hy.lt_or_lt
diff --git a/Mathlib/Data/Finset/Option.lean b/Mathlib/Data/Finset/Option.lean
index 69f58fa332fdd..453a2483a5e66 100644
--- a/Mathlib/Data/Finset/Option.lean
+++ b/Mathlib/Data/Finset/Option.lean
@@ -75,6 +75,10 @@ theorem mem_insertNone {s : Finset α} : ∀ {o : Option α}, o ∈ insertNone s
 theorem some_mem_insertNone {s : Finset α} {a : α} : some a ∈ insertNone s ↔ a ∈ s := by simp
 #align finset.some_mem_insert_none Finset.some_mem_insertNone
 
+lemma none_mem_insertNone {s : Finset α} : none ∈ insertNone s := by simp
+
+lemma insertNone_nonempty {s : Finset α} : insertNone s |>.Nonempty := ⟨none, none_mem_insertNone⟩
+
 @[simp]
 theorem card_insertNone (s : Finset α) : s.insertNone.card = s.card + 1 := by simp [insertNone]
 #align finset.card_insert_none Finset.card_insertNone
diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
index 56036dccdb907..5da9e0349183a 100644
--- a/Mathlib/Data/Matrix/Basic.lean
+++ b/Mathlib/Data/Matrix/Basic.lean
@@ -459,6 +459,47 @@ theorem diagonal_smul [Monoid R] [AddMonoid α] [DistribMulAction R α] (r : R)
   simp [h]
 #align matrix.diagonal_smul Matrix.diagonal_smul
 
+@[simp]
+theorem diagonal_neg [DecidableEq n] [NegZeroClass α] (d : n → α) :
+    -diagonal d = diagonal fun i => -d i := by
+  ext i j
+  by_cases h : i = j <;>
+  simp [h]
+#align matrix.diagonal_neg Matrix.diagonal_neg
+
+@[simp]
+theorem diagonal_sub [SubNegZeroMonoid α] (d₁ d₂ : n → α) :
+    diagonal d₁ - diagonal d₂ = diagonal fun i => d₁ i - d₂ i := by
+  ext i j
+  by_cases h : i = j <;>
+  simp [h]
+
+instance [Zero α] [NatCast α] : NatCast (Matrix n n α) where
+  natCast m := diagonal fun _ => m
+
+@[norm_cast]
+theorem diagonal_natCast [Zero α] [NatCast α] (m : ℕ) : diagonal (fun _ : n => (m : α)) = m := rfl
+
+@[norm_cast]
+theorem diagonal_natCast' [Zero α] [NatCast α] (m : ℕ) : diagonal ((m : n → α)) = m := rfl
+
+-- See note [no_index around OfNat.ofNat]
+theorem diagonal_ofNat [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
+    diagonal (fun _ : n => no_index (OfNat.ofNat m : α)) = OfNat.ofNat m := rfl
+
+-- See note [no_index around OfNat.ofNat]
+theorem diagonal_ofNat' [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
+    diagonal (no_index (OfNat.ofNat m : n → α)) = OfNat.ofNat m := rfl
+
+instance [Zero α] [IntCast α] : IntCast (Matrix n n α) where
+  intCast m := diagonal fun _ => m
+
+@[norm_cast]
+theorem diagonal_intCast [Zero α] [IntCast α] (m : ℤ) : diagonal (fun _ : n => (m : α)) = m := rfl
+
+@[norm_cast]
+theorem diagonal_intCast' [Zero α] [IntCast α] (m : ℤ) : diagonal ((m : n → α)) = m := rfl
+
 variable (n α)
 
 /-- `Matrix.diagonal` as an `AddMonoidHom`. -/
@@ -539,6 +580,30 @@ theorem one_eq_pi_single {i j} : (1 : Matrix n n α) i j = Pi.single (f := fun _
 
 end One
 
+instance instAddMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (Matrix n n α) where
+  natCast_zero := show diagonal _ = _ by
+    rw [Nat.cast_zero, diagonal_zero]
+  natCast_succ n := show diagonal _ = diagonal _ + _ by
+    rw [Nat.cast_succ, ←diagonal_add, diagonal_one]
+
+instance instAddGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (Matrix n n α) where
+  intCast_ofNat n := show diagonal _ = diagonal _ by
+    rw [Int.cast_ofNat]
+  intCast_negSucc n := show diagonal _ = -(diagonal _) by
+    rw [Int.cast_negSucc, diagonal_neg]
+  __ := addGroup
+  __ := instAddMonoidWithOne
+
+instance instAddCommMonoidWithOne [AddCommMonoidWithOne α] :
+    AddCommMonoidWithOne (Matrix n n α) where
+  __ := addCommMonoid
+  __ := instAddMonoidWithOne
+
+instance instAddCommGroupWithOne [AddCommGroupWithOne α] :
+    AddCommGroupWithOne (Matrix n n α) where
+  __ := addCommGroup
+  __ := instAddGroupWithOne
+
 section Numeral
 
 set_option linter.deprecated false
@@ -910,12 +975,6 @@ theorem mul_apply' [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {
   rfl
 #align matrix.mul_apply' Matrix.mul_apply'
 
-@[simp]
-theorem diagonal_neg [DecidableEq n] [AddGroup α] (d : n → α) :
-    -diagonal d = diagonal fun i => -d i :=
-  ((diagonalAddMonoidHom n α).map_neg d).symm
-#align matrix.diagonal_neg Matrix.diagonal_neg
-
 theorem sum_apply [AddCommMonoid α] (i : m) (j : n) (s : Finset β) (g : β → Matrix m n α) :
     (∑ c in s, g c) i j = ∑ c in s, g c i j :=
   (congr_fun (s.sum_apply i g) j).trans (s.sum_apply j _)
@@ -1077,18 +1136,10 @@ protected theorem mul_one [Fintype n] [DecidableEq n] (M : Matrix m n α) :
 #align matrix.mul_one Matrix.mul_one
 
 instance nonAssocSemiring [Fintype n] [DecidableEq n] : NonAssocSemiring (Matrix n n α) :=
-  { Matrix.nonUnitalNonAssocSemiring with
+  { Matrix.nonUnitalNonAssocSemiring, Matrix.instAddCommMonoidWithOne with
     one := 1
     one_mul := Matrix.one_mul
-    mul_one := Matrix.mul_one
-    natCast := fun n => diagonal fun _ => n
-    natCast_zero := by
-      ext
-      simp [Nat.cast]
-    natCast_succ := fun n => by
-      ext i j
-      by_cases i = j <;>
-      simp [Nat.cast, *]}
+    mul_one := Matrix.mul_one }
 
 @[simp]
 theorem map_mul [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β]
@@ -1171,11 +1222,11 @@ instance instNonUnitalRing [Fintype n] [NonUnitalRing α] : NonUnitalRing (Matri
 
 instance instNonAssocRing [Fintype n] [DecidableEq n] [NonAssocRing α] :
     NonAssocRing (Matrix n n α) :=
-  { Matrix.nonAssocSemiring, Matrix.addCommGroup with }
+  { Matrix.nonAssocSemiring, Matrix.instAddCommGroupWithOne with }
 #align matrix.non_assoc_ring Matrix.instNonAssocRing
 
 instance instRing [Fintype n] [DecidableEq n] [Ring α] : Ring (Matrix n n α) :=
-  { Matrix.semiring, Matrix.addCommGroup with }
+  { Matrix.semiring, Matrix.instAddCommGroupWithOne with }
 #align matrix.ring Matrix.instRing
 
 section Semiring
diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
index c018b986246e2..b5a9582183f7b 100644
--- a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
+++ b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
@@ -24,6 +24,12 @@ and `α → (E)NNReal` functions in two cases,
 * `ENNReal.lintegral_mul_le_Lp_mul_Lq` : ℝ≥0∞ functions,
 * `NNReal.lintegral_mul_le_Lp_mul_Lq`  : ℝ≥0 functions.
 
+`ENNReal.lintegral_mul_norm_pow_le` is a variant where the exponents are not reciprocals:
+`∫ (f ^ p * g ^ q) ∂μ ≤ (∫ f ∂μ) ^ p * (∫ g ∂μ) ^ q` where `p, q ≥ 0` and `p + q = 1`.
+`ENNReal.lintegral_prod_norm_pow_le` generalizes this to a finite family of functions:
+`∫ (∏ i, f i ^ p i) ∂μ ≤ ∏ i, (∫ f i ∂μ) ^ p i` when the `p` is a collection
+of nonnegative weights with sum 1.
+
 Minkowski's inequality for the Lebesgue integral of measurable functions with `ℝ≥0∞` values:
 we prove `(∫ (f + g)^p ∂μ) ^ (1/p) ≤ (∫ f^p ∂μ) ^ (1/p) + (∫ g^p ∂μ) ^ (1/p)` for `1 ≤ p`.
 -/
@@ -48,7 +54,7 @@ only to prove the more general results:
 
 noncomputable section
 
-open Classical BigOperators NNReal ENNReal MeasureTheory
+open Classical BigOperators NNReal ENNReal MeasureTheory Finset
 
 set_option linter.uppercaseLean3 false
 
@@ -175,6 +181,101 @@ theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.IsConj
   exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero
 #align ennreal.lintegral_mul_le_Lp_mul_Lq ENNReal.lintegral_mul_le_Lp_mul_Lq
 
+/-- A different formulation of Hölder's inequality for two functions, with two exponents that sum to
+1, instead of reciprocals of  -/
+theorem lintegral_mul_norm_pow_le {α} [MeasurableSpace α] {μ : Measure α}
+    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) :
+    ∫⁻ a, f a ^ p * g a ^ q ∂μ ≤ (∫⁻ a, f a ∂μ) ^ p * (∫⁻ a, g a ∂μ) ^ q := by
+  rcases hp.eq_or_lt with rfl|hp
+  · rw [zero_add] at hpq
+    simp [hpq]
+  rcases hq.eq_or_lt with rfl|hq
+  · rw [add_zero] at hpq
+    simp [hpq]
+  have h2p : 1 < 1 / p := by
+    rw [one_div]
+    apply one_lt_inv hp
+    linarith
+  have h2pq : 1 / (1 / p) + 1 / (1 / q) = 1 := by
+    simp [hp.ne', hq.ne', hpq]
+  have := ENNReal.lintegral_mul_le_Lp_mul_Lq μ ⟨h2p, h2pq⟩ (hf.pow_const p) (hg.pow_const q)
+  simpa [← ENNReal.rpow_mul, hp.ne', hq.ne'] using this
+
+/-- A version of Hölder with multiple arguments -/
+theorem lintegral_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
+    (s : Finset ι) {f : ι → α → ℝ≥0∞} (hf : ∀ i ∈ s, AEMeasurable (f i) μ)
+    {p : ι → ℝ} (hp : ∑ i in s, p i = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) :
+    ∫⁻ a, ∏ i in s, f i a ^ p i ∂μ ≤ ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+  induction s using Finset.induction generalizing p
+  case empty =>
+    simp at hp
+  case insert i₀ s hi₀ ih =>
+    rcases eq_or_ne (p i₀) 1 with h2i₀|h2i₀
+    · simp [hi₀]
+      have h2p : ∀ i ∈ s, p i = 0 := by
+        simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
+          using hp
+      calc ∫⁻ a, f i₀ a ^ p i₀ * ∏ i in s, f i a ^ p i ∂μ
+          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i in s, 1 ∂μ := by
+            congr! 3 with x
+            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
+        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i in s, 1 := by simp [h2i₀]
+        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+            congr 1
+            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
+    · have hpi₀ : 0 ≤ 1 - p i₀ := by
+        simp_rw [sub_nonneg, ← hp, single_le_sum h2p (mem_insert_self ..)]
+      have h2pi₀ : 1 - p i₀ ≠ 0 := by
+        rwa [sub_ne_zero, ne_comm]
+      let q := fun i ↦ p i / (1 - p i₀)
+      have hq : ∑ i in s, q i = 1 := by
+        rw [← Finset.sum_div, ← sum_insert_sub hi₀, hp, div_self h2pi₀]
+      have h2q : ∀ i ∈ s, 0 ≤ q i :=
+        fun i hi ↦ div_nonneg (h2p i <| mem_insert_of_mem hi) hpi₀
+      calc ∫⁻ a, ∏ i in insert i₀ s, f i a ^ p i ∂μ
+          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i in s, f i a ^ p i ∂μ := by simp [hi₀]
+        _ = ∫⁻ a, f i₀ a ^ p i₀ * (∏ i in s, f i a ^ q i) ^ (1 - p i₀) ∂μ := by
+            simp [← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
+              div_mul_cancel (h := h2pi₀)]
+        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∫⁻ a, ∏ i in s, f i a ^ q i ∂μ) ^ (1 - p i₀) := by
+            apply ENNReal.lintegral_mul_norm_pow_le
+            · exact hf i₀ <| mem_insert_self ..
+            · exact s.aemeasurable_prod <| fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _
+            · exact h2p i₀ <| mem_insert_self ..
+            · exact hpi₀
+            · apply add_sub_cancel'_right
+        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∏ i in s, (∫⁻ a, f i a ∂μ) ^ q i) ^ (1 - p i₀) := by
+            gcongr -- behavior of gcongr is heartbeat-dependent, which makes code really fragile...
+            exact ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q
+        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+            simp [← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
+              div_mul_cancel (h := h2pi₀)]
+        _ = ∏ i in insert i₀ s, (∫⁻ a, f i a ∂μ) ^ p i := by simp [hi₀]
+
+/-- A version of Hölder with multiple arguments, one of which plays a distinguished role. -/
+theorem lintegral_mul_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
+    (s : Finset ι) {g : α →  ℝ≥0∞} {f : ι → α → ℝ≥0∞} (hg : AEMeasurable g μ)
+    (hf : ∀ i ∈ s, AEMeasurable (f i) μ) (q : ℝ) {p : ι → ℝ} (hpq : q + ∑ i in s, p i = 1)
+    (hq :  0 ≤ q) (hp : ∀ i ∈ s, 0 ≤ p i) :
+    ∫⁻ a, g a ^ q * ∏ i in s, f i a ^ p i ∂μ ≤
+      (∫⁻ a, g a ∂μ) ^ q * ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+  suffices
+    ∫⁻ t, ∏ j in insertNone s, Option.elim j (g t) (fun j ↦ f j t) ^ Option.elim j q p ∂μ
+    ≤ ∏ j in insertNone s, (∫⁻ t, Option.elim j (g t) (fun j ↦ f j t) ∂μ) ^ Option.elim j q p by
+    simpa using this
+  refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
+  · rintro (_|i) hi
+    · exact hg
+    · refine hf i ?_
+      simpa using hi
+  · simp_rw [sum_insertNone, Option.elim]
+    exact hpq
+  · rintro (_|i) hi
+    · exact hq
+    · refine hp i ?_
+      simpa using hi
+
 theorem lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {p : ℝ} {f g : α → ℝ≥0∞}
     (hf : AEMeasurable f μ) (hf_top : (∫⁻ a, f a ^ p ∂μ) < ⊤) (hg_top : (∫⁻ a, g a ^ p ∂μ) < ⊤)
     (hp1 : 1 ≤ p) : (∫⁻ a, (f + g) a ^ p ∂μ) < ⊤ := by
diff --git a/Mathlib/Tactic/Peel.lean b/Mathlib/Tactic/Peel.lean
index e050247f54099..717fa7fcb05cc 100644
--- a/Mathlib/Tactic/Peel.lean
+++ b/Mathlib/Tactic/Peel.lean
@@ -207,6 +207,7 @@ def peelIffAux : TacticM Unit := do
           | apply exists_congr
           | apply eventually_congr
           | apply frequently_congr
+          | apply and_congr_right
           | fail "failed to apply a quantifier congruence lemma."))
 
 /-- Peel off quantifiers from an `↔` and assign the names given in `l` to the introduced
diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean
index e61e05c1d1142..528b51b7cb0ed 100644
--- a/Mathlib/Topology/EMetricSpace/Basic.lean
+++ b/Mathlib/Topology/EMetricSpace/Basic.lean
@@ -852,9 +852,9 @@ open TopologicalSpace
 
 variable (α)
 
-/-- A sigma compact pseudo emetric space has second countable topology. This is not an instance
-to avoid a loop with `sigmaCompactSpace_of_locally_compact_second_countable`.  -/
-theorem secondCountable_of_sigmaCompact [SigmaCompactSpace α] : SecondCountableTopology α := by
+/-- A sigma compact pseudo emetric space has second countable topology. -/
+instance (priority := 90) secondCountable_of_sigmaCompact [SigmaCompactSpace α] :
+    SecondCountableTopology α := by
   suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
   choose T _ hTc hsubT using fun n =>
     subset_countable_closure_of_compact (isCompact_compactCovering α n)
diff --git a/Mathlib/Topology/Metrizable/Urysohn.lean b/Mathlib/Topology/Metrizable/Urysohn.lean
index 49c6c06e2e9ec..e80219edb5447 100644
--- a/Mathlib/Topology/Metrizable/Urysohn.lean
+++ b/Mathlib/Topology/Metrizable/Urysohn.lean
@@ -109,7 +109,8 @@ theorem exists_inducing_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Inducing f := by
 /-- *Urysohn's metrization theorem* (Tychonoff's version):
 a regular topological space with second countable topology `X` is metrizable,
 i.e., there exists a pseudometric space structure that generates the same topology. -/
-lemma PseudoMetrizableSpace.of_regularSpace_secondCountableTopology : PseudoMetrizableSpace X :=
+instance (priority := 90) PseudoMetrizableSpace.of_regularSpace_secondCountableTopology :
+    PseudoMetrizableSpace X :=
   let ⟨_, hf⟩ := exists_inducing_l_infty X
   hf.pseudoMetrizableSpace
 
@@ -124,8 +125,7 @@ theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f :=
 /-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second
 countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the
 same topology. -/
-theorem metrizableSpace_of_t3_second_countable : MetrizableSpace X :=
+instance (priority := 90) metrizableSpace_of_t3_second_countable : MetrizableSpace X :=
   let ⟨_, hf⟩ := exists_embedding_l_infty X
   hf.metrizableSpace
 #align topological_space.metrizable_space_of_t3_second_countable TopologicalSpace.metrizableSpace_of_t3_second_countable
-
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index d5116154d14a0..6b153484e8bc6 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1731,8 +1731,8 @@ section ClosableCompactSubsetOpenSpace
 
 /-- A class of topological spaces in which, given a compact set included inside an open set, then
 the closure of the compact set is also included in the open set.
-Satisfied notably for T2 spaces and regular spaces, and useful
-when discussing classes of regular measures. -/
+Satisfied notably for T2 spaces and regular spaces, and useful when discussing classes of
+regular measures. Equivalent to regularity among locally compact spaces. -/
 class ClosableCompactSubsetOpenSpace (X : Type*) [TopologicalSpace X] : Prop :=
   closure_subset_of_isOpen : ∀ (K U : Set X), IsCompact K → IsOpen U → K ⊆ U → closure K ⊆ U
 
@@ -1741,12 +1741,12 @@ theorem IsCompact.closure_subset_of_isOpen [ClosableCompactSubsetOpenSpace X]
     closure s ⊆ u :=
   ClosableCompactSubsetOpenSpace.closure_subset_of_isOpen s u hs hu h
 
-instance [T2Space X] : ClosableCompactSubsetOpenSpace X :=
+instance (priority := 150) [T2Space X] : ClosableCompactSubsetOpenSpace X :=
   ⟨fun K _U K_comp _U_open KU ↦ by rwa [K_comp.isClosed.closure_eq]⟩
 
 /-- In a (possibly non-Hausdorff) regular space, if a compact set `s` is contained in an
 open set `u`, then its closure is also contained in `u`. -/
-instance [RegularSpace X] : ClosableCompactSubsetOpenSpace X := by
+instance (priority := 150) [RegularSpace X] : ClosableCompactSubsetOpenSpace X := by
   refine ⟨fun s u hs hu h ↦ ?_⟩
   obtain ⟨F, sF, F_closed, Fu⟩ : ∃ F, s ⊆ F ∧ IsClosed F ∧ F ⊆ u := by
     apply hs.induction_on (p := fun t ↦ ∃ F, t ⊆ F ∧ IsClosed F ∧ F ⊆ u)
@@ -1779,6 +1779,16 @@ theorem exists_compact_closed_between [LocallyCompactSpace X] [ClosableCompactSu
   · apply M_comp.closure_subset_of_isOpen hU
     exact ML.trans (interior_subset.trans LU)
 
+/-- A locally compact space with the `ClosableCompactSubsetOpenSpace` is `Regular`. -/
+instance (priority := 80) [LocallyCompactSpace X] [ClosableCompactSubsetOpenSpace X] :
+    RegularSpace X := by
+  apply RegularSpace.ofExistsMemNhdsIsClosedSubset (fun x s hx ↦ ?_)
+  rcases _root_.mem_nhds_iff.1 hx with ⟨u, us, u_open, xu⟩
+  rcases exists_compact_closed_between (isCompact_singleton (a := x)) u_open (by simpa using xu)
+    with ⟨t, -, t_closed, xt, tu⟩
+  have : interior t ∈ 𝓝 x := isOpen_interior.mem_nhds (by simpa using xt)
+  exact ⟨t, interior_mem_nhds.mp this, t_closed, tu.trans us⟩
+
 protected theorem IsCompact.closure [WeaklyLocallyCompactSpace X] [ClosableCompactSubsetOpenSpace X]
     {K : Set X} (hK : IsCompact K) : IsCompact (closure K) := by
   rcases exists_compact_superset hK with ⟨L, L_comp, hL⟩
diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean
index 85088d3fa9759..24ac35cef721e 100644
--- a/Mathlib/Topology/UrysohnsLemma.lean
+++ b/Mathlib/Topology/UrysohnsLemma.lean
@@ -20,6 +20,14 @@ closed sets `s` and `t` in a normal topological space `X` there exists a continu
 * `f` equals one on `t`;
 * `0 ≤ f x ≤ 1` for all `x`.
 
+We also give versions in a regular locally compact space where one assumes that `s` is compact
+and `t` is closed, in `exists_continuous_zero_one_of_isCompact`
+and `exists_continuous_one_zero_of_isCompact` (the latter providing additionally a function with
+compact support).
+
+We write a generic proof so that it applies both to normal spaces and to regular locally
+compact spaces.
+
 ## Implementation notes
 
 Most paper sources prove Urysohn's lemma using a family of open sets indexed by dyadic rational
@@ -28,10 +36,10 @@ needs to formalize the "dyadic induction", then prove that the resulting family
 monotone). So, we formalize a slightly different proof.
 
 Let `Urysohns.CU` be the type of pairs `(C, U)` of a closed set `C` and an open set `U` such that
-`C ⊆ U`. Since `X` is a normal topological space, for each `c : CU X` there exists an open set `u`
+`C ⊆ U`. Since `X` is a normal topological space, for each `c : CU` there exists an open set `u`
 such that `c.C ⊆ u ∧ closure u ⊆ c.U`. We define `c.left` and `c.right` to be `(c.C, u)` and
 `(closure u, c.U)`, respectively. Then we define a family of functions
-`Urysohns.CU.approx (c : Urysohns.CU X) (n : ℕ) : X → ℝ` by recursion on `n`:
+`Urysohns.CU.approx (c : Urysohns.CU) (n : ℕ) : X → ℝ` by recursion on `n`:
 
 * `c.approx 0` is the indicator of `c.Uᶜ`;
 * `c.approx (n + 1) x = (c.left.approx n x + c.right.approx n x) / 2`.
@@ -66,76 +74,88 @@ lemmas about `midpoint`.
 
 ## Tags
 
-Urysohn's lemma, normal topological space
+Urysohn's lemma, normal topological space, locally compact topological space
 -/
 
 
 variable {X : Type*} [TopologicalSpace X]
 
 open Set Filter TopologicalSpace Topology Filter
+open scoped Pointwise
 
 namespace Urysohns
 
 set_option linter.uppercaseLean3 false
 
 /-- An auxiliary type for the proof of Urysohn's lemma: a pair of a closed set `C` and its
-open neighborhood `U`. -/
-structure CU (X : Type*) [TopologicalSpace X] where
-  protected (C U : Set X)
+open neighborhood `U`, together with the assumption that `C` satisfies the property `P C`. The
+latter assumption will make it possible to prove simultaneously both versions of Urysohn's lemma,
+in normal spaces (with `P` always true) and in locally compact spaces (with `P = IsCompact`).
+We put also in the structure the assumption that, for any such pair, one may find an intermediate
+pair inbetween satisfying `P`, to avoid carrying it around in the argument. -/
+structure CU {X : Type*} [TopologicalSpace X] (P : Set X → Prop) where
+  /-- The inner set in the inductive construction towards Urysohn's lemma -/
+  protected C : Set X
+  /-- The outer set in the inductive construction towards Urysohn's lemma -/
+  protected U : Set X
+  protected P_C : P C
   protected closed_C : IsClosed C
   protected open_U : IsOpen U
   protected subset : C ⊆ U
+  protected hP : ∀ {c u : Set X}, IsClosed c → P c → IsOpen u → c ⊆ u →
+    ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)
 #align urysohns.CU Urysohns.CU
 
-instance : Inhabited (CU X) :=
-  ⟨⟨∅, univ, isClosed_empty, isOpen_univ, empty_subset _⟩⟩
-
-variable [NormalSpace X]
-
 namespace CU
 
-/-- Due to `normal_exists_closure_subset`, for each `c : CU X` there exists an open set `u`
+variable {P : Set X → Prop}
+
+/-- By assumption, for each `c : CU P` there exists an open set `u`
 such that `c.C ⊆ u` and `closure u ⊆ c.U`. `c.left` is the pair `(c.C, u)`. -/
 @[simps C]
-def left (c : CU X) : CU X where
+def left (c : CU P) : CU P where
   C := c.C
-  U := (normal_exists_closure_subset c.closed_C c.open_U c.subset).choose
+  U := (c.hP c.closed_C c.P_C c.open_U c.subset).choose
   closed_C := c.closed_C
-  open_U := (normal_exists_closure_subset c.closed_C c.open_U c.subset).choose_spec.1
-  subset := (normal_exists_closure_subset c.closed_C c.open_U c.subset).choose_spec.2.1
+  P_C := c.P_C
+  open_U := (c.hP c.closed_C c.P_C c.open_U c.subset).choose_spec.1
+  subset := (c.hP c.closed_C c.P_C c.open_U c.subset).choose_spec.2.1
+  hP := c.hP
 #align urysohns.CU.left Urysohns.CU.left
 
-/-- Due to `normal_exists_closure_subset`, for each `c : CU X` there exists an open set `u`
+/-- By assumption, for each `c : CU P` there exists an open set `u`
 such that `c.C ⊆ u` and `closure u ⊆ c.U`. `c.right` is the pair `(closure u, c.U)`. -/
 @[simps U]
-def right (c : CU X) : CU X where
-  C := closure (normal_exists_closure_subset c.closed_C c.open_U c.subset).choose
+def right (c : CU P) : CU P where
+  C := closure (c.hP c.closed_C c.P_C c.open_U c.subset).choose
   U := c.U
   closed_C := isClosed_closure
+  P_C := (c.hP c.closed_C c.P_C c.open_U c.subset).choose_spec.2.2.2
   open_U := c.open_U
-  subset := (normal_exists_closure_subset c.closed_C c.open_U c.subset).choose_spec.2.2
+  subset := (c.hP c.closed_C c.P_C c.open_U c.subset).choose_spec.2.2.1
+  hP := c.hP
 #align urysohns.CU.right Urysohns.CU.right
 
-theorem left_U_subset_right_C (c : CU X) : c.left.U ⊆ c.right.C :=
+theorem left_U_subset_right_C (c : CU P) : c.left.U ⊆ c.right.C :=
   subset_closure
 #align urysohns.CU.left_U_subset_right_C Urysohns.CU.left_U_subset_right_C
 
-theorem left_U_subset (c : CU X) : c.left.U ⊆ c.U :=
+theorem left_U_subset (c : CU P) : c.left.U ⊆ c.U :=
   Subset.trans c.left_U_subset_right_C c.right.subset
 #align urysohns.CU.left_U_subset Urysohns.CU.left_U_subset
 
-theorem subset_right_C (c : CU X) : c.C ⊆ c.right.C :=
+theorem subset_right_C (c : CU P) : c.C ⊆ c.right.C :=
   Subset.trans c.left.subset c.left_U_subset_right_C
 #align urysohns.CU.subset_right_C Urysohns.CU.subset_right_C
 
 /-- `n`-th approximation to a continuous function `f : X → ℝ` such that `f = 0` on `c.C` and `f = 1`
 outside of `c.U`. -/
-noncomputable def approx : ℕ → CU X → X → ℝ
+noncomputable def approx : ℕ → CU P → X → ℝ
   | 0, c, x => indicator c.Uᶜ 1 x
   | n + 1, c, x => midpoint ℝ (approx n c.left x) (approx n c.right x)
 #align urysohns.CU.approx Urysohns.CU.approx
 
-theorem approx_of_mem_C (c : CU X) (n : ℕ) {x : X} (hx : x ∈ c.C) : c.approx n x = 0 := by
+theorem approx_of_mem_C (c : CU P) (n : ℕ) {x : X} (hx : x ∈ c.C) : c.approx n x = 0 := by
   induction' n with n ihn generalizing c
   · exact indicator_of_not_mem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
   · simp only [approx]
@@ -143,7 +163,7 @@ theorem approx_of_mem_C (c : CU X) (n : ℕ) {x : X} (hx : x ∈ c.C) : c.approx
     exacts [c.subset_right_C hx, hx]
 #align urysohns.CU.approx_of_mem_C Urysohns.CU.approx_of_mem_C
 
-theorem approx_of_nmem_U (c : CU X) (n : ℕ) {x : X} (hx : x ∉ c.U) : c.approx n x = 1 := by
+theorem approx_of_nmem_U (c : CU P) (n : ℕ) {x : X} (hx : x ∉ c.U) : c.approx n x = 1 := by
   induction' n with n ihn generalizing c
   · rw [← mem_compl_iff] at hx
     exact indicator_of_mem hx _
@@ -152,14 +172,14 @@ theorem approx_of_nmem_U (c : CU X) (n : ℕ) {x : X} (hx : x ∉ c.U) : c.appro
     exacts [hx, fun hU => hx <| c.left_U_subset hU]
 #align urysohns.CU.approx_of_nmem_U Urysohns.CU.approx_of_nmem_U
 
-theorem approx_nonneg (c : CU X) (n : ℕ) (x : X) : 0 ≤ c.approx n x := by
+theorem approx_nonneg (c : CU P) (n : ℕ) (x : X) : 0 ≤ c.approx n x := by
   induction' n with n ihn generalizing c
   · exact indicator_nonneg (fun _ _ => zero_le_one) _
   · simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]
     refine' mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg _ _) <;> apply ihn
 #align urysohns.CU.approx_nonneg Urysohns.CU.approx_nonneg
 
-theorem approx_le_one (c : CU X) (n : ℕ) (x : X) : c.approx n x ≤ 1 := by
+theorem approx_le_one (c : CU P) (n : ℕ) (x : X) : c.approx n x ≤ 1 := by
   induction' n with n ihn generalizing c
   · exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
   · simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
@@ -168,11 +188,11 @@ theorem approx_le_one (c : CU X) (n : ℕ) (x : X) : c.approx n x ≤ 1 := by
     exact Iff.mpr (div_le_one zero_lt_two) this
 #align urysohns.CU.approx_le_one Urysohns.CU.approx_le_one
 
-theorem bddAbove_range_approx (c : CU X) (x : X) : BddAbove (range fun n => c.approx n x) :=
+theorem bddAbove_range_approx (c : CU P) (x : X) : BddAbove (range fun n => c.approx n x) :=
   ⟨1, fun _ ⟨n, hn⟩ => hn ▸ c.approx_le_one n x⟩
 #align urysohns.CU.bdd_above_range_approx Urysohns.CU.bddAbove_range_approx
 
-theorem approx_le_approx_of_U_sub_C {c₁ c₂ : CU X} (h : c₁.U ⊆ c₂.C) (n₁ n₂ : ℕ) (x : X) :
+theorem approx_le_approx_of_U_sub_C {c₁ c₂ : CU P} (h : c₁.U ⊆ c₂.C) (n₁ n₂ : ℕ) (x : X) :
     c₂.approx n₂ x ≤ c₁.approx n₁ x := by
   by_cases hx : x ∈ c₁.U
   · calc
@@ -183,7 +203,7 @@ theorem approx_le_approx_of_U_sub_C {c₁ c₂ : CU X} (h : c₁.U ⊆ c₂.C) (
       _ = approx n₁ c₁ x := (approx_of_nmem_U _ _ hx).symm
 #align urysohns.CU.approx_le_approx_of_U_sub_C Urysohns.CU.approx_le_approx_of_U_sub_C
 
-theorem approx_mem_Icc_right_left (c : CU X) (n : ℕ) (x : X) :
+theorem approx_mem_Icc_right_left (c : CU P) (n : ℕ) (x : X) :
     c.approx n x ∈ Icc (c.right.approx n x) (c.left.approx n x) := by
   induction' n with n ihn generalizing c
   · exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset)
@@ -194,7 +214,7 @@ theorem approx_mem_Icc_right_left (c : CU X) (n : ℕ) (x : X) :
     exacts [subset_closure, subset_closure]
 #align urysohns.CU.approx_mem_Icc_right_left Urysohns.CU.approx_mem_Icc_right_left
 
-theorem approx_le_succ (c : CU X) (n : ℕ) (x : X) : c.approx n x ≤ c.approx (n + 1) x := by
+theorem approx_le_succ (c : CU P) (n : ℕ) (x : X) : c.approx n x ≤ c.approx (n + 1) x := by
   induction' n with n ihn generalizing c
   · simp only [approx, right_U, right_le_midpoint]
     exact (approx_mem_Icc_right_left c 0 x).2
@@ -202,7 +222,7 @@ theorem approx_le_succ (c : CU X) (n : ℕ) (x : X) : c.approx n x ≤ c.approx
     exact midpoint_le_midpoint (ihn _) (ihn _)
 #align urysohns.CU.approx_le_succ Urysohns.CU.approx_le_succ
 
-theorem approx_mono (c : CU X) (x : X) : Monotone fun n => c.approx n x :=
+theorem approx_mono (c : CU P) (x : X) : Monotone fun n => c.approx n x :=
   monotone_nat_of_le_succ fun n => c.approx_le_succ n x
 #align urysohns.CU.approx_mono Urysohns.CU.approx_mono
 
@@ -211,48 +231,48 @@ theorem approx_mono (c : CU X) (x : X) : Monotone fun n => c.approx n x :=
 * `0 ≤ f x ≤ 1` for all `x`;
 * `f` equals zero on `c.C` and equals one outside of `c.U`;
 -/
-protected noncomputable def lim (c : CU X) (x : X) : ℝ :=
+protected noncomputable def lim (c : CU P) (x : X) : ℝ :=
   ⨆ n, c.approx n x
 #align urysohns.CU.lim Urysohns.CU.lim
 
-theorem tendsto_approx_atTop (c : CU X) (x : X) :
+theorem tendsto_approx_atTop (c : CU P) (x : X) :
     Tendsto (fun n => c.approx n x) atTop (𝓝 <| c.lim x) :=
   tendsto_atTop_ciSup (c.approx_mono x) ⟨1, fun _ ⟨_, hn⟩ => hn ▸ c.approx_le_one _ _⟩
 #align urysohns.CU.tendsto_approx_at_top Urysohns.CU.tendsto_approx_atTop
 
-theorem lim_of_mem_C (c : CU X) (x : X) (h : x ∈ c.C) : c.lim x = 0 := by
+theorem lim_of_mem_C (c : CU P) (x : X) (h : x ∈ c.C) : c.lim x = 0 := by
   simp only [CU.lim, approx_of_mem_C, h, ciSup_const]
 #align urysohns.CU.lim_of_mem_C Urysohns.CU.lim_of_mem_C
 
-theorem lim_of_nmem_U (c : CU X) (x : X) (h : x ∉ c.U) : c.lim x = 1 := by
+theorem lim_of_nmem_U (c : CU P) (x : X) (h : x ∉ c.U) : c.lim x = 1 := by
   simp only [CU.lim, approx_of_nmem_U c _ h, ciSup_const]
 #align urysohns.CU.lim_of_nmem_U Urysohns.CU.lim_of_nmem_U
 
-theorem lim_eq_midpoint (c : CU X) (x : X) :
+theorem lim_eq_midpoint (c : CU P) (x : X) :
     c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x) := by
   refine' tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 _)
   simp only [approx]
   exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)
 #align urysohns.CU.lim_eq_midpoint Urysohns.CU.lim_eq_midpoint
 
-theorem approx_le_lim (c : CU X) (x : X) (n : ℕ) : c.approx n x ≤ c.lim x :=
+theorem approx_le_lim (c : CU P) (x : X) (n : ℕ) : c.approx n x ≤ c.lim x :=
   le_ciSup (c.bddAbove_range_approx x) _
 #align urysohns.CU.approx_le_lim Urysohns.CU.approx_le_lim
 
-theorem lim_nonneg (c : CU X) (x : X) : 0 ≤ c.lim x :=
+theorem lim_nonneg (c : CU P) (x : X) : 0 ≤ c.lim x :=
   (c.approx_nonneg 0 x).trans (c.approx_le_lim x 0)
 #align urysohns.CU.lim_nonneg Urysohns.CU.lim_nonneg
 
-theorem lim_le_one (c : CU X) (x : X) : c.lim x ≤ 1 :=
+theorem lim_le_one (c : CU P) (x : X) : c.lim x ≤ 1 :=
   ciSup_le fun _ => c.approx_le_one _ _
 #align urysohns.CU.lim_le_one Urysohns.CU.lim_le_one
 
-theorem lim_mem_Icc (c : CU X) (x : X) : c.lim x ∈ Icc (0 : ℝ) 1 :=
+theorem lim_mem_Icc (c : CU P) (x : X) : c.lim x ∈ Icc (0 : ℝ) 1 :=
   ⟨c.lim_nonneg x, c.lim_le_one x⟩
 #align urysohns.CU.lim_mem_Icc Urysohns.CU.lim_mem_Icc
 
 /-- Continuity of `Urysohns.CU.lim`. See module docstring for a sketch of the proofs. -/
-theorem continuous_lim (c : CU X) : Continuous c.lim := by
+theorem continuous_lim (c : CU P) : Continuous c.lim := by
   obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
   refine'
     continuous_iff_continuousAt.2 fun x =>
@@ -293,8 +313,6 @@ end CU
 
 end Urysohns
 
-variable [NormalSpace X]
-
 /-- Urysohn's lemma: if `s` and `t` are two disjoint closed sets in a normal topological space `X`,
 then there exists a continuous function `f : X → ℝ` such that
 
@@ -302,10 +320,80 @@ then there exists a continuous function `f : X → ℝ` such that
 * `f` equals one on `t`;
 * `0 ≤ f x ≤ 1` for all `x`.
 -/
-theorem exists_continuous_zero_one_of_closed {s t : Set X} (hs : IsClosed s) (ht : IsClosed t)
+theorem exists_continuous_zero_one_of_closed [NormalSpace X]
+    {s t : Set X} (hs : IsClosed s) (ht : IsClosed t)
     (hd : Disjoint s t) : ∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
   -- The actual proof is in the code above. Here we just repack it into the expected format.
-  set c : Urysohns.CU X := ⟨s, tᶜ, hs, ht.isOpen_compl, disjoint_left.1 hd⟩
+  let P : Set X → Prop := fun _ ↦ True
+  set c : Urysohns.CU P :=
+  { C := s
+    U := tᶜ
+    P_C := trivial
+    closed_C := hs
+    open_U := ht.isOpen_compl
+    subset := disjoint_left.1 hd
+    hP := by
+      rintro c u c_closed - u_open cu
+      rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
+      exact ⟨v, v_open, cv, hv, trivial⟩ }
   exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_nmem_U _ fun h => h hx,
     c.lim_mem_Icc⟩
 #align exists_continuous_zero_one_of_closed exists_continuous_zero_one_of_closed
+
+/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
+space `X`, with `s` compact and `t` closed, then there exists a continuous
+function `f : X → ℝ` such that
+
+* `f` equals zero on `s`;
+* `f` equals one on `t`;
+* `0 ≤ f x ≤ 1` for all `x`.
+-/
+theorem exists_continuous_zero_one_of_isCompact [RegularSpace X] [LocallyCompactSpace X]
+    {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
+    ∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
+  obtain ⟨k, k_comp, k_closed, sk, kt⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ s ⊆ interior k ∧ k ⊆ tᶜ :=
+    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
+  let P : Set X → Prop := IsCompact
+  set c : Urysohns.CU P :=
+  { C := k
+    U := tᶜ
+    P_C := k_comp
+    closed_C := k_closed
+    open_U := ht.isOpen_compl
+    subset := kt
+    hP := by
+      rintro c u - c_comp u_open cu
+      rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩
+      have A : closure (interior k) ⊆ k :=
+        (IsClosed.closure_subset_iff k_closed).2 interior_subset
+      refine ⟨interior k, isOpen_interior, ck, A.trans ku,
+        k_comp.of_isClosed_subset isClosed_closure A⟩ }
+  exact ⟨⟨c.lim, c.continuous_lim⟩, fun x hx ↦ c.lim_of_mem_C _ (sk.trans interior_subset hx),
+    fun x hx => c.lim_of_nmem_U _ fun h => h hx, c.lim_mem_Icc⟩
+
+/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
+space `X`, with `s` compact and `t` closed, then there exists a continuous compactly supported
+function `f : X → ℝ` such that
+
+* `f` equals one on `s`;
+* `f` equals zero on `t`;
+* `0 ≤ f x ≤ 1` for all `x`.
+-/
+theorem exists_continuous_one_zero_of_isCompact [RegularSpace X] [LocallyCompactSpace X]
+    {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
+    ∃ f : C(X, ℝ), EqOn f 1 s ∧ EqOn f 0 t ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
+  obtain ⟨k, k_comp, k_closed, sk, kt⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ s ⊆ interior k ∧ k ⊆ tᶜ :=
+    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
+  rcases exists_continuous_zero_one_of_isCompact hs isOpen_interior.isClosed_compl
+    (disjoint_compl_right_iff_subset.mpr sk) with ⟨⟨f, hf⟩, hfs, hft, h'f⟩
+  have A : t ⊆ (interior k)ᶜ := subset_compl_comm.mpr (interior_subset.trans kt)
+  refine ⟨⟨fun x ↦ 1 - f x, continuous_const.sub hf⟩, fun x hx ↦ by simpa using hfs hx,
+    fun x hx ↦ by simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, fun x ↦ ?_⟩
+  · apply HasCompactSupport.intro' k_comp k_closed (fun x hx ↦ ?_)
+    simp only [ContinuousMap.coe_mk, sub_eq_zero]
+    apply (hft _).symm
+    contrapose! hx
+    simp only [mem_compl_iff, not_not] at hx
+    exact interior_subset hx
+  · have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x
+    simp [this]
diff --git a/lake-manifest.json b/lake-manifest.json
index b7153885efeec..9a5afb367f351 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "396201245bf244f9d78e9007a02dd1c388193d27",
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
diff --git a/test/peel.lean b/test/peel.lean
index 661d643e3ac02..bcb2e64677a2b 100644
--- a/test/peel.lean
+++ b/test/peel.lean
@@ -150,6 +150,10 @@ example (x y : ℝ) : (∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) ↔
     intro
     linarith
 
+example : (∃ k > 0, ∃ n ≥ k, n = k) ↔ ∃ k > 0, ∃ n ≥ k, k = n := by
+  peel 4
+  exact eq_comm
+
 /-! ## Eventually and frequently -/
 
 example {f : ℝ → ℝ} (h : ∀ x : ℝ, ∀ᶠ y in 𝓝 x, |f y - f x| ≤ |y - x|) :