mono in data.set.lattice

Stream: general

[Patrick Massot]

Is there any objection to have import tactic.monotonicity at top of data.set.lattice? I'm asking because this is a fairly foundational file.

[Patrick Massot]

The monotonicity tactics are currently very under-employed in mathlib, but many lemmas from that file could be tagged. Like norm_cast, these tactics become useful only if lemmas are tagged appropriately.

[Rob Lewis]

tactic.monotonicity doesn't look so foundational itself. Does this import even work?

[Rob Lewis]

You can always tag the lemmas in tactic.monotonicity instead of at the moment of definition.

[Patrick Massot]

Yes, that's why I ask, and yes it works.

[Rob Lewis]

Without looking at an import graph it's hard to judge the cost here. Do we have a quick way to generate one of those yet?

[Patrick Massot]

Sure.

[Patrick Massot]

Which part do you want to see?

[Patrick Massot]

Everything below tactic.monotonicity?

[Patrick Massot]

Actually I was wrong, it's not easy. It seems that the recent fix that allows to use open_locale right after imports was not propagated to lean --deps, so import graph generation is currently broken @Gabriel Ebner

$ lean --deps src/algebra/pi_instances.lean
/tmp/mathlib/src/algebra/module.olean
/tmp/mathlib/src/ring_theory/subring.olean
/tmp/mathlib/src/ring_theory/prod.olean
error: file 'open_locale' not found in the LEAN_PATH
error: file 'big_operators' not found in the LEAN_PATH
/home/pmassot/.elan/toolchains/leanprover-community-lean-3.16.1/lib/lean/library/init/default.olean

[Gabriel Ebner]

Oops, lean#323.