Loogle didn't find this

Stream: general

[Kenny Lau]

Using _ ≤ nonZeroDivisors _ did not find Ideal.primeCompl_le_nonZeroDivisors?

[Yury G. Kudryashov]

This is a known issue: loogle includes all instance names in the search, so it fails to find theorems that take a different path in the instance resolution.

[Yury G. Kudryashov]

As a workaround, I use something like |- _ ≤ _, nonZeroDivisors. It gives some false positives though.

[Kevin Buzzard]

I have no idea what Yury's answer means. The proof is

theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type*} [CommSemiring R] [NoZeroDivisors R]
    (P : Ideal R) [P.IsPrime] : P.primeCompl ≤ nonZeroDivisors R :=
  le_nonZeroDivisors_of_noZeroDivisors <| not_not_intro P.zero_mem

Where is the "different path in the instance resolution"?

[Kenny Lau]

@Kevin Buzzard I've used pp.explicit to print out the two expressions and compared them:

import Mathlib

set_option pp.explicit true
#check _ ≤ nonZeroDivisors _
#check Ideal.primeCompl_le_nonZeroDivisors

and for everyone's convenience I've extracted out the two important parts: the resolution for the LE instance and the MulOneClass instance (for submonoid)

-- from #check _ ≤ nonZeroDivisors _

(@Preorder.toLE _
  (@PartialOrder.toPreorder _
    (@CompletePartialOrder.toPartialOrder _
      (@CompleteLattice.toCompletePartialOrder _
        (@Submonoid.instCompleteLattice ?m.3 _)))))

(@Submonoid ?m.3
  (@MulZeroOneClass.toMulOneClass ?m.3
    (@MonoidWithZero.toMulZeroOneClass ?m.3 ?m.4)))

-- from #check Ideal.primeCompl_le_nonZeroDivisors

(@Preorder.toLE _
  (@PartialOrder.toPreorder _
    (@OmegaCompletePartialOrder.toPartialOrder _
      (@CompleteLattice.instOmegaCompletePartialOrder _
        (@Submonoid.instCompleteLattice R _)))))

(@Submonoid R
  (@MulZeroOneClass.toMulOneClass R
    (@NonAssocSemiring.toMulZeroOneClass R _)))

and I would guess that it is because of the subtle differences here.

[Kenny Lau]

the second one actually would seem more likely, and the difference is the two different ways to obtain MulZeroOneClass:

• @MonoidWithZero.toMulZeroOneClass ?m.3 ?m.4 vs.
• @NonAssocSemiring.toMulZeroOneClass R _