## Stream: new members

### Topic: a way to try a tactic and "no-op"

#### Eric Rodriguez (Feb 25 2021 at 18:45):

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?

tactic#try

thanks!

#### Eric Rodriguez (Feb 25 2021 at 18:48):

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

#### Eric Rodriguez (Feb 25 2021 at 18:50):

wait no I'm being silly sorry!

#### Eric Wieser (Feb 25 2021 at 18:59):

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

#### Damiano Testa (Feb 25 2021 at 20:00):

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

#### Yakov Pechersky (Feb 25 2021 at 20:06):

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


Last updated: May 12 2021 at 22:15 UTC