awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
inr : ∀ x ∈ K, f x' x < z
⊢ sSup (f x' '' K) < z

Tactic:
rw [hK.sSup_lt_iff_of_continuous h0K
        (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn]

Premises used: Continuous.continuousOn, IsCompact.sSup_lt_iff_of_continuous, Continuous.comp, Continuous.prodMk_right
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ x ∈ K, f x' x < z

Tactic:
fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, Set.mk_mem_prod
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ x ∈ K, f x' x < z

Tactic:
exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sInf (f x '' K)

Tactic:
IsCompact.continuous_sSup (α := αᵒᵈ) hK hf

Premises used: IsCompact.continuous_sSup, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
⊢ f '' Icc a b = Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))

Tactic:
eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, isPreconnected_Icc.image f h⟩
    (isCompact_Icc.image_of_continuousOn h)

Premises used: Iff.mpr, IsPreconnected.image, Set.nonempty_Icc, isPreconnected_Icc, CompactIccSpace.isCompact_Icc, eq_Icc_of_connected_compact, Set.Nonempty.image, IsCompact.image_of_continuousOn, And.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ f '' [[a, b]] = Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))

Tactic:
image_Icc min_le_max h

Premises used: min_le_max, ContinuousOn.image_Icc, Set.uIcc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm

Premises used: Set.uIcc_of_le, ContinuousOn.image_uIcc_eq_Icc, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
refine : sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
⊢ f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
refine h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm

Premises used: Set.uIcc_of_le, ContinuousOn.image_uIcc_eq_Icc, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])

Tactic:
csInf_le_csSup (nonempty_uIcc.image _) ?_ ?_

Premises used: csInf_le_csSup, Set.Nonempty.image, Set.nonempty_uIcc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
refine_1 : BddBelow (f '' [[a, b]])
refine_2 : BddAbove (f '' [[a, b]])
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])

Tactic:
refine csInf_le_csSup (nonempty_uIcc.image _) ?_ ?_

Premises used: csInf_le_csSup, Set.Nonempty.image, Set.nonempty_uIcc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
refine_1 : BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
⊢ BddBelow (f '' [[a, b]])

Tactic:
rw [h.image_uIcc_eq_Icc]

Premises used: ContinuousOn.image_uIcc_eq_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
refine_2 : BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
⊢ BddAbove (f '' [[a, b]])

Tactic:
rw [h.image_uIcc_eq_Icc]

Premises used: ContinuousOn.image_uIcc_eq_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
bddBelow_Icc

Premises used: bddBelow_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
bddAbove_Icc

Premises used: bddAbove_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
exacts [bddBelow_Icc, bddAbove_Icc]

Premises used: bddAbove_Icc, bddBelow_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ f c ∈ f '' Icc a b

Tactic:
have := mem_image_of_mem f hc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))

Tactic:
rw [h.image_Icc (hc.1.trans hc.2)] at this

Premises used: ContinuousOn.image_Icc, And.right, And.left, LE.le.trans
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
rw : Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b)) = Icc (f a) (f b)
⊢ f '' Icc a b = Icc (f a) (f b)

Tactic:
rw [h.image_Icc hab]

Premises used: ContinuousOn.image_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
h₁ : sInf (f '' Icc a b) = f a
h₂ : sSup (f '' Icc a b) = f b
⊢ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b)) = Icc (f a) (f b)

Tactic:
congr!
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a

Tactic:
h'.sInf_image_Icc hab

Premises used: MonotoneOn.sInf_image_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a

Tactic:
exact h'.sInf_image_Icc hab

Premises used: MonotoneOn.sInf_image_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
⊢ sSup (f '' Icc a b) = f b

Tactic:
h'.sSup_image_Icc hab

Premises used: MonotoneOn.sSup_image_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
⊢ sSup (f '' Icc a b) = f b

Tactic:
exact h'.sSup_image_Icc hab

Premises used: MonotoneOn.sSup_image_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
rw : Icc (f b) (f a) = (⇑ofDual : (a : βᵒᵈ) → β) ⁻¹' Icc (f b) (f a)
⊢ Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))

Tactic:
rw [Icc_toDual]

Premises used: Set.Icc_toDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
⊢ Icc (f b) (f a) = (⇑ofDual : (a : βᵒᵈ) → β) ⁻¹' Icc (f b) (f a)

Tactic:
rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
⊢ Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))

Tactic:
have : Icc (f b) (f a) = Icc (toDual (f a)) (toDual (f b)) := by rw [Icc_toDual]; rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
this : Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
rw : f '' Icc a b = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
⊢ f '' Icc a b = Icc (f b) (f a)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
this : Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
⊢ f '' Icc a b = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))

Tactic:
image_Icc_of_monotoneOn (β := βᵒᵈ) hab h h'.dual_right

Premises used: AntitoneOn.dual_right, ContinuousOn.image_Icc_of_monotoneOn, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
this : Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
⊢ f '' Icc a b = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))

Tactic:
exact image_Icc_of_monotoneOn (β := βᵒᵈ) hab h h'.dual_right

Premises used: AntitoneOn.dual_right, ContinuousOn.image_Icc_of_monotoneOn
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s : Set X
exists_countable_separating :
  ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn X (fun (x : Set X) ↦ Membership.mem (γ := Set (Set X)) (range Iio) x) s

Tactic:
constructor
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s : Set X
exists_countable_separating :
  ∀ (s_1 : Set X) (hsc : s_1.Countable) (hsd : Dense s_1),
    ∃ (S : Set (Set X)),
      S.Countable ∧
        (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
rcases TopologicalSpace.exists_countable_dense X with ⟨s, hsc, hsd⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧
        ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
⟨Iio '' t, .image ?_ _, ?_, ?_⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.image, Set.Iio
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
exists_countable_separating : t.Countable
exists_countable_separating₁ : ∀ s ∈ Iio '' t, Membership.mem (γ := Set (Set X)) (range Iio) s
exists_countable_separating₂ : ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧
        ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
refine ⟨Iio '' t, .image ?_ _, ?_, ?_⟩
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
⊢ t.Countable

Tactic:
hsc.union countable_setOf_covBy_left

Premises used: countable_setOf_covBy_left, Set.Countable.union
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
⊢ t.Countable

Tactic:
exact hsc.union countable_setOf_covBy_left

Premises used: countable_setOf_covBy_left, Set.Countable.union
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
⊢ ∀ s ∈ Iio '' t, Membership.mem (γ := Set (Set X)) (range Iio) s

Tactic:
image_subset_range _ _

Premises used: Set.image_subset_range, Set.Subset
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
⊢ ∀ s ∈ Iio '' t, Membership.mem (γ := Set (Set X)) (range Iio) s

Tactic:
exact image_subset_range _ _

Premises used: Set.image_subset_range
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
exists_countable_separating : ∀ (hne : x ≠ y), False
⊢ x = y

Tactic:
by_contra! hne
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
exists_countable_separating :
  ∀ (this : ∀ (x y : X) (h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) (hne : x ≠ y) (hlt : x < y), False) (hlt : ¬x < y), False
wlog : ∀ (x y : X) (h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) (hne : x ≠ y) (hlt : x < y), False
⊢ False

Tactic:
wlog hlt : x < y generalizing x y