apply a term to all assumptions?

Stream: new members

[Chris M]

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]

This doesn't exactly answer your question, but you can do

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]

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]

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