chore: adaptations for nightly-2025-12-13

Archive/Imo/Imo2015Q6.lean

@@ -85,7 +85,7 @@ lemma pool_subset_Icc : ∀ {t}, pool a t ⊆ Icc 0 2014
   | t + 1 => by
     intro x hx
     simp_rw [pool, mem_map, Equiv.coe_toEmbedding, Equiv.subRight_apply] at hx
-    obtain ⟨y, my, ey⟩ := hx
+    obtain ⟨y, my, rfl⟩ := hx
     suffices y ∈ Icc 1 2015 by rw [mem_Icc] at this ⊢; lia
     rw [mem_insert, mem_erase] at my; rcases my with h | ⟨h₁, h₂⟩
     · exact h ▸ ha.1 t

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -27,7 +27,7 @@ theorem IsMulTorsionFree.mk' (ih : ∀ x ≠ 0, ∀ y ≠ 0, ∀ n ≠ 0, (x ^ n
   refine ⟨fun n hn x y hxy ↦ ?_⟩
   by_cases h : x ≠ 0 ∧ y ≠ 0
   · exact ih x h.1 y h.2 n hn hxy
-  grind [pow_eq_zero, zero_pow]
+  grind [eq_zero_of_pow_eq_zero, zero_pow]
 
 variable [UniqueFactorizationMonoid M] [NormalizationMonoid M] [IsMulTorsionFree Mˣ]
 

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -225,7 +225,18 @@ end Fewnomials
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
     coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
   rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-  all_goals grind [mem_antidiagonal, mul_zero]
+  #adaptation_note
+  /--
+  It may be possible to change this back to
+  `all_goals grind [mem_antidiagonal, mul_zero]`
+  on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+  but if not just remove this note.
+  The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+  -/
+  · rintro ⟨i, j⟩ h1 h2
+    rw [coeff_X_pow, if_neg, mul_zero]
+    grind [mem_antidiagonal]
+  · grind [mem_antidiagonal]
 
 @[simp]
 theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :

Mathlib/Algebra/Polynomial/RuleOfSigns.lean

@@ -313,7 +313,15 @@ theorem succ_signVariations_le_X_sub_C_mul (hη : 0 < η) (hP : P ≠ 0) :
   · --P is zero degree, therefore a constant.
     have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
     have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
-      grind [coeff_X_sub_C_mul, mul_zero, coeff_eq_zero_of_natDegree_lt]
+      #adaptation_note
+      /--
+      It may be possible to change this back to
+      `grind [coeff_X_sub_C_mul, mul_zero, coeff_eq_zero_of_natDegree_lt]`
+      on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+      but if not just remove this note.
+      The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+      -/
+      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
     dsimp [signVariations, coeffList]
     rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]
     simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]

Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

@@ -104,7 +104,7 @@ def mk₂ {n : ℕ} {X : Truncated.{u} (n + 1)} (p q : X.Path 1)
 
 /-- For `j + l ≤ m`, a path of length `m` restricts to a path of length `l`, namely
 the subpath spanned by the vertices `j ≤ i ≤ j + l` and edges `j ≤ i < j + l`. -/
-def interval (f : Path X m) (j l : ℕ) (h : j + l ≤ m := by lia) : Path X l where
+def interval (f : Path X m) (j l : ℕ) (h : j + l ≤ m := by omega) : Path X l where
   vertex i := f.vertex ⟨j + i, by lia⟩
   arrow i := f.arrow ⟨j + i, by lia⟩
   arrow_src i := f.arrow_src ⟨j + i, by lia⟩

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -259,6 +259,7 @@ lemma cfcₙHom_eq_cfcₙ_extend {a : A} (g : R → R) (ha : p a) (f : C(σₙ R
   have hg0 : (Function.extend Subtype.val f g) 0 = 0 := by
     rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]
     exact map_zero f
+  generalize Function.extend Subtype.val f g = f' at *
   rw [cfcₙ_apply ..]
   congr!
 

Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

@@ -60,18 +60,18 @@ variable {J : Type w}
 inductive WalkingParallelFamily (J : Type w) : Type w
   | zero : WalkingParallelFamily J
   | one : WalkingParallelFamily J
+deriving Inhabited
 
 open WalkingParallelFamily
 
+-- We do not use `deriving DecidableEq` here
+-- because it generates an instance with unnecessary hypotheses.
 instance : DecidableEq (WalkingParallelFamily J)
   | zero, zero => isTrue rfl
-  | zero, one => isFalse fun t => WalkingParallelFamily.noConfusion t
-  | one, zero => isFalse fun t => WalkingParallelFamily.noConfusion t
+  | zero, one => isFalse fun t => by grind
+  | one, zero => isFalse fun t => by grind
   | one, one => isTrue rfl
 
-instance : Inhabited (WalkingParallelFamily J) :=
-  ⟨zero⟩
-
 -- Don't generate unnecessary `sizeOf_spec` lemma which the `simpNF` linter will complain about.
 set_option genSizeOfSpec false in
 /-- The type family of morphisms for the diagram indexing a wide (co)equalizer. -/

Mathlib/CategoryTheory/Shift/CommShiftTwo.lean

@@ -66,7 +66,7 @@ noncomputable def CommShift₂Setup.int [Preadditive D] [HasShift D ℤ]
   assoc _ _ _ := by
     dsimp
     rw [← zpow_add, ← zpow_add]
-    cutsat
+    lia
   commShift _ _ := ⟨by cat_disch⟩
   ε p q := (-1) ^ (p * q)
 

Mathlib/Combinatorics/Quiver/Path.lean

@@ -270,7 +270,7 @@ def decidableEqBddPathsOfDecidableEq (n : ℕ) (h₁ : DecidableEq V)
     | _, _, .nil, .nil => isTrue rfl
     | _, _, .nil, .cons _ _
     | _, _, .cons _ _, .nil =>
-      isFalse fun h => Quiver.Path.noConfusion rfl (heq_of_eq (Subtype.mk.inj h))
+      isFalse fun h => Quiver.Path.noConfusion rfl .rfl .rfl .rfl (heq_of_eq (Subtype.mk.inj h))
     | _, _, .cons (b := v') p' α, .cons (b := v'') q' β =>
       match v', v'', h₁ v' v'' with
       | _, _, isTrue (Eq.refl _) =>

Mathlib/Control/Lawful.lean

@@ -21,24 +21,6 @@ section
 
 variable {σ : Type u} {m : Type u → Type v} {α β : Type u}
 
-/--
-`StateT` doesn't require a constructor, but it appears confusing to declare the
-following theorem as a simp theorem.
-```lean
-@[simp]
-theorem run_fun (f : σ → m (α × σ)) (st : σ) : StateT.run (fun s => f s) st = f st :=
-  rfl
-```
-If we declare this theorem as a simp theorem, `StateT.run f st` is simplified to `f st` by eta
-reduction. This breaks the structure of `StateT`.
-So, we declare a constructor-like definition `StateT.mk` and a simp theorem for it.
--/
-protected def mk (f : σ → m (α × σ)) : StateT σ m α := f
-
-@[simp]
-theorem run_mk (f : σ → m (α × σ)) (st : σ) : StateT.run (StateT.mk f) st = f st :=
-  rfl
-
 /-- A copy of `LawfulFunctor.map_const` for `StateT` that holds even if `m` is not lawful. -/
 protected lemma map_const [Monad m] :
     (Functor.mapConst : α → StateT σ m β → StateT σ m α) = Functor.map ∘ Function.const β :=
@@ -62,38 +44,4 @@ theorem run_monadLift {n} [Monad m] [MonadLiftT n m] (x : n α) :
     (monadLift x : ExceptT ε m α).run = Except.ok <$> (monadLift x : m α) :=
   rfl
 
-@[simp]
-theorem run_monadMap {n} [MonadFunctorT n m] (f : ∀ {α}, n α → n α) :
-    (monadMap (@f) x : ExceptT ε m α).run = monadMap (@f) x.run :=
-  rfl
-
 end ExceptT
-
-namespace ReaderT
-
-section
-
-variable {m : Type u → Type v}
-variable {α σ : Type u}
-
-/--
-`ReaderT` doesn't require a constructor, but it appears confusing to declare the
-following theorem as a simp theorem.
-```lean
-@[simp]
-theorem run_fun (f : σ → m α) (r : σ) : ReaderT.run (fun r' => f r') r = f r :=
-  rfl
-```
-If we declare this theorem as a simp theorem, `ReaderT.run f st` is simplified to `f st` by eta
-reduction. This breaks the structure of `ReaderT`.
-So, we declare a constructor-like definition `ReaderT.mk` and a simp theorem for it.
--/
-protected def mk (f : σ → m α) : ReaderT σ m α := f
-
-@[simp]
-theorem run_mk (f : σ → m α) (r : σ) : ReaderT.run (ReaderT.mk f) r = f r :=
-  rfl
-
-end
-
-end ReaderT

Mathlib/Data/ENNReal/Inv.lean

@@ -231,9 +231,29 @@ protected theorem div_le_iff' {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ 
 protected theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) :
     (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
   cases b
-  case top => grind [mul_top, mul_zero, inv_top, ENNReal.inv_eq_zero]
+  case top =>
+    #adaptation_note
+    /--
+    It may be possible to change this back to
+    `grind [mul_top, mul_zero, inv_top, ENNReal.inv_eq_zero]`
+    on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+    but if not just remove this note.
+    The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+    -/
+    simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
+      mul_top, inv_top, mul_zero]
   cases a
-  case top => grind [top_mul, zero_mul, inv_top, ENNReal.inv_eq_zero]
+  case top =>
+    #adaptation_note
+    /--
+    It may be possible to change this back to
+    `grind [top_mul, zero_mul, inv_top, ENNReal.inv_eq_zero]`
+    on nightly-2025-12-14 (or ideally without needing the `zero_mul`),
+    but if not just remove this note.
+    The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `zero_mul`) by e-matching.
+    -/
+    simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
+      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]
   grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
     =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]
 

Mathlib/Data/Fin/Basic.lean

@@ -31,19 +31,6 @@ assert_not_exists Monoid Finset
 
 open Fin Nat Function
 
-namespace Fin
-protected alias val_sub := Fin.coe_sub
-alias val_neg' := Fin.coe_neg
-alias val_castSucc := coe_castSucc
-alias val_castAdd := coe_castAdd
-alias val_cast := coe_cast
-alias val_castLT := coe_castLT
-alias val_castLE := coe_castLE
-alias val_natAdd := coe_natAdd
-alias val_pred := coe_pred
-alias val_subNat := coe_subNat
-end Fin
-
 attribute [simp] Fin.succ_ne_zero Fin.castSucc_lt_last
 
 theorem Nat.forall_lt_iff_fin {n : ℕ} {p : ∀ k, k < n → Prop} :

Mathlib/Data/Fin/SuccPred.lean

@@ -911,7 +911,7 @@ theorem succAbove_succAbove_succAbove_predAbove {n : ℕ}
   by saying that both functions are strictly monotone and have the same range `{i, i.succAbove j}ᶜ`,
   we give a direct proof by case analysis to avoid extra dependencies. -/
   ext
-  simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, coe_pred, coe_castPred,
+  simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, val_pred, coe_castPred,
     dite_eq_ite, apply_ite Fin.val, val_succ]
   split_ifs <;> lia
 

Mathlib/Data/Fin/VecNotation.lean

@@ -145,7 +145,8 @@ open Lean Qq
 
 `let ⟨xs, tailn, tail⟩ ← matchVecConsPrefix n e` decomposes `e : Fin n → _` in the form
 `vecCons x₀ <| ... <| vecCons xₙ <| tail` where `tail : Fin tailn → _`. -/
-meta def matchVecConsPrefix (n : Q(Nat)) (e : Expr) : MetaM <| List Expr × Q(Nat) × Expr := do
+meta partial def matchVecConsPrefix (n : Q(Nat)) (e : Expr) :
+    MetaM <| List Expr × Q(Nat) × Expr := do
   match_expr ← Meta.whnfR e with
   | Matrix.vecCons _ n x xs => do
     let (elems, n', tail) ← matchVecConsPrefix n xs

Mathlib/Data/Int/Interval.lean

@@ -57,7 +57,7 @@ instance instLocallyFiniteOrder : LocallyFiniteOrder ℤ where
     · lia
     · intro
       use (x - (a + 1)).toNat
-      lia
+      omega
   finset_mem_Ioo a b x := by
     simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
       addLeftEmbedding_apply]

Mathlib/Data/List/Cycle.lean

@@ -300,7 +300,7 @@ theorem next_eq_getElem {l : List α} {a : α} (ha : a ∈ l) :
 
 theorem next_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
     l.next l[i] (get_mem ..) = l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi)) := by
-  grind [next_eq_getElem, idxOf_getElem]
+  grind [next_eq_getElem]
 
 theorem prev_eq_getElem?_idxOf_pred_of_ne_head {l : List α} {a : α} (ha : a ∈ l)
     (ha₀ : a ≠ l.head (ne_nil_of_mem ha)) : l.prev a ha = l[l.idxOf a - 1]? := by
@@ -338,7 +338,7 @@ theorem prev_eq_getElem {l : List α} {a : α} (ha : a ∈ l) :
 
 theorem prev_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
     l.prev l[i] (get_mem ..) = l[(i + (l.length - 1)) % l.length]'(Nat.mod_lt _ (by lia)) := by
-  grind [prev_eq_getElem, idxOf_getElem]
+  grind [prev_eq_getElem]
 
 @[simp]
 theorem next_getLast_eq_head (l : List α) (h : l ≠ []) (hn : l.Nodup) :

Mathlib/Data/List/Infix.lean

@@ -204,8 +204,8 @@ theorem mem_inits : ∀ s t : List α, s ∈ inits t ↔ s <+: t
       match s, mi with
       | [], ⟨_, rfl⟩ => Or.inl rfl
       | b :: s, ⟨r, hr⟩ =>
-        (List.noConfusion hr) fun ba (st : s ++ r = t) =>
-          Or.inr <| by rw [ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩⟩
+        (List.noConfusion rfl (heq_of_eq hr)) fun ba (st : s ++ r ≍ t) =>
+          Or.inr <| by rw [eq_of_heq ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, eq_of_heq st⟩, rfl⟩⟩
 
 @[simp]
 theorem mem_tails : ∀ s t : List α, s ∈ tails t ↔ s <:+ t
@@ -222,7 +222,8 @@ theorem mem_tails : ∀ s t : List α, s ∈ tails t ↔ s <:+ t
           fun e =>
           match s, t, e with
           | _, t, ⟨[], rfl⟩ => Or.inl rfl
-          | s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩
+          | s, t, ⟨b :: l, he⟩ =>
+            List.noConfusion rfl (heq_of_eq he) fun _ lt => Or.inr ⟨l, eq_of_heq lt⟩⟩
 
 theorem inits_cons (a : α) (l : List α) : inits (a :: l) = [] :: l.inits.map fun t => a :: t := by
   simp

Mathlib/Data/Nat/Find.lean

@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Data.Nat.Basic
 public import Mathlib.Tactic.Push
-public import Batteries.WF
 
 /-!
 # `Nat.find` and `Nat.findGreatest`

Mathlib/Data/PFun.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
 -/
 module
 
-public import Batteries.WF
 public import Batteries.Tactic.GeneralizeProofs
 public import Mathlib.Data.Part
 public import Mathlib.Data.Rel

Mathlib/Data/Part.lean

@@ -296,7 +296,7 @@ def ofOption : Option α → Part α
 
 @[simp]
 theorem mem_ofOption {a : α} : ∀ {o : Option α}, a ∈ ofOption o ↔ a ∈ o
-  | Option.none => ⟨fun h => h.fst.elim, fun h => Option.noConfusion h⟩
+  | Option.none => ⟨fun h => h.fst.elim, fun h => Option.noConfusion rfl (heq_of_eq h)⟩
   | Option.some _ => ⟨fun h => congr_arg Option.some h.snd, fun h => ⟨trivial, Option.some.inj h⟩⟩
 
 @[simp]

Mathlib/Data/Prod/Basic.lean

@@ -26,8 +26,10 @@ namespace Prod
 lemma swap_eq_iff_eq_swap {x : α × β} {y : β × α} : x.swap = y ↔ x = y.swap := by aesop
 
 def mk.injArrow {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
-    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
-  fun h₁ _ h₂ ↦ Prod.noConfusion h₁ h₂
+    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := by
+  intros h P w
+  cases h
+  exact w rfl rfl
 
 @[simp]
 theorem mk.eta : ∀ {p : α × β}, (p.1, p.2) = p

Mathlib/Data/Prod/PProd.lean

@@ -22,8 +22,10 @@ variable {α β γ δ : Sort*}
 namespace PProd
 
 def mk.injArrow {α : Type*} {β : Type*} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
-    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
-  fun h₁ _ h₂ ↦ Prod.noConfusion h₁ h₂
+    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := by
+  intros h P w
+  cases h
+  exact w rfl rfl
 
 @[simp]
 theorem mk.eta {p : PProd α β} : PProd.mk p.1 p.2 = p :=

Mathlib/Data/Set/Image.lean

@@ -747,7 +747,7 @@ theorem isCompl_range_inl_range_inr : IsCompl (range <| @Sum.inl α β) (range S
   IsCompl.of_le
     (by
       rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
-      exact Sum.noConfusion h)
+      exact Sum.noConfusion rfl rfl (heq_of_eq h))
     (by rintro (x | y) - <;> [left; right] <;> exact mem_range_self _)
 
 @[simp]

Mathlib/Data/Sigma/Basic.lean

@@ -51,8 +51,10 @@ instance instDecidableEqSigma [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq
     | _, b₁, _, b₂, isTrue (Eq.refl _) =>
       match b₁, b₂, h₂ _ b₁ b₂ with
       | _, _, isTrue (Eq.refl _) => isTrue rfl
-      | _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂
-    | _, _, _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun e₁ _ ↦ n e₁
+      | _, _, isFalse n => isFalse fun h ↦
+        Sigma.noConfusion rfl .rfl (heq_of_eq h) fun _ e₂ ↦ n (eq_of_heq e₂)
+    | _, _, _, _, isFalse n => isFalse fun h ↦
+      Sigma.noConfusion rfl .rfl (heq_of_eq h) fun e₁ _ ↦ n (eq_of_heq e₁)
 
 theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
     Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ ≍ b₂ := by simp
@@ -228,8 +230,10 @@ instance decidableEq [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)]
     | _, b₁, _, b₂, isTrue (Eq.refl _) =>
       match b₁, b₂, h₂ _ b₁ b₂ with
       | _, _, isTrue (Eq.refl _) => isTrue rfl
-      | _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂
-    | _, _, _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun e₁ _ ↦ n e₁
+      | _, _, isFalse n => isFalse fun h ↦
+        PSigma.noConfusion rfl .rfl (heq_of_eq h) fun _ e₂ ↦ n (eq_of_heq e₂)
+    | _, _, _, _, isFalse n => isFalse fun h ↦
+      PSigma.noConfusion rfl .rfl (heq_of_eq h) fun e₁ _ ↦ n (eq_of_heq e₁)
 
 theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
     @PSigma.mk α β a₁ b₁ = @PSigma.mk α β a₂ b₂ ↔ a₁ = a₂ ∧ b₁ ≍ b₂ :=

Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

@@ -521,7 +521,7 @@ scoped macro:max K:term "⟮" xs:term,* "⟯" : term => do ``(adjoin $K $(← mk
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 @[app_delab IntermediateField.adjoin]
-meta def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
+meta partial def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
   let e ← getExpr
   guard <| e.isAppOfArity ``adjoin 6
   let F ← withNaryArg 0 delab