diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
index 79bc93e777efe..79c185c5e800c 100644
--- a/Mathlib/Order/Filter/Basic.lean
+++ b/Mathlib/Order/Filter/Basic.lean
@@ -785,7 +785,8 @@ instance : DistribLattice (Filter α) :=
           x.sets_of_superset hs inter_subset_right, ht₂, rfl⟩ }
 
 /-- The dual version does not hold! `Filter α` is not a `CompleteDistribLattice`. -/
-def coframeMinimalAxioms : Coframe.MinimalAxioms (Filter α) :=
+-- See note [reducible non-instances]
+abbrev coframeMinimalAxioms : Coframe.MinimalAxioms (Filter α) :=
   { Filter.instCompleteLatticeFilter with
     iInf_sup_le_sup_sInf := fun f s t ⟨h₁, h₂⟩ => by
       classical