apply? tactic fails?

Stream: lean4

[DogaCanSertbas]

In LFTCM2023, we had a problem related to "apply?" tactic. More precisely, after writing the "apply?" tactic, it gave several suggestions. However, after doing the corresponding replacement, say "refine Iff.mpr mem_lowerBounds ?h.a", then LEAN failed to continue. Thanks to Eric Wieser, he suggested to rewrite "refine Iff.mpr mem_lowerBounds ?h.aa" which solved the problem. It seems that it is a bug

[Bhavik Mehta]

(I am in the process of minimising the example for Doga)

[Martin Dvořák]

On a related note, has the output of apply? ever been useful for you?

[Martin Dvořák]

I am not attempting to criticize the tactic. I just want to know whether I should keep trying to make use of it.

[Bhavik Mehta]

In this actual case the third result of apply? was a sensible suggestion (although rw? finds the same correct lemma as its first suggestion, and avoids the Iff.mpr at the start). So I suppose it was useful but not as useful as rw? would have been

[DogaCanSertbas]

Martin Dvořák dedi:

On a related note, has the output of apply? ever been useful for you?

As a beginner, I can say yes :)

[Martin Dvořák]

I am happy to hear about it!

[Martin Dvořák]

Speaking of beginners, it took me almost two years to learn what the .mpr thing means, lol.

[Bhavik Mehta]

I'm struggling to get it more minimised, so here's my progress so far in case someone else can take it further:

import Mathlib.Data.Real.Basic

noncomputable def bad_definition : ℝ := ⨅ (n : ℕ) (_ : 1 ≤ n), 1 / n

theorem failure : bad_definition ≤ 1 := by
  apply ciInf_le_of_le _ 1
  · apply ciInf_le_of_le _ le_rfl
    · sorry
    · use 0
      refine Iff.mpr mem_lowerBounds ?h.a
      sorry
  · use 0
    apply?

[Alex J. Best]

I'm not sure exactly what the correct fix is yet, but here is a more minimal example with the same behaviour (though in this case you could say that axiom f is written badly)

import Mathlib.Tactic.LibrarySearch

axiom T : (a : Nat) → Prop
axiom f (a : Nat) : (h : T (3 * a)) → (h : T (2 * a)) → T a
example (b : Nat) : T b := by
  apply f
  apply f
  sorry
  apply?

[Bhavik Mehta]

Would it work to have two axioms which both use the name h, so it's not attributable to bad naming of a single thing?