chore(Filter/Basic): use abbrev (#16624)

Otherwise `coframeMinimalAxioms.toCompleteLattice = instCompleteLatticeFilter` isn't `with_reducible_and_instances rfl`.
leanprover-community · Sep 9, 2024 · 1fa672e · 1fa672e
1 parent 9d2de1a
commit 1fa672e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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