How can I direct apply to use my variables?

Stream: new members

[Baran Zadeoglu]

I am new to lean and having a lot of problems with the apply tactic. In particular, I often try and fail to apply a fact using different variables. For example the code below, I try to apply "h" with a and b flipped.

theorem aux : min a b + c ≤ min (a + c) (b + c) := by
  have h: min a b + c ≤ a + c := by
    apply add_le_add_right
    apply min_le_left
  apply le_min
  ·apply h
  ·rw[min_comm]
   apply h

Another example:

#check (abs_add : ∀ a b : ℝ, |a + b| ≤ |a| + |b|)

example : |a| - |b| ≤ |a - b| := by

To this, I would want to apply abs_add to a-b, b. I can't quite figure out the write way to do it.

Both are from the book "mathematics in lean".

[Ruben Van de Velde]

It would be easier to help you if you posted a #mwe

[Ruben Van de Velde]

Possibly you meant your have h to be about all a, b, c rather than just the ones from your theorem? Then you should add \forall a b c, to the start