Skip to content

Commit cc26c21

Browse files
committed
chore: fix implicit-reducible diamond in digraphs (#38291)
The following fails on master, works after the PR: ```lean example : (Digraph.instPartialOrder.toLE : LE (Digraph V)) = Digraph.instLE := by with_reducible_and_instances rfl ``` Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
1 parent af3d952 commit cc26c21

File tree

1 file changed

+2
-4
lines changed

1 file changed

+2
-4
lines changed

Mathlib/Combinatorics/Digraph/Basic.lean

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -167,11 +167,9 @@ theorem iSup_adj {f : ι → Digraph V} : (⨆ i, f i).Adj a b ↔ ∃ i, (f i).
167167
@[simp]
168168
theorem iInf_adj {f : ι → Digraph V} : (⨅ i, f i).Adj a b ↔ (∀ i, (f i).Adj a b) := by simp [iInf]
169169

170-
instance : PartialOrder (Digraph V) where
171-
__ := PartialOrder.lift _ adj_injective
172-
le G H := ∀ ⦃a b⦄, G.Adj a b → H.Adj a b
170+
instance : PartialOrder (Digraph V) := fast_instance% PartialOrder.lift _ adj_injective
173171

174-
instance distribLattice : DistribLattice (Digraph V) :=
172+
instance distribLattice : DistribLattice (Digraph V) := fast_instance%
175173
adj_injective.distribLattice _ .rfl .rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl
176174

177175
instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Digraph V) where

0 commit comments

Comments
 (0)