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 δ
a b : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Ioc (f b) (f a) ⊆ f '' Ico a b

Tactic:
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_lt_of_ge (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioc _ _ _ _ _ _ _ isPreconnected_Ico _ _ ⟨refl a, hlt⟩
      (right_nhdsWithin_Ico_neBot hlt) inf_le_right _ (hf.mono Ico_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ico_subset_Icc_self)

Premises used: Set.Ico_subset_Icc_self, inf_le_right, Eq.rec, isPreconnected_Ico, eq_or_lt_of_le, absurd, IsPreconnected.intermediate_value_Ioc, And.right, ContinuousWithinAt.mono, And.left, And.intro, ContinuousOn.mono, Or.elim, refl, ContinuousOn.continuousWithinAt, not_lt_of_ge
-- 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 : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Ioc (f a) (f b) ⊆ f '' Ioc a b

Tactic:
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_le_of_gt (he ▸ h.1))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioc _ _ _ _ _ _ _ isPreconnected_Ioc _ _ ⟨hlt, refl b⟩
      (left_nhdsWithin_Ioc_neBot hlt) inf_le_right _ (hf.mono Ioc_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioc_subset_Icc_self)

Premises used: Set.Ioc_subset_Icc_self, inf_le_right, Eq.rec, eq_or_lt_of_le, isPreconnected_Ioc, absurd, IsPreconnected.intermediate_value_Ioc, And.right, ContinuousWithinAt.mono, And.left, And.intro, ContinuousOn.mono, not_le_of_gt, Or.elim, refl, ContinuousOn.continuousWithinAt
-- 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 : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Ico (f b) (f a) ⊆ f '' Ioc a b

Tactic:
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_le_of_gt (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ico _ _ _ _ _ _ _ isPreconnected_Ioc _ _ ⟨hlt, refl b⟩
      (left_nhdsWithin_Ioc_neBot hlt) inf_le_right _ (hf.mono Ioc_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioc_subset_Icc_self)

Premises used: IsPreconnected.intermediate_value_Ico, Set.Ioc_subset_Icc_self, inf_le_right, Eq.rec, eq_or_lt_of_le, isPreconnected_Ioc, absurd, And.right, ContinuousWithinAt.mono, And.left, And.intro, ContinuousOn.mono, not_le_of_gt, Or.elim, refl, ContinuousOn.continuousWithinAt
-- 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 : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Ioo (f a) (f b) ⊆ f '' Ioo a b

Tactic:
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_lt_of_gt (he ▸ h.1))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _ isPreconnected_Ioo _ _
      (left_nhdsWithin_Ioo_neBot hlt) (right_nhdsWithin_Ioo_neBot hlt) inf_le_right inf_le_right _
      (hf.mono Ioo_subset_Icc_self) _ _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ioo_subset_Icc_self)

Premises used: Set.Ioo_subset_Icc_self, IsPreconnected.intermediate_value_Ioo, inf_le_right, Eq.rec, eq_or_lt_of_le, isPreconnected_Ioo, absurd, And.right, ContinuousWithinAt.mono, And.left, And.intro, not_lt_of_gt, ContinuousOn.mono, Or.elim, refl, ContinuousOn.continuousWithinAt
-- 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 : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Ioo (f b) (f a) ⊆ f '' Ioo a b

Tactic:
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_lt_of_gt (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _ isPreconnected_Ioo _ _
      (right_nhdsWithin_Ioo_neBot hlt) (left_nhdsWithin_Ioo_neBot hlt) inf_le_right inf_le_right _
      (hf.mono Ioo_subset_Icc_self) _ _
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ioo_subset_Icc_self)
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)

Premises used: Set.Ioo_subset_Icc_self, IsPreconnected.intermediate_value_Ioo, inf_le_right, Eq.rec, eq_or_lt_of_le, isPreconnected_Ioo, absurd, And.right, ContinuousWithinAt.mono, And.left, And.intro, not_lt_of_gt, ContinuousOn.mono, Or.elim, refl, ContinuousOn.continuousWithinAt
-- 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 δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ SurjOn f s (Icc (f a) (f b))

Tactic:
hs.isPreconnected.intermediate_value ha hb hf

Premises used: Set.SurjOn, Set.OrdConnected.isPreconnected, IsPreconnected.intermediate_value
-- 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 δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
inl : ∀ (hab : f a ≤ f b), SurjOn f s [[f a, f b]]
inr : ∀ (hab : f b ≤ f a), SurjOn f s [[f a, f b]]
⊢ SurjOn f s [[f a, f b]]

Tactic:
rcases le_total (f a) (f b) with hab | hab

Premises used: le_total
-- 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 δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f a ≤ f b
⊢ SurjOn f s [[f a, f b]]

Tactic:
simp [hf.surjOn_Icc, *]

Premises used: ContinuousOn.surjOn_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 δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f b ≤ f a
⊢ SurjOn f s [[f a, f b]]

Tactic:
simp [hf.surjOn_Icc, *]

Premises used: ContinuousOn.surjOn_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 : Continuous[inst, inst_5] f
h_top : Tendsto f atTop atTop
h_bot : Tendsto f atBot atBot
⊢ Surjective f

Tactic:
fun p =>
  mem_range_of_exists_le_of_exists_ge hf (h_bot.eventually (eventually_le_atBot p)).exists
    (h_top.eventually (eventually_ge_atTop p)).exists

Premises used: Set.Mem, setOf, Filter.Eventually.exists, Filter.Tendsto.eventually, Filter.eventually_ge_atTop, Filter.eventually_le_atBot, Set.range, mem_range_of_exists_le_of_exists_ge, Function.Surjective
-- 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 : Continuous[inst, inst_5] f
h_top : Tendsto f atBot atTop
h_bot : Tendsto f atTop atBot
⊢ Surjective f

Tactic:
Continuous.surjective (α := αᵒᵈ) hf h_top h_bot

Premises used: Continuous.surjective, OrderDual
-- 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 : α → δ
s : Set α
inst_7 : s.OrdConnected
hs : s.Nonempty
hf : ContinuousOn f s
hbot : Tendsto.{u, u_1} (β := δ) (fun (x : (↑s : Type u)) ↦ f (↑x : α)) atBot atBot
htop : Tendsto.{u, u_1} (β := δ) (fun (x : (↑s : Type u)) ↦ f (↑x : α)) atTop atTop
⊢ SurjOn f s univ

Tactic:
haveI := Classical.inhabited_of_nonempty hs.to_subtype
  surjOn_iff_surjective.2 <| hf.restrict.surjective htop hbot

Premises used: Iff.mpr, Set.surjOn_iff_surjective, Continuous.surjective, ContinuousOn.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 δ
f : α → δ
s : Set α
inst_7 : s.OrdConnected
hs : s.Nonempty
hf : ContinuousOn f s
hbot : Tendsto.{u, u_1} (β := δ) (fun (x : (↑s : Type u)) ↦ f (↑x : α)) atBot atTop
htop : Tendsto.{u, u_1} (β := δ) (fun (x : (↑s : Type u)) ↦ f (↑x : α)) atTop atBot
⊢ SurjOn f s univ

Tactic:
ContinuousOn.surjOn_of_tendsto (δ := δᵒᵈ) hs hf hbot htop

Premises used: ContinuousOn.surjOn_of_tendsto, OrderDual
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
by_contra! : ∀ (h : f b ≤ f a), False
⊢ f a < f b

Tactic:
by_contra! h
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
⊢ f b < f a

Tactic:
have H : f b < f a := lt_of_le_of_ne h <| hf_i.ne hab.ne'
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
pos : ∀ (ha : f a ≤ f ⊥), False
neg : ∀ (ha : f ⊥ < f a), False
⊢ False

Tactic:
by_cases! ha : f a ≤ f ⊥

Premises used: Bot.bot
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f a ≤ f ⊥
pos : ∀ (u : α) (hu : u ∈ Ioc b ⊤ ∧ f u = f ⊥), False
⊢ False

Tactic:
obtain ⟨u, hu⟩ := intermediate_value_Ioc le_top hf_c.continuousOn ⟨H.trans_le ha, hf⟩

Premises used: Continuous.continuousOn, LT.lt.trans_le, le_top, And.intro, intermediate_value_Ioc
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f a ≤ f ⊥
u : α
hu : u ∈ Ioc b ⊤ ∧ f u = f ⊥
⊢ u = ⊥

Tactic:
have : u = ⊥ := hf_i hu.2
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f a ≤ f ⊥
u : α
hu : u ∈ Ioc b ⊤ ∧ f u = f ⊥
this : u = ⊥
⊢ False

Tactic:
simp_all
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
pos : ∀ (hb : f ⊥ < f b), False
neg : ∀ (hb : f b ≤ f ⊥), False
⊢ False

Tactic:
by_cases! hb : f ⊥ < f b

Premises used: Bot.bot
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
pos : ∀ (u : α) (hu : u ∈ Ioo ⊥ a ∧ f u = f b), False
⊢ False

Tactic:
obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩

Premises used: Continuous.continuousOn, intermediate_value_Ioo, And.intro, bot_le
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : u ∈ Ioo ⊥ a ∧ f u = f b
⊢ b ∈ Ioo ⊥ a ∧ f b = f b

Tactic:
rw [hf_i hu.2] at hu

Premises used: And.right
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : b ∈ Ioo ⊥ a ∧ f b = f b
⊢ False

Tactic:
(hab.trans hu.1.2).false

Premises used: And.right, And.left, LT.lt.trans, LT.lt.false
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : b ∈ Ioo ⊥ a ∧ f b = f b
⊢ False

Tactic:
exact (hab.trans hu.1.2).false

Premises used: And.right, And.left, LT.lt.trans, LT.lt.false
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b ≤ f ⊥
⊢ f b < f ⊥

Tactic:
replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b < f ⊥
neg : ∀ (u : α) (hu : u ∈ Ioo a b ∧ f u = f ⊥), False
⊢ False

Tactic:
obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩

Premises used: Continuous.continuousOn, intermediate_value_Ioo', LT.lt.le, And.intro
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b < f ⊥
u : α
hu : u ∈ Ioo a b ∧ f u = f ⊥
⊢ u = ⊥

Tactic:
have : u = ⊥ := hf_i hu.2
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b < f ⊥
u : α
hu : u ∈ Ioo a b ∧ f u = f ⊥
this : u = ⊥
⊢ False

Tactic:
simp_all
-- 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊤ ≤ f ⊥
hf_i : Injective f
⊢ StrictAnti f

Tactic:
hf_c.strictMono_of_inj_boundedOrder (δ := δᵒᵈ) hf hf_i

Premises used: StrictAnti, 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 δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
⊢ StrictMono f ∨ StrictAnti f

Tactic:
(le_total (f ⊥) (f ⊤)).imp
    (hf_c.strictMono_of_inj_boundedOrder · hf_i)
    (hf_c.strictAnti_of_inj_boundedOrder · hf_i)

Premises used: Bot.bot, le_total, Continuous.strictMono_of_inj_boundedOrder, Continuous.strictAnti_of_inj_boundedOrder, Or.imp, Top.top
-- 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
⊢ s ≤ a

Tactic:
have hsa : s ≤ a := min_le_left 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
⊢ b ≤ t

Tactic:
have hbt : b ≤ t := le_max_left 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
⊢ Fact (s ≤ t)

Tactic:
have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
-- 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 : Fact (s ≤ t)
⊢ StrictMono ((Icc s t).restrict (π := fun (a : α) ↦ δ) f) ∨ StrictAnti ((Icc s t).restrict (π := fun (a : α) ↦ δ) f)

Tactic:
have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.restrict (Icc s t) f)
      hf_c.continuousOn.restrict hf_i.injOn.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 δ
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_1 : Fact (s ≤ t)
this :
  StrictMono ((Icc s t).restrict (π := fun (a : α) ↦ δ) f) ∨ StrictAnti ((Icc s t).restrict (π := fun (a : α) ↦ δ) f)
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)

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 δ
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_1 : Fact (s ≤ t)
this :
  StrictMono ((Icc s t).restrict (π := fun (a : α) ↦ δ) f) ∨ StrictAnti ((Icc s t).restrict (π := fun (a : α) ↦ δ) f)
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)

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