From 1fa672e90293f0cfd345e1750284b2ec9a631a04 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 9 Sep 2024 19:54:58 +0000 Subject: [PATCH] chore(Filter/Basic): use `abbrev` (#16624) Otherwise `coframeMinimalAxioms.toCompleteLattice = instCompleteLatticeFilter` isn't `with_reducible_and_instances rfl`. --- Mathlib/Order/Filter/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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