How to use `apply?` effectively

Stream: new members

[Nick Attkiss]

Hi all,

I'm currently working through the Mathematics in Lean tutorial, and Chapter 5 presents the following simple example:

example (a b c : Nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c :=
  -- apply? suggests the following:
  (mul_right_inj' h').mp h

I tried using apply? myself to see the suggestion, but

example (a b c : Nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c := by
  apply?

gives me a long list of complicated choices involving the refine tactic (which I've not seen yet), none of which seem to be the desired proof term (mul_right_inj' h').mp h.

Is this expected behavior? If so, how am I meant to use apply? effectively if even the above simple example generates so much noise?

[Kevin Buzzard]

I believe apply? basically doesn't work for equality goals

[Kevin Buzzard]

How does exact? fare?

[Ruben Van de Velde]

Does apply? using h do anything?

[Bbbbbbbbba]

Did you do import Mathlib or otherwise have mul_right_inj in scope?

[Kevin Buzzard]

Indeed, I'll have to retract my previous comment: apply? is working fine for me with enough imports. However it's finding Nat.mul_right_inj.