How to specify where "apply" applies

Stream: new members

[Jakob Scholbach]

Another a newbie question (I never felt this stupid!):

example : min (min a b) c = min a (min b c) :=
begin
  apply le_antisymm,
  {
    apply le_min,
    {
      -- the goal here is:  min (min a b) c ≤ a
     },
    {

    }
  },
  {

  }
end

In this example, at the indicated spot I would like to do "apply min_le_left to the outer min". How do I specify where apply does its job?

[Riccardo Brasca]

min_le_left takes two argument, you can specify them writing min_le_left x y explicitly

[Jakob Scholbach]

OK, I see. If I add apply min_le_left (min a b) c, it says invalid apply tactic, failed to unify min (min a b) c ≤ a with min (min a b) c ≤ min a b. I guess I further need to combine this inequality I got from here with min a b \le a. Is there a quick way to do this or do I need to write something like have h : ... and then say apply h?

[Riccardo Brasca]

min_le_left (min a b) c says that min (min a b) c ≤ min a b, but your goal is min (min a b) c ≤ min b c so you cannot use it

[Riccardo Brasca]

How is your proof with pen and paper?

[Ruben Van de Velde]

transitivity (min b c),, perhaps

[Riccardo Brasca]

I guess it is an exercise... if we can use the full mathlib min_assoc a b c says exactly min (min a b) c = min a (min b c)

[Jakob Scholbach]

@Riccardo Brasca : yes, I would like to "save" as an intermediate step min (min a b) c \le min a b, then apply min a b \le a and use transitivity of min.

[Riccardo Brasca]

Indeed the actual proof uses it

[Ruben Van de Velde]

Or with calc:

import data.nat.basic

example (a b c : nat) : min (min a b) c = min a (min b c) :=
begin
  apply le_antisymm,
  { apply le_min,
    { calc min (min a b) c
          ≤ min a b : min_le_left _ _
      ... ≤ a : min_le_left _ _ },
    { sorry } },
  { sorry }
end