Commit 2026-09-30 15:25 0c031865

chore: fix implicit reducible diamond in faces lattice (#44127) The following fails before the PR, works after it:

example : (PointedCone.Face.instCompleteLattice.toSemilatticeInf : SemilatticeInf C.Face) = 
    PointedCone.Face.instSemilatticeInf := by
  with_implicit rfl