How to apply eq_or_lt_of_le on a hypothesis

Stream: new members

[Shadman Sakib]

import data.real.basic
import algebra.group.pi

set_option pp.beta true

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

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

example (f : ℝ → ℝ) : (non_decreasing f) ↔ ∀ x y, x < y → f x ≤ f y :=
begin
  split,
  intros hf x₁ x₂ h,
  apply hf,
  exact le_of_lt h,

  intros h x₁ y₁ hf,
  apply eq_or_lt_of_le at hf,

end

[Shadman Sakib]

I want to use the eq_or_lt_of_le term to rewrite my hypothesis x \le y as x = y or x < y, but I can't

[Shadman Sakib]

Is there a way to do this?

[Adam Topaz]

your code is not working for me. Are those all the imports?

[Shadman Sakib]

Sorry forgot the defs

[Adam Topaz]

import data.real.basic
import algebra.group.pi

set_option pp.beta true

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

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

example (f : ℝ → ℝ) : (non_decreasing f) ↔ ∀ x y, x < y → f x ≤ f y :=
begin
  split,
  intros hf x₁ x₂ h,
  apply hf,
  exact le_of_lt h,

  intros h x₁ y₁ hf,
  replace hf := eq_or_lt_of_le hf,

end

[Shadman Sakib]

Thanks!

[Shadman Sakib]

Now is there a way to split hf?

[Adam Topaz]

cases hf

[Shadman Sakib]

or is that through cases

[Shadman Sakib]

yeah

[Shadman Sakib]

okay thanks

[Shadman Sakib]

very trivial questions

[Adam Topaz]

It's good practice to use { .. } to break up your goals. Something like this:

import data.real.basic
import algebra.group.pi

set_option pp.beta true

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

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

example (f : ℝ → ℝ) : (non_decreasing f) ↔ ∀ x y, x < y → f x ≤ f y :=
begin
  split,
  { intros hf x₁ x₂ h,
    apply hf,
    exact le_of_lt h },
  { intros h x₁ y₁ hf,
    replace hf := eq_or_lt_of_le hf,
    sorry,
  }
end

[Shadman Sakib]

Okay

[Shadman Sakib]

Helps with organization

[Shadman Sakib]

General question: How come sorry makes it so that I don't have to prove x_1 = y_1 implies my goal? I only had to prove the x_1 < y_1 case

[Adam Topaz]

I'm not sure what you mean... sorry is just a placeholder for a proof that should be filled in later.

[Bryan Gin-ge Chen]

You haven't proved it until you've removed all the sorrys!

[Adam Topaz]

I think what must have happened is that you did cases hf which gives you two separate goals, and the sorry killed the first goal, and only the second goal was left.

[Shadman Sakib]

Ahh I see

[Adam Topaz]

again, it's good practice to introduce { ... } immediately after the cases hf since you created new goals.

[Adam Topaz]

example (f : ℝ → ℝ) : (non_decreasing f) ↔ ∀ x y, x < y → f x ≤ f y :=
begin
  split,
  { intros hf x₁ x₂ h,
    apply hf,
    exact le_of_lt h },
  { intros h x₁ y₁ hf,
    replace hf := eq_or_lt_of_le hf,
    cases hf,
    { sorry },
    { sorry } }
end

[Adam Topaz]

So now the two sorry's are just placeholders for proofs that you still need to finish. And as you can see, there are two separate goals that need to be finished.

[Shadman Sakib]

Yeah, I see both now, thank you!