a way to try a tactic and "no-op"

Stream: new members

[Eric Rodriguez]

So for example, I apply mul_lt_mul and I get four goals; 3 of them are easily provable by assumption;, but one isn't. What I want to do is something like apply mul_lt_mul; assumption, and then deal with the last case. However, assumption errors here; is there a way to just ignore that?

[Eric Wieser]

tactic#try

[Eric Rodriguez]

thanks!

[Eric Rodriguez]

wait, no, that doesn't work; it solves the first goal and then gives up after the goal that errors

[Eric Rodriguez]

wait no I'm being silly sorry!

[Eric Wieser]

Of course, another approach would just be to add have : last_goal, {...} before you apply, and then assumption will succeed :)

[Damiano Testa]

Also, any_goals { [...] }, applies [...] to any unsolved goal, failing only if what you feed it makes progress nowhere.

[Yakov Pechersky]

For others, an example:

import data.nat.basic

example {a b c d : ℕ} (h : a < c) (h' : b ≤ d) (hb : 0 < b) : a * b < c * d :=
begin
  apply mul_lt_mul;
  try { assumption },
  exact (show 0 ≤ c, from sorry)
end