rw with hypotheses

Stream: new members

[Jordi Saludes Closa]

I wonder how can Irw taking into account an hypothesis.

For instance: there is min_cases:

∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a

and I want to make the following work.

example (h: a ≤ b) :  min a b = a := by
  rw [min_cases]

Should I somehow split min_cases first?

[Notification Bot]

A message was moved here from #new members > multiplication in EReal, least upper bounds over Real, ENNRe by Ruben Van de Velde.

[Julian Berman]

Can you make that a #mwe?

[Julian Berman]

(deleted)

[Ruben Van de Velde]

And what do you mean by "work" :)

[Michal Wallace (tangentstorm)]

@Jordi Saludes Closa rw applies rules that use = or ↔ or → as the top-level operator. In min_cases, the top level is ∨, so it isn't the right tool for the job.

But if you try this:

example {a b:Nat} (h: a ≤ b) :  min a b = a := by rw?

Lean will suggest a proof that does use rw with the hypothesis:

example {a b:Nat} (h: a ≤ b) :  min a b = a := by rw [Nat.min_eq_left h]

[Jordi Saludes Closa]

I see. Thanks!