dunfold for abbreviated notations?

Stream: new members

[Chris M]

Consider the following code:

import tactic

variables {a b c : ℕ}
example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) :=
begin
   dunfold | at divab,
end

The dunfold doesn't work, probably because | is an abbreviation. Is there a way to make this work? (hopefully without actually manually stating the definition of a | b)

[Jalex Stark]

you probably want cases divab

[Jalex Stark]

I think \mid is an abbreviation for has_dvd.dvd, so it may be easier to rw or unfold with that

[Chris M]

Yeah I do, but I also want to know how to see the definition of a | b within the tactic.

[Kevin Buzzard]

The easiest way (in VS Code): hover over the \| symbol in the statement of your example, to discover that it is has_dvd.dvd. Other ways: #print notation \| just above or below your example, or set_option pp.notation false above your example, so you can see what Lean actually sees after the notation has been unravelled. dunfold takes a function, not notation. Finally, once you've figured out how to proceed after the unfolding:

import tactic

variables {a b c : ℕ}
example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) :=
begin
  dunfold has_dvd.dvd at divab,
  -- divab: ∃ (c : ℕ), b = a * c
  cases divab with m hm,
  -- ...
  sorry
end

don't forget to delete the dunfold, because your code probably compiles without it.