-- Module: Mathlib.Order.Monotone.Extension
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
The : ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)), ∃ (g : α → β), Monotone g ∧ EqOn f g s
The₁ The₂ :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    ∃ (g : α → β), Monotone g ∧ EqOn f g s
The₃ :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s), ∃ (g : α → β), Monotone g ∧ EqOn f g s
The₄ :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s) (x y : α) (hxy : x ≤ y), g x ≤ g y
neg :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s) (x y : α) (hxy : x ≤ y) (hx : Disjoint (Iic x) s) (hy : ¬Disjoint (Iic y) s),
      a ≤ sSup (f '' (Iic y ∩ s))
pos :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s) (x y : α) (hxy : x ≤ y) (hx : ¬Disjoint (Iic x) s) (hy : Disjoint (Iic y) s),
      sSup (f '' (Iic x ∩ s)) ≤ a
neg₁ :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s) (x y : α) (hxy : x ≤ y) (hx : ¬Disjoint (Iic x) s) (hy : ¬Disjoint (Iic y) s),
      sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
pos₁ :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s) (x y : α) (hxy : x ≤ y) (hx : ¬Disjoint (Iic x) s) (hy : Disjoint (Iic y) s),
      sSup (f '' (Iic x ∩ s)) ≤ a
neg₂ neg₃ :
  ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))),
    let g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s));
    ∀ (hgs : EqOn f g s) (x y : α) (hxy : x ≤ y) (hx : ¬Disjoint (Iic x) s) (hy : ¬Disjoint (Iic y) s),
      sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s

Tactic:
classical
    /- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
      of `f` to the left of `x` for `x ≥ a`. -/
    rcases hl with ⟨a, ha⟩
    have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x =>
      hu.mono (image_mono inter_subset_right)
    let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
    have hgs : EqOn f g s := by
      intro x hx
      simp only [g]
      have : IsGreatest (Iic x ∩ s) x := ⟨⟨self_mem_Iic, hx⟩, fun y hy => hy.1⟩
      rw [if_neg this.nonempty.not_disjoint,
        ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]
    refine ⟨g, fun x y hxy => ?_, hgs⟩
    by_cases hx : Disjoint (Iic x) s <;> by_cases hy : Disjoint (Iic y) s <;>
      simp only [g, if_pos, if_neg, not_false_iff, *, refl]
    · rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
      exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
    · exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
    · rw [not_disjoint_iff_nonempty_inter] at hx
      gcongr; exacts [hu' _, hx.image _]

Premises used: Set.not_disjoint_iff_nonempty_inter, if_pos, not_false_iff, refl, if_neg