Increasing on closed interval

Stream: new members

[Iocta]

There must be an easier way to do this?

import Mathlib.Data.Real.Basic
import Mathlib.Order.Interval.Set.Defs
import Mathlib.Order.Monotone.Basic
import Mathlib.Order.Basic
import Mathlib.Order.Defs.LinearOrder
import Mathlib.Topology.Basic
import Mathlib.Topology.Defs.Filter
import Mathlib.Topology.Instances.Real


lemma endpoint_characterization {a b : ℝ} (h : a ≤ b) (x : ℝ)
  (hx : x ∈ Set.Icc a b \ Set.Ioo a b) : x = a ∨ x = b := by
  have h_interval : x ∈ Set.Icc a b := hx.left
  have h_not_interior : x ∉ Set.Ioo a b := hx.right
  have h_cases : x = a ∨ x = b ∨ (a < x ∧ x < b) := by
    simp_all only [Set.Icc_diff_Ioo_same, Set.mem_insert_iff, Set.mem_singleton_iff, Set.mem_Icc, Set.mem_Ioo,]
    simp_all only [not_and, not_lt, or_false]
  rcases h_cases with (ha | hb | hinterior)
  · exact Or.inl ha
  · exact Or.inr hb
  · have contra : ¬(a < x ∧ x < b) := h_not_interior
    contradiction


lemma c11e6 (f : ℝ → ℝ) (a b : ℝ) (a_le_b : a ≤ b)
    (hmono: MonotoneOn f (Set.Ioo a b))
    (hcont : ContinuousOn f (Set.Icc a b))
    : MonotoneOn f (Set.Icc a b) := by
  unfold MonotoneOn
  intros x hx x' hx' x_le_x'
  have hx_cases : x ∈ Set.Ioo a b ∨ (x ∈ Set.Icc a b \ Set.Ioo a b) := by
    apply Set.mem_or_mem_of_mem_union
    rw [Set.union_diff_self]
    exact Or.inr hx
  have hx'_cases : x' ∈ Set.Ioo a b ∨ (x' ∈ Set.Icc a b \ Set.Ioo a b) := by
    apply Set.mem_or_mem_of_mem_union
    rw [Set.union_diff_self]
    exact Or.inr hx'
  cases hx_cases with
  | inl hx_open => {
    cases hx'_cases with
    | inl hx'_open => apply hmono hx_open hx'_open x_le_x'
    | inr hx'_endpoints => {
        sorry
    }

  }
  | inr hx_endpoints => {
    have hxab : x = a ∨ x = b := by
      apply endpoint_characterization a_le_b x hx_endpoints
    cases hxab with
    | inl hxa => {
        rw [hxa]
        cases hx'_cases with
        | inl hx'_open => {
            by_contra h
            simp at h
            have hx'_between : a < x' ∧ x' < b := hx'_open
            have : ∃ x'', a < x'' ∧ x'' < x ∧ f x < f x'' := by
                sorry
            cases this with
            | intro x'' hx'' => {
                linarith
            }
        }
        | inr hx'_endpoints => sorry
    }
    | inr hxb => {
        have hx'b : x' = b := by sorry
        simp_all only [Set.mem_Icc, le_refl, and_self, Set.mem_Ioo, lt_self_iff_false, and_false,]
    }
  }

[Kevin Buzzard]

My effort for the easy one:

import Mathlib

lemma endpoint_characterization {a b : ℝ} (x : ℝ)
  (hx : x ∈ Set.Icc a b \ Set.Ioo a b) : x = a ∨ x = b := by
  simp at hx
  obtain ⟨⟨h1, h2⟩, h3⟩ := hx
  obtain h1 | rfl := h1.lt_or_eq
  · exact Or.inr (le_antisymm h2 <| h3 h1)
  · exact Or.inl rfl

[Matt Diamond]

maybe there's something useful in Mathlib.Topology.Order.Monotone

[Ruben Van de Velde]

import Mathlib

lemma endpoint_characterization {a b : ℝ} (x : ℝ)
    (hx : x ∈ Set.Icc a b \ Set.Ioo a b) : x = a ∨ x = b := by
  have hab : a ≤ b := by
    by_contra! hab
    rwa [Set.Icc_eq_empty_of_lt hab, Set.empty_diff, Set.mem_empty_iff_false] at hx
  rwa [Set.Icc_diff_Ioo_same hab, Set.mem_insert_iff, Set.mem_singleton_iff] at hx

[Ruben Van de Velde]

Oh, and you'd even found Set.Icc_diff_Ioo_same already