awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a b : X
ha : a ∈ s
hb : b ∈ s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
hb' : g b ≤ f b
⊢ ∃ x ∈ s, f x = g x

Tactic:
let ⟨x, hx⟩ :=
    @intermediate_value_univ₂ s α _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ ⟨b, hb⟩ _ _
      (continuousOn_iff_continuous_restrict.1 hf) (continuousOn_iff_continuous_restrict.1 hg) ha'
      hb'
  ⟨x, x.2, hx⟩

Premises used: Membership.mem, Exists, intermediate_value_univ₂, And, continuousOn_iff_continuous_restrict, And.intro, Exists.intro, Iff.mp, _private.0.IsPreconnected.intermediate_value₂.match_1, Subtype.val, Eq, Subtype.property
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
⊢ f a ≤ g a

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
ha'₁ : f a ≤ g a
⊢ g ≤ᶠ[l] f

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
obtain :
  ∀ (b : (↑s : Type u)) (h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b),
    ∃ x ∈ s, f x = g x
⊢ ∃ x ∈ s, f x = g x

Tactic:
obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
      (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)

Premises used: intermediate_value_univ₂_eventually₁, Filter.Eventually.comap
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : (↑s : Type u)
h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b
⊢ ∃ x ∈ s, f x = g x

Tactic:
⟨b, b.prop, h⟩

Premises used: Subtype.prop, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : (↑s : Type u)
h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b
⊢ ∃ x ∈ s, f x = g x

Tactic:
exact ⟨b, b.prop, h⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
⊢ f ≤ᶠ[l₁] g

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
he₃ : f ≤ᶠ[l₁] g
⊢ g ≤ᶠ[l₂] f

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
obtain :
  ∀ (b : (↑s : Type u)) (h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b),
    ∃ x ∈ s, f x = g x
⊢ ∃ x ∈ s, f x = g x

Tactic:
obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
      (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg
      (he₁.comap _) (he₂.comap _)

Premises used: intermediate_value_univ₂_eventually₂, Filter.Eventually.comap
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
b : (↑s : Type u)
h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b
⊢ ∃ x ∈ s, f x = g x

Tactic:
⟨b, b.prop, h⟩

Premises used: Subtype.prop, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
b : (↑s : Type u)
h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b
⊢ ∃ x ∈ s, f x = g x

Tactic:
exact ⟨b, b.prop, h⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a b : X
ha : a ∈ s
hb : b ∈ s
f : X → α
hf : ContinuousOn f s
⊢ Icc (f a) (f b) ⊆ f '' s

Tactic:
fun _x hx =>
  hs.intermediate_value₂ ha hb hf continuousOn_const hx.1 hx.2

Premises used: Set.Mem, setOf, continuousOn_const, IsPreconnected.intermediate_value₂, Set.Subset, And.right, And.left, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
v : α
ht : Tendsto f l (𝓝 v)
⊢ Ico (f a) v ⊆ f '' s

Tactic:
fun _ h =>
  hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h.1 (ht.eventually_const_le h.2)

Premises used: Filter.Tendsto.eventually_const_le, Set.Mem, setOf, continuousOn_const, Set.Subset, And.right, And.left, IsPreconnected.intermediate_value₂_eventually₁, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
v : α
ht : Tendsto f l (𝓝 v)
⊢ Ioc v (f a) ⊆ f '' s

Tactic:
fun _ h =>
  (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h.2
    (ht.eventually_le_const h.1)).imp fun _ h => h.imp_right Eq.symm

Premises used: Set.Mem, setOf, continuousOn_const, Filter.Tendsto.eventually_le_const, Exists.imp, Set.Subset, And.right, And.left, IsPreconnected.intermediate_value₂_eventually₁, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
v₁ v₂ : α
ht₁ : Tendsto f l₁ (𝓝 v₁)
ht₂ : Tendsto f l₂ (𝓝 v₂)
⊢ Ioo v₁ v₂ ⊆ f '' s

Tactic:
fun _ h =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const
    (ht₁.eventually_le_const h.1) (ht₂.eventually_const_le h.2)

Premises used: Filter.Tendsto.eventually_const_le, Set.Mem, setOf, continuousOn_const, IsPreconnected.intermediate_value₂_eventually₂, Filter.Tendsto.eventually_le_const, Set.Subset, And.right, And.left, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
ht : Tendsto f l atTop
⊢ Ici (f a) ⊆ f '' s

Tactic:
fun y h =>
  hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h (tendsto_atTop.1 ht y)

Premises used: Set.Mem, setOf, continuousOn_const, Filter.tendsto_atTop, Set.Subset, IsPreconnected.intermediate_value₂_eventually₁, Iff.mp, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
ht : Tendsto f l atBot
⊢ Iic (f a) ⊆ f '' s

Tactic:
fun y h =>
  (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h (tendsto_atBot.1 ht y)).imp
    fun _ h => h.imp_right Eq.symm

Premises used: Set.Mem, setOf, continuousOn_const, Exists.imp, Set.Subset, Filter.tendsto_atBot, IsPreconnected.intermediate_value₂_eventually₁, Iff.mp, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
v : α
ht₁ : Tendsto f l₁ (𝓝 v)
ht₂ : Tendsto f l₂ atTop
⊢ Ioi v ⊆ f '' s

Tactic:
fun y h =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const
    (ht₁.eventually_le_const h) (ht₂.eventually_ge_atTop y)

Premises used: Set.Mem, setOf, continuousOn_const, IsPreconnected.intermediate_value₂_eventually₂, Filter.Tendsto.eventually_le_const, Set.Subset, Set.image, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
v : α
ht₁ : Tendsto f l₁ atBot
ht₂ : Tendsto f l₂ (𝓝 v)
⊢ Iio v ⊆ f '' s

Tactic:
fun y h =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y)
    (ht₂.eventually_const_le h)

Premises used: Filter.Tendsto.eventually_const_le, Set.Mem, setOf, continuousOn_const, IsPreconnected.intermediate_value₂_eventually₂, Filter.Tendsto.eventually_le_atBot, Set.Subset, Set.image
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f : X → α
hf : ContinuousOn f s
ht₁ : Tendsto f l₁ atBot
ht₂ : Tendsto f l₂ atTop
⊢ univ ⊆ f '' s

Tactic:
fun y _ =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y)
    (ht₂.eventually_ge_atTop y)

Premises used: Set.Mem, setOf, continuousOn_const, IsPreconnected.intermediate_value₂_eventually₂, Filter.Tendsto.eventually_le_atBot, Set.Subset, Set.image, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a b : X
f : X → α
hf : Continuous[inst, inst_2] f
⊢ Icc (f a) (f b) ⊆ range f

Tactic:
fun _ hx => intermediate_value_univ₂ hf continuous_const hx.1 hx.2

Premises used: Set.Mem, continuous_const, setOf, Set.Subset, intermediate_value_univ₂, And.right, And.left, Set.range
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
c : α
f : X → α
hf : Continuous[inst, inst_2] f
h₁ : ∃ (a : X), f a ≤ c
h₂ : ∃ (b : X), c ≤ f b
⊢ c ∈ range f

Tactic:
let ⟨a, ha⟩ := h₁; let ⟨b, hb⟩ := h₂; intermediate_value_univ a b hf ⟨ha, hb⟩

Premises used: _private.0.mem_range_of_exists_le_of_exists_ge.match_2, Membership.mem, _private.0.mem_range_of_exists_le_of_exists_ge.match_1, And.intro, intermediate_value_univ, Set.range
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
simpa only [image_id] using hs.intermediate_value ha hb continuousOn_id

Premises used: IsPreconnected.intermediate_value, continuousOn_id, Set.image_id
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
h : IsPreconnected s
⊢ s.OrdConnected

Tactic:
⟨fun _ hx _ hy => h.Icc_subset hx hy⟩

Premises used: Set.OrdConnected.mk, IsPreconnected.Icc_subset
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsConnected s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
hs.2.Icc_subset ha hb

Premises used: And.right, IsPreconnected.Icc_subset
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s = univ

Tactic:
eq_univ_of_forall fun x => ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
refine : ∀ (x : α), x ∈ s
⊢ s = univ

Tactic:
refine eq_univ_of_forall fun x => ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
⊢ ∃ y ∈ s, y < x

Tactic:
not_bddBelow_iff.1 hb x

Premises used: not_bddBelow_iff, Iff.mp
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
obtain : ∀ (y : α) (ys : y ∈ s) (hy : y < x), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, y < x := not_bddBelow_iff.1 hb x

Premises used: not_bddBelow_iff, Iff.mp
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
⊢ ∃ z ∈ s, x < z

Tactic:
not_bddAbove_iff.1 ha x

Premises used: Iff.mp, not_bddAbove_iff
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
obtain : ∀ (z : α) (zs : z ∈ s) (hz : x < z), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x

Premises used: Iff.mp, not_bddAbove_iff
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
z : α
zs : z ∈ s
hz : x < z
⊢ x ∈ s

Tactic:
hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩

Premises used: le_of_lt, And.intro, IsPreconnected.Icc_subset
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
z : α
zs : z ∈ s
hz : x < z
⊢ x ∈ s

Tactic:
exact hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩

Premises used: le_of_lt, And.intro, IsPreconnected.Icc_subset
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : PreconnectedSpace α
x y : α
hxy : x < y
this : (Iio y ∩ Ioi x).Nonempty
⊢ ∃ (a : α), x < a ∧ a < y

Tactic:
grind [Set.inter_nonempty_iff_exists_left]

Premises used: Set.inter_nonempty_iff_exists_left
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : PreconnectedSpace α
x y : α
hxy : x < y
suffices : (Iio y ∩ Ioi x).Nonempty
⊢ ∃ (a : α), x < a ∧ a < y

Tactic:
suffices (Iio y ∩ Ioi x).Nonempty by grind [Set.inter_nonempty_iff_exists_left]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : PreconnectedSpace α
x y : α
hxy : x < y
⊢ (Iio y ∩ Ioi x).Nonempty

Tactic:
nonempty_inter (isOpen_Iio' y) (isOpen_Ioi' x) (Set.Iio_union_Ioi_of_lt hxy)
      ⟨x, Set.mem_Iio.mpr hxy⟩ ⟨y, Set.mem_Ioi.mpr hxy⟩

Premises used: Iff.mpr, Set.mem_Iio, isOpen_Iio', Set.Iio_union_Ioi_of_lt, Set.mem_Ioi, nonempty_inter, Exists.intro, isOpen_Ioi'
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : PreconnectedSpace α
x y : α
hxy : x < y
⊢ (Iio y ∩ Ioi x).Nonempty

Tactic:
exact nonempty_inter (isOpen_Iio' y) (isOpen_Ioi' x) (Set.Iio_union_Ioi_of_lt hxy)
      ⟨x, Set.mem_Iio.mpr hxy⟩ ⟨y, Set.mem_Ioi.mpr hxy⟩

Premises used: Iff.mpr, Set.mem_Iio, isOpen_Iio', Set.Iio_union_Ioi_of_lt, Set.mem_Ioi, nonempty_inter, Exists.intro, isOpen_Ioi'