awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s
have 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
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
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
⊢ ∃ (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),
    sSup (f '' (Iic x ∩ s)) ≤ 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
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ MonovaryOrder f g a b ∨ a = b ∨ MonovaryOrder f g b a
have h : a = b ↔ (f a, g a, a) = (f b, g b, b)
Tactic: convert! trichotomous_of (Prod.Lex (· < ·) <| Prod.Lex (· < ·) WellOrderingRel) _ _
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
h : a = b ↔ (f a, g a, a) = (f b, g b, b)
⊢ MonovaryOrder f g a b ∨ a = b ∨ MonovaryOrder f g b a
have convert_6 : Std.Trichotomous (α := α × β × ι)
  (Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel))
Tactic: convert! trichotomous_of (Prod.Lex (· < ·) <| Prod.Lex (· < ·) WellOrderingRel) _ _
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ a = b ↔ (f a, g a, a) = (f b, g b, b)
have h : (a = b → f a = f b) ∧ (a = b → g a = g b)
Tactic: simp only [Prod.ext_iff, ← and_assoc, imp_and, iff_and_self]
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
have refine_1 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
Tactic: refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
refine_1 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
have refine_2 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
Tactic: refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
refine_1 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
refine_2 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
have refine_3 : (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
Tactic: refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ f i ≤ f j
have refine_1 : ∀ (h : (f i, g i, i).1 < (f j, g j, j).1), f i ≤ f j
Tactic: obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
refine_1 : ∀ (h : (f i, g i, i).1 < (f j, g j, j).1), f i ≤ f j
⊢ f i ≤ f j
have refine_1₁ : ∀ (h : (f i, g i, i).1 = (f j, g j, j).1), f i ≤ f j
Tactic: obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ g i ≤ g j
have refine_2 : ∀ (h : (f i, g i, i).1 < (f j, g j, j).1), g i ≤ g j
Tactic: obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
refine_2 : ∀ (h : (f i, g i, i).1 < (f j, g j, j).1), g i ≤ g j
⊢ g i ≤ g j
have refine_2₁ : ∀ (h : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2), g i ≤ g j
Tactic: obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
⊢ g i ≤ g j
have refine_2 : ∀ (h : (f i, g i, i).2.1 < (f j, g j, j).2.1), g i ≤ g j
Tactic: obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
refine_2 : ∀ (h : (f i, g i, i).2.1 < (f j, g j, j).2.1), g i ≤ g j
⊢ g i ≤ g j
have refine_2₁ : ∀ (h : (f i, g i, i).2.1 = (f j, g j, j).2.1), g i ≤ g j
Tactic: obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
letI letI₁ letI₂ : MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
have refine_1 : let this := linearOrderOfSTO (MonovaryOrder f g);
∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
Tactic: classical
  letI := linearOrderOfSTO (MonovaryOrder f g)
  refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
  · obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
  · obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
    · exact hfg.symm hi hj h
    obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
  · rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
letI letI₁ letI₂ : MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
refine_1 :
  let this := linearOrderOfSTO (MonovaryOrder f g);
  ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
have refine_2 : let this := linearOrderOfSTO (MonovaryOrder f g);
∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
Tactic: classical
  letI := linearOrderOfSTO (MonovaryOrder f g)
  refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
  · obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
  · obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
    · exact hfg.symm hi hj h
    obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
  · rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
letI letI₁ letI₂ : MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
refine_1 :
  let this := linearOrderOfSTO (MonovaryOrder f g);
  ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
refine_2 :
  let this := linearOrderOfSTO (MonovaryOrder f g);
  ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
have refine_3 : (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
Tactic: classical
  letI := linearOrderOfSTO (MonovaryOrder f g)
  refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
  · obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
  · obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
    · exact hfg.symm hi hj h
    obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
  · rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
have simp_rw : MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
  ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
Tactic: simp_rw [← monovaryOn_toDual_right, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
simp_rw :
  MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
    ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
⊢ AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
have simp_rw₁ : (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn (β := βᵒᵈ) ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s) ↔
  ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
Tactic: simp_rw [← monovaryOn_toDual_right, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
have simp_rw : AntivaryOn (α := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔
  ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
Tactic: simp_rw [← antivaryOn_toDual_left, antivaryOn_iff_exists_monotoneOn_antitoneOn,
    monotoneOn_toDual_comp_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
simp_rw :
  AntivaryOn (α := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔
    ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
have simp_rw₁ : (∃ (x : LinearOrder ι), MonotoneOn (β := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s ∧ AntitoneOn g s) ↔
  ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
Tactic: simp_rw [← antivaryOn_toDual_left, antivaryOn_iff_exists_monotoneOn_antitoneOn,
    monotoneOn_toDual_comp_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
have simp_rw : MonovaryOn (α := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔
  ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
Tactic: simp_rw [← monovaryOn_toDual_left, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.MonovaryOrder (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
simp_rw :
  MonovaryOn (α := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔
    ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
⊢ AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
have simp_rw₁ : (∃ (x : LinearOrder ι), MonotoneOn (β := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s ∧ MonotoneOn g s) ↔
  ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
Tactic: simp_rw [← monovaryOn_toDual_left, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Odd (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
⊢ StrictMono f
have refine : ∀ (x : G) (hx : Membership.mem (γ := Set G) (Iic 0) x) (y : G) (hy : Membership.mem (γ := Set G) (Iic 0) y)
  (hxy : x < y), -f y < -f x
Tactic: refine StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 ?_) h₂
-- Lean 4 proof step from Mathlib.Order.Monotone.Odd (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x < y
⊢ -f y < -f x
have rw : f (-y) < f (-x)
Tactic: rw [← h₁, ← h₁]
-- Lean 4 proof step from Mathlib.Order.Monotone.Odd (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f
have refine : ∀ (x : G) (hx : Membership.mem (γ := Set G) (Iic 0) x) (y : G) (hy : Membership.mem (γ := Set G) (Iic 0) y)
  (hxy : x ≤ y), -f y ≤ -f x
Tactic: refine MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂
-- Lean 4 proof step from Mathlib.Order.Monotone.Odd (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x ≤ y
⊢ -f y ≤ -f x
have rw : f (-y) ≤ f (-x)
Tactic: rw [← h₁, ← h₁]
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
⊢ x ∈ s
have inl : x ∈ s → x ∈ s
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
inl : x ∈ s → x ∈ s
⊢ x ∈ s
have inr : x ∈ t → x ∈ s
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
⊢ x ∈ s
have inr : ∀ (hs : IsGreatest s x) (ht : IsLeast t x) (hxc : x ≤ x), x ∈ s
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
Cleared hypotheses: c, hs, ht, hxc
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
inr : ∀ (hs : IsGreatest s x) (ht : IsLeast t x) (hxc : x ≤ x), x ∈ s
⊢ x ∈ s
have inr₁ : ∀ (h'x : x < c), x ∈ s
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ StrictMonoOn f (s ∪ t)
have A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
Tactic: have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
    intro x hx hxc
    cases hx
    · assumption
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact hs.1
    exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
-- Lean 4 proof step from Mathlib.Order.Monotone.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t
have inl : ∀ (hx : c ∈ s ∪ t) (hxc : c ≤ c) (hx : c ∈ s), c ∈ t
Tactic: rcases eq_or_lt_of_le hxc with (rfl | h'x)
Cleared hypotheses: x, hx_1, hxc, hx