max(a,b) ≤ c → (a ≤ c)∧(b ≤ c)

Stream: new members

[Michael Nestor]

seems so simple but don't know how to apply le_max_left

example (a b c: ℝ): max a b ≤ c → (a ≤ c ∧ b ≤ c) :=
begin
  intros h,
  have h1: a ≤ max a b, sorry,  -- use le_max_left?
  have h2: b ≤ max a b, sorry,
  split, linarith, linarith,
end

[Sky Wilshaw]

You can try

have h1: a ≤ max a b := le_max_left a b

or

have h1: a ≤ max a b,
{ exact le_max_left a b, },

[Michael Nestor]

got it! I was tripped up on some cases where we don't need := after have

[Sky Wilshaw]

have x : T := a makes a new hypothesis called x of type T, and assigns it the proof term a

[Sky Wilshaw]

If you want to use tactics to solve the proposition in your have-expression, you don't use :=, and start a new tactic block.

[Sky Wilshaw]

Proof terms can be difficult to write, so in more complex cases than this I avoid the := syntax and just solve the sub-goal with tactics.

[Yaël Dillies]

docs#max_le_iff if you want to have a look at how mathlib does it