awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)

Tactic:
have hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t) := by
    have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
    have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.restrict (Icc s t) f)
      hf_c.continuousOn.restrict hf_i.injOn.injective
    exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
⊢ Icc a b ⊆ Icc s t

Tactic:
have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : Icc a b ⊆ Icc s t
⊢ StrictAntiOn f (Icc a b)

Tactic:
replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : StrictAntiOn f (Icc a b)
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Icc a b)

Tactic:
replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Icc a b)
⊢ False

Tactic:
this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab

Premises used: Iff.mpr, Set.right_mem_Icc, le_of_lt, Set.left_mem_Icc, IsAntichain.not_lt
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Icc a b)
⊢ False

Tactic:
exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab

Premises used: Iff.mpr, Set.right_mem_Icc, le_of_lt, Set.left_mem_Icc, IsAntichain.not_lt
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
⊢ ∀ (h : StrictAntiOn f (Icc s t)), False

Tactic:
have (h : StrictAntiOn f (Icc s t)) : False := by
    have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
    replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
    replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
    exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
this : ∀ (h : StrictAntiOn f (Icc s t)), False
⊢ StrictMonoOn f (Icc s t)

Tactic:
replace hf_mono_st : StrictMonoOn f (Icc s t) := hf_mono_st.resolve_right this
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : ∀ (h : StrictAntiOn f (Icc s t)), False
hf_mono_st : StrictMonoOn f (Icc s t)
⊢ s ≤ x

Tactic:
have hsx : s ≤ x := min_le_right a x
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : ∀ (h : StrictAntiOn f (Icc s t)), False
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
⊢ y ≤ t

Tactic:
have hyt : y ≤ t := le_max_right b y
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : ∀ (h : StrictAntiOn f (Icc s t)), False
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
⊢ Icc x y ⊆ Icc s t

Tactic:
replace : Icc x y ⊆ Icc s t := Icc_subset_Icc hsx hyt
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : Icc x y ⊆ Icc s t
⊢ StrictMonoOn f (Icc x y)

Tactic:
replace : StrictMonoOn f (Icc x y) := StrictMonoOn.mono hf_mono_st this
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : StrictMonoOn f (Icc x y)
⊢ f x < f y

Tactic:
this (left_mem_Icc.mpr (le_of_lt hxy)) (right_mem_Icc.mpr (le_of_lt hxy)) hxy

Premises used: Iff.mpr, Set.right_mem_Icc, le_of_lt, Set.left_mem_Icc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : StrictMonoOn f (Icc x y)
⊢ f x < f y

Tactic:
exact this (left_mem_Icc.mpr (le_of_lt hxy)) (right_mem_Icc.mpr (le_of_lt hxy)) hxy

Premises used: Iff.mpr, Set.right_mem_Icc, le_of_lt, Set.left_mem_Icc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ Fact (a ≤ b)

Tactic:
have : Fact (a ≤ b) := ⟨hab⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
⊢ StrictMonoOn f (Icc a b)

Tactic:
StrictMono.of_restrict ?_

Premises used: StrictMono.of_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
refine : StrictMono ((Icc a b).restrict (π := fun (a : α) ↦ δ) f)
⊢ StrictMonoOn f (Icc a b)

Tactic:
refine StrictMono.of_restrict ?_

Premises used: StrictMono.of_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
set :
  let g := (Icc a b).restrict (π := fun (a : α) ↦ δ) f;
  StrictMono g
⊢ StrictMono ((Icc a b).restrict (π := fun (a : α) ↦ δ) f)

Tactic:
set g : Icc a b → δ := Set.restrict (Icc a b) f

Premises used: Set.Icc, Set.restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : (↑(Icc a b) : Type u) → δ := (Icc a b).restrict (π := fun (a : α) ↦ δ) f
⊢ g ⊥ ≤ g ⊤

Tactic:
aesop
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : (↑(Icc a b) : Type u) → δ := (Icc a b).restrict (π := fun (a : α) ↦ δ) f
⊢ g ⊥ ≤ g ⊤

Tactic:
have hgab : g ⊥ ≤ g ⊤ := by aesop
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : (↑(Icc a b) : Type u) → δ := (Icc a b).restrict (π := fun (a : α) ↦ δ) f
hgab : g ⊥ ≤ g ⊤
⊢ StrictMono g

Tactic:
Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.restrict hgab hf_i.injective

Premises used: Set.Mem, Set.InjOn.injective, ContinuousOn.restrict, Continuous.strictMono_of_inj_boundedOrder
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : (↑(Icc a b) : Type u) → δ := (Icc a b).restrict (π := fun (a : α) ↦ δ) f
hgab : g ⊥ ≤ g ⊤
⊢ StrictMono g

Tactic:
exact Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.restrict hgab hf_i.injective

Premises used: Set.InjOn.injective, ContinuousOn.restrict, Continuous.strictMono_of_inj_boundedOrder
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f b ≤ f a
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictAntiOn f (Icc a b)

Tactic:
ContinuousOn.strictMonoOn_of_injOn_Icc (δ := δᵒᵈ) hab hfab hf_c hf_i

Premises used: StrictAntiOn, ContinuousOn.strictMonoOn_of_injOn_Icc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictMonoOn f (Icc a b) ∨ StrictAntiOn f (Icc a b)

Tactic:
(le_total (f a) (f b)).imp
    (ContinuousOn.strictMonoOn_of_injOn_Icc hab · hf_c hf_i)
    (ContinuousOn.strictAntiOn_of_injOn_Icc hab · hf_c hf_i)

Premises used: le_total, ContinuousOn.strictMonoOn_of_injOn_Icc, Or.imp, ContinuousOn.strictAntiOn_of_injOn_Icc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
⊢ ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f

Tactic:
have H {c d : α} (hcd : c < d) : StrictMono f ∨ StrictAnti f :=
    (hf_c.continuousOn.strictMonoOn_of_injOn_Icc' hcd.le hf_i.injOn).imp
      (hf_c.strictMonoOn_of_inj_rigidity hf_i hcd)
      (hf_c.strictMonoOn_of_inj_rigidity (δ := δᵒᵈ) hf_i hcd)
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
h : Subsingleton α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
Or.inl <| Subsingleton.strictMono f

Premises used: Or.inl, Subsingleton.strictMono
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
h : Subsingleton α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
exact Or.inl <| Subsingleton.strictMono f

Premises used: Or.inl, Subsingleton.strictMono
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
h : Nontrivial α
inr : ∀ (a b : α) (hab : a < b), StrictMono f ∨ StrictAnti f
⊢ StrictMono f ∨ StrictAnti f

Tactic:
obtain ⟨a, b, hab⟩ := exists_pair_lt α

Premises used: exists_pair_lt
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
h : Nontrivial α
a b : α
hab : a < b
⊢ StrictMono f ∨ StrictAnti f

Tactic:
H hab
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
h : Nontrivial α
a b : α
hab : a < b
⊢ StrictMono f ∨ StrictAnti f

Tactic:
exact H hab
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
⊢ Subsingleton α ∨ Nontrivial α

Tactic:
cases subsingleton_or_nontrivial α with
  | inl h => exact Or.inl <| Subsingleton.strictMono f
  | inr h =>
    obtain ⟨a, b, hab⟩ := exists_pair_lt α
    exact H hab

Premises used: subsingleton_or_nontrivial, Or.inl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
haveI : ∀ (this : Inhabited (↑(Ioo a b) : Type u)), StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
haveI : Inhabited (Ioo a b) := Classical.inhabited_of_nonempty (nonempty_Ioo_subtype hab)
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited (↑(Ioo a b) : Type u)
g : (↑(Ioo a b) : Type u) → δ := (Ioo a b).restrict (π := fun (a : α) ↦ δ) f
⊢ StrictMono g ∨ StrictAnti g

Tactic:
have : StrictMono g ∨ StrictAnti g :=
    Continuous.strictMono_of_inj hf_c.restrict hf_i.injective
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this_1 : Inhabited (↑(Ioo a b) : Type u)
g : (↑(Ioo a b) : Type u) → δ := (Ioo a b).restrict (π := fun (a : α) ↦ δ) f
this : StrictMono g ∨ StrictAnti g
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr

Premises used: Iff.mpr, strictMono_restrict, Iff.mp, Or.imp, Set.strictAntiOn_iff_strictAnti
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this_1 : Inhabited (↑(Ioo a b) : Type u)
g : (↑(Ioo a b) : Type u) → δ := (Ioo a b).restrict (π := fun (a : α) ↦ δ) f
this : StrictMono g ∨ StrictAnti g
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr

Premises used: Iff.mpr, strictMono_restrict, Iff.mp, Or.imp, Set.strictAntiOn_iff_strictAnti
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
rcases : ∀ (a' : α) (ha' : a' ∈ s), ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Tactic:
rcases hs with ⟨a', ha'⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
inl : ∀ (ha : IsLUB s a') (h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun (x : α) ↦ x ∈ s) x), False
inr : ∀ (ha'a : a' < a), False
⊢ False

Tactic:
rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)

Premises used: LE.le.eq_or_lt, And.left, rfl
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun (x : α) ↦ x ∈ s) x
⊢ False

Tactic:
h.self_of_nhdsWithin le_rfl ha'

Premises used: Filter.Eventually.self_of_nhdsWithin, le_rfl