awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Monotone.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : γ → α
g : γ → β
simp_rw :
  (∀ ⦃a b : γ⦄, a ≤ b → (f a, g a) ≤ (f b, g b)) ↔ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b) ∧ ∀ ⦃a b : γ⦄, a ≤ b → g a ≤ g b
⊢ (Monotone (β := α × β) fun (x : γ) ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g
have simp_rw₁ : (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b ∧ g a ≤ g b) ↔ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b) ∧ ∀ ⦃a b : γ⦄, a ≤ b → g a ≤ g b
Tactic: simp_rw [Monotone, Prod.mk_le_mk, forall_and]
-- Lean 4 proof step from Mathlib.Order.Monotone.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a < b → Prod.map f g a < Prod.map f g b
have simp : a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
  (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
    (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd
Tactic: simp only [Prod.lt_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a
have simp : a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
  (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
    (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd
Tactic: simp only [Prod.lt_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
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)
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have rcases : ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)), ∃ (g : α → β), Monotone g ∧ EqOn f g s
Tactic: rcases hl with ⟨a, ha⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
Tactic: have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x =>
      hu.mono (image_mono inter_subset_right)
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
have this : IsGreatest (Iic x ∩ s) x
Tactic: have : IsGreatest (Iic x ∩ s) x := ⟨⟨self_mem_Iic, hx⟩, fun y hy => hy.1⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
have rw : f x = sSup (f '' (Iic x ∩ s))
Tactic: rw [if_neg this.nonempty.not_disjoint,
        ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
rw : f x = sSup (f '' (Iic x ∩ s))
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
have rw₁ : f x = f x
Tactic: rw [if_neg this.nonempty.not_disjoint,
        ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have hgs : EqOn f g s
Tactic: 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]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
have refine : ∀ (x y : α) (hxy : x ≤ y), g x ≤ g y
Tactic: refine ⟨g, fun x y hxy => ?_, hgs⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
have pos : ∀ (hx : Disjoint (Iic x) s), g x ≤ g y
Tactic: by_cases hx : Disjoint (Iic x) s
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
pos : ∀ (hx : Disjoint (Iic x) s), g x ≤ g y
⊢ g x ≤ g y
have neg : ∀ (hx : ¬Disjoint (Iic x) s), g x ≤ g y
Tactic: by_cases hx : Disjoint (Iic x) s
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
⊢ g x ≤ g y
have pos : ∀ (hy : Disjoint (Iic y) s), g x ≤ g y
Tactic: by_cases hy : Disjoint (Iic y) s
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
pos : ∀ (hy : Disjoint (Iic y) s), g x ≤ g y
⊢ g x ≤ g y
have neg : ∀ (hy : ¬Disjoint (Iic y) s), g x ≤ g y
Tactic: by_cases hy : Disjoint (Iic y) s
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
⊢ g x ≤ g y
have pos : ∀ (hy : Disjoint (Iic y) s), g x ≤ g y
Tactic: by_cases hy : Disjoint (Iic y) s
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
pos : ∀ (hy : Disjoint (Iic y) s), g x ≤ g y
⊢ g x ≤ g y
have neg : ∀ (hy : ¬Disjoint (Iic y) s), g x ≤ g y
Tactic: by_cases hy : Disjoint (Iic y) s
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
⊢ g x ≤ g y
have neg : a ≤ sSup (f '' (Iic y ∩ s))
Tactic: simp only [g, if_pos, if_neg, not_false_iff, *, refl]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
⊢ g x ≤ g y
have pos : sSup (f '' (Iic x ∩ s)) ≤ a
Tactic: simp only [g, if_pos, if_neg, not_false_iff, *, refl]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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
⊢ g x ≤ g y
have neg : sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
Tactic: simp only [g, if_pos, if_neg, not_false_iff, *, refl]
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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))
have neg : ∀ (z : α) (hz : z ∈ Iic y ∩ s), a ≤ sSup (f '' (Iic y ∩ s))
Tactic: rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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))
have hx₁ : (Iic x ∩ s).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter] at hx
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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 : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
have neg : BddAbove (f '' (Iic y ∩ s))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
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 : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
neg : BddAbove (f '' (Iic y ∩ s))
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
have neg₁ : (f '' (Iic x ∩ s)).Nonempty
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
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)
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have The : ∀ (a : β) (ha : a ∈ lowerBounds (f '' 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 _]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
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
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have The₁ : ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)) (hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ 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 _]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
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
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have 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
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 _]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
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
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have 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
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 _]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Monotone.Extension (goal)
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
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have 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))
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 _]
Cleared hypotheses: hl