## Stream: new members

### Topic: apply a term to all assumptions?

#### Chris M (Jul 22 2020 at 04:32):

The following is a working proof, but it's slightly verbose to have to apply  to hfa, hfb, nng separately. Is it possible to just say: "apply x to all assumptions"?

import data.real.basic
import tactic

example (hfa : fn_ub f a) (hfb : fn_ub g b)
(nng : fn_lb g 0) (nna : 0 ≤ a) :
fn_ub (λ x, f x * g x) (a * b) :=
begin
dunfold fn_ub fn_lb at *,
intro x,
have h1:= hfa x,
have h1:= hfb x,
have h3:= nng x,
nlinarith
end


#### Alex J. Best (Jul 22 2020 at 04:48):

example (hfa : fn_ub f a) (hfb : fn_ub g b)
(nng : fn_lb g 0) (nna : 0 ≤ a) :
fn_ub (λ x, f x * g x) (a * b) :=
begin
dunfold fn_ub fn_lb at *,
intro x,
nlinarith [hfa x, hfb x, nng x],
end


to avoid typing have a lot

#### Chris M (Jul 22 2020 at 04:50):

Yeah that's good but not exactly what I was after.
In fact, it would be nice to replace hfa, hfb, nng with hfa x, hfb x, nng x respectively, so that one has a cleaner goal state.

#### Alex J. Best (Jul 22 2020 at 04:51):

For that you can use specialize

example (hfa : fn_ub f a) (hfb : fn_ub g b)
(nng : fn_lb g 0) (nna : 0 ≤ a) :
fn_ub (λ x, f x * g x) (a * b) :=
begin
dunfold fn_ub fn_lb at *,
intro x,
specialize hfa x,
specialize hfb x,
specialize nng x,
nlinarith,
end


Last updated: May 08 2021 at 09:11 UTC