Transparency setting in `solve_by_elim`

Stream: mathlib4

[Heather Macbeth]

I notice that the "apply config" objects no longer have a transparency setting in Lean 4, whereas they did in Lean 3, compare docs4#Lean.Meta.ApplyConfig with docs#tactic.apply_cfg. I assume that in Lean 4 the intention is to deal with this using with_reducible or similar. Is that right? For example:

import Mathlib.Data.Rat.Order

-- works
example {a b : ℚ} : a / 4 ≤ b / 4 := by
  apply mul_le_mul <;> sorry

-- fails
example {a b : ℚ} : a / 4 ≤ b / 4 := by
  with_reducible { apply mul_le_mul <;> sorry }
/-
tactic 'apply' failed, failed to unify
  ?a * ?c ≤ ?b * ?d
with
  a / 4 ≤ b / 4
-/

[Heather Macbeth]

I noticed this because in mathlib3 the transparency setting in apply_config percolated to a transparency setting in apply_rules, where I used it a lot. (For example, to ensure that in an example like the above, I could use an apply_rules attribute set including both mul_le_mul and div_le_div, without fussing about lemma ordering to make sure that the dumb choice didn't take precedence.)

I guess it's now a little harder to provide transparency settings for apply_rules and solve_by_elim, but if my guess above about the expected approach is correct, probably it's not too hard? Anyway, that's one more feature request from me on solve_by_elim ... cc @Scott Morrison

[Scott Morrison]

Does it work if you put with_reducible around the solve_by_elim / apply_rules?

[Heather Macbeth]

Yes. This makes the sensible choice div_le_div no matter what the ordering of [mul_le_mul, div_le_div] is:

import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Data.Rat.Order

example {a b : ℚ} : a / 4 ≤ b / 4 := by with_reducible {
  apply_rules [mul_le_mul, div_le_div]
  . sorry
  . sorry
  . sorry
  . sorry }

and this does nothing (as desired):

example {a b : ℚ} : a / 4 ≤ b / 4 := by with_reducible {
  apply_rules [mul_le_mul]
  sorry }

[Heather Macbeth]

But it's awkward having to put with_reducible around the whole thing, including the proofs of the goals created -- is there a syntax for with_reducible { ... } which sends the goals produced onwards, so the sorries don't need to be inside the braces?

[Scott Morrison]

It's okay, I can add this as an option to solve_by_elim easily.

[Scott Morrison]

mathlib4#1609, not tested at all! @Heather Macbeth, could you check if that helps, and then write a test case? (Either post here or add the to PR directly, as suits you.)

[Heather Macbeth]

Wow, that was fast :). I'm off now for a couple of hours but I'll test it later tonight. Thank you!

[Heather Macbeth]

@Scott Morrison It works perfectly. I pushed a test.