Turning a proof by cases into a linear proof

Stream: new members

[Aniruddh Agarwal]

Consider the following proof:

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

example (f : ℝ → ℝ) (h : non_decreasing f) (h' : ∀ x, f (f x) = x) : ∀ x, f x = x :=
begin
  intro x,
  specialize h' x,
  unfold non_decreasing at h,
  cases le_total (f x) x with,
  { specialize h (f x) x h_1,
    rw h' at h,
    exact le_antisymm h_1 h },
  { specialize h x (f x) h_1,
    rw h' at h,
    exact le_antisymm h h_1 }
end

The proof for each case is basically the same (with the only difference being the calls to le_antisymm, which are also the same modulo the symmetry of equality). Is there any way I can make the proof completely linear?

[Yakov Pechersky]

example (f : ℝ → ℝ) (h : non_decreasing f) (h' : ∀ x, f (f x) = x) : ∀ x, f x = x :=
begin
  intro x,
  specialize h' x,
  cases le_total x (f x);
  linarith [h _ _ h_1]
end

[Yakov Pechersky]

Still splits into cases, but both are just dealing with linear arithmetic, as you pointed out, and the terms can be inferred from the goal for the h hypothesis

[Aniruddh Agarwal]

Thanks!

[Aniruddh Agarwal]

This wasn't quite what I was hoping for, but I'm still very satisfied with the solution you provided

[Yakov Pechersky]

What were you hoping for?

[Aniruddh Agarwal]

I'm not sure honestly

[Jalex Stark]

you might have been looking for tactic#wlog

[Aniruddh Agarwal]

Jalex Stark said:

you might have been looking for tactic#wlog

Can you explain?

[Jalex Stark]

it is supposed to be similar to the mathematician's "without loss of generality", which means "if you give me a proof of one case, I'll show you how to turn it into a proof of the others"

[Jalex Stark]

i, uh, don't really know how to use it

[Aniruddh Agarwal]

I'll have to remind myself of what I was originally trying to do, but I'll take a look at this in a few minutes. wlog sounds like it could be very useful

[Kevin Buzzard]

It's not as powerful as mathematician's WLOG. I'm not sure it's up to this task.