diff --git a/Mathlib/Tactic/TFAE.lean b/Mathlib/Tactic/TFAE.lean
index 80cfbc9e87059..4594db66cf4d4 100644
--- a/Mathlib/Tactic/TFAE.lean
+++ b/Mathlib/Tactic/TFAE.lean
@@ -128,7 +128,8 @@ partial def proveChain (i : ℕ) (is : List ℕ) (P : Q(Prop)) (l : Q(List Prop)
   match l with
   | ~q([]) => return q(Chain.nil)
   | ~q($P' :: $l') =>
-    let i' :: is' := is | unreachable!
+    -- `id` is a workaround for https://github.com/leanprover-community/quote4/issues/30
+    let i' :: is' := id is | unreachable!
     have cl' : Q(Chain (· → ·) $P' $l') := ← proveChain i' is' q($P') q($l')
     let p ← proveImpl hyps atoms i i' P P'
     return q(Chain.cons $p $cl')
@@ -139,7 +140,8 @@ partial def proveGetLastDImpl (i i' : ℕ) (is : List ℕ) (P P' : Q(Prop)) (l :
   match l with
   | ~q([]) => proveImpl hyps atoms i' i P' P
   | ~q($P'' :: $l') =>
-    let i'' :: is' := is | unreachable!
+    -- `id` is a workaround for https://github.com/leanprover-community/quote4/issues/30
+    let i'' :: is' := id is | unreachable!
     proveGetLastDImpl i i'' is' P P'' l'
 
 /-- Attempt to prove a statement of the form `TFAE [P₁, P₂, ...]`. -/
@@ -148,7 +150,8 @@ def proveTFAE (is : List ℕ) (l : Q(List Prop)) : MetaM Q(TFAE $l) := do
   | ~q([]) => return q(tfae_nil)
   | ~q([$P]) => return q(tfae_singleton $P)
   | ~q($P :: $P' :: $l') =>
-    let i :: i' :: is' := is | unreachable!
+    -- `id` is a workaround for https://github.com/leanprover-community/quote4/issues/30
+    let i :: i' :: is' := id is | unreachable!
     let c ← proveChain hyps atoms i (i'::is') P q($P' :: $l')
     let il ← proveGetLastDImpl hyps atoms i i' is' P P' l'
     return q(tfae_of_cycle $c $il)
diff --git a/lean-toolchain b/lean-toolchain
index b39e2129f7686..ec40378583fcc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-23
+leanprover/lean4:nightly-2024-01-24