awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
m : β
hm : m < f x
h : ∀ (y : α) (hy : y ∈ s ∩ Ioi x), m < f y
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, m < f b

Tactic:
filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
m : β
hm : m < f x
y : α
hy : y ∈ s ∩ Ioi x
⊢ m < f y

Tactic:
hm.trans_le (hf xs hy.1 (le_of_lt hy.2))

Premises used: le_of_lt, And.right, And.left, LT.lt.trans_le
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
m : β
hm : m < f x
y : α
hy : y ∈ s ∩ Ioi x
⊢ m < f y

Tactic:
exact hm.trans_le (hf xs hy.1 (le_of_lt hy.2))

Premises used: le_of_lt, And.right, And.left, LT.lt.trans_le
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
refine_2 : ∀ (v : α) (vs : v ∈ s) (xv : x < v) (fvu : f v < u), ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u

Tactic:
rcases hx xs u hu with ⟨v, vs, xv, fvu⟩
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
⊢ s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x

Tactic:
simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]

Premises used: Filter.mem_inf_of_left, Filter.mem_inf_of_right, self_mem_nhdsWithin, nhdsWithin_inter, Ioo_mem_nhdsGT
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
⊢ s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x

Tactic:
have : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x := by simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
h : ∀ (y : α) (hy : y ∈ s ∩ Ioo x v), f y < u
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
y : α
hy : y ∈ s ∩ Ioo x v
⊢ f y < u

Tactic:
(hf hy.1 vs hy.2.2.le).trans_lt fvu

Premises used: LT.lt.le, And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
y : α
hy : y ∈ s ∩ Ioo x v
⊢ f y < u

Tactic:
exact (hf hy.1 vs hy.2.2.le).trans_lt fvu

Premises used: LT.lt.le, And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}

Tactic:
hf.dual.countable_not_continuousWithinAt_Ioi

Premises used: MonotoneOn.countable_not_continuousWithinAt_Ioi, Set.Mem, setOf, MonotoneOn.dual, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
apply :
  Subset.{u_1} (α := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}

Tactic:
apply (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono

Premises used: MonotoneOn.countable_not_continuousWithinAt_Ioi, Set.Countable.union, Set.Countable.mono, MonotoneOn.countable_not_continuousWithinAt_Iio
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
⊢ Subset.{u_1} (α := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})

Tactic:
compl_subset_compl.1 ?_

Premises used: Set.compl_subset_compl, Iff.mp
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
refine :
  Subset.{u_1} (α := Set α)
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})ᶜ
    {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ
⊢ Subset.{u_1} (α := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})

Tactic:
refine compl_subset_compl.1 ?_

Premises used: Set.compl_subset_compl, Iff.mp
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
simp :
  Subset.{u_1} (α := Set α)
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}ᶜ ∩ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}ᶜ)
    {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ
⊢ Subset.{u_1} (α := Set α)
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})ᶜ
    {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ

Tactic:
simp only [compl_union]

Premises used: Set.compl_union
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}ᶜ x
h'x : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}ᶜ x
simp :
  ∀ (hx : x ∈ s → ContinuousWithinAt f (s ∩ Ioi x) x) (h'x : x ∈ s → ContinuousWithinAt f (s ∩ Iio x) x),
    x ∈ s → ContinuousWithinAt f s x
⊢ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ x

Tactic:
simp only [mem_compl_iff, mem_setOf_eq, not_and, not_not] at hx h'x ⊢

Premises used: Classical.not_not, Set.mem_setOf_eq, not_and, Set.mem_compl_iff
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
hx : x ∈ s → ContinuousWithinAt f (s ∩ Ioi x) x
h'x : x ∈ s → ContinuousWithinAt f (s ∩ Iio x) x
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
continuousWithinAt_iff_continuous_left'_right'.2 ⟨h'x xs, hx xs⟩

Premises used: Iff.mpr, continuousWithinAt_iff_continuous_left'_right', And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
hx : x ∈ s → ContinuousWithinAt f (s ∩ Ioi x) x
h'x : x ∈ s → ContinuousWithinAt f (s ∩ Iio x) x
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
exact continuousWithinAt_iff_continuous_left'_right'.2 ⟨h'x xs, hx xs⟩

Premises used: Iff.mpr, continuousWithinAt_iff_continuous_left'_right', And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : Monotone f
⊢ Set.Countable.{u_1} (α := α) {x : α | ¬ContinuousAt f x}

Tactic:
simpa [continuousWithinAt_univ] using (hf.monotoneOn univ).countable_not_continuousWithinAt

Premises used: continuousWithinAt_univ, Set.univ, MonotoneOn.countable_not_continuousWithinAt, Monotone.monotoneOn
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
s : Set α
hf : AntitoneOn f s
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}

Tactic:
hf.dual_right.countable_not_continuousWithinAt

Premises used: setOf, AntitoneOn.dual_right, MonotoneOn.countable_not_continuousWithinAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : Antitone f
⊢ Set.Countable.{u_1} (α := α) {x : α | ¬ContinuousAt f x}

Tactic:
hf.dual_right.countable_not_continuousAt

Premises used: Antitone.dual_right, setOf, Monotone.countable_not_continuousAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousWithinAt f A (sSup A)
Mf : MonotoneOn f A
A_nonemp : A.Nonempty
A_bdd : BddAbove A
⊢ f (sSup A) = sSup (f '' A)

Tactic:
.symm <| ((isLUB_csSup A_nonemp A_bdd).isLUB_of_tendsto Mf A_nonemp <|
    Cf.mono_left fun ⦃_⦄ a ↦ a).csSup_eq (A_nonemp.image f)

Premises used: Set.Nonempty.image, IsLUB.csSup_eq, Filter.Tendsto.mono_left, IsLUB.isLUB_of_tendsto, isLUB_csSup, Eq.symm
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousAt f (sSup A)
Mf : Monotone f
A_nonemp : A.Nonempty
A_bdd : BddAbove A
⊢ f (sSup A) = sSup (f '' A)

Tactic:
MonotoneOn.map_csSup_of_continuousWithinAt Cf.continuousWithinAt
    (Mf.monotoneOn _) A_nonemp A_bdd

Premises used: ContinuousAt.continuousWithinAt, MonotoneOn.map_csSup_of_continuousWithinAt, Monotone.monotoneOn
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
rw₄ rw₅ : Eq.{u_2 + 1} (α := β) (sSup (range fun (x : ι) ↦ f (g x))) (sSup (range fun (i : ι) ↦ f (g i)))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]

Premises used: Set.range_comp, iSup, Monotone.map_csSup_of_continuousAt, Function.comp_def, Set.range_nonempty
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousWithinAt f A (sInf A)
Mf : MonotoneOn f A
A_nonemp : A.Nonempty
A_bdd : BddBelow A
⊢ f (sInf A) = sInf (f '' A)

Tactic:
MonotoneOn.map_csSup_of_continuousWithinAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual A_nonemp A_bdd

Premises used: MonotoneOn.map_csSup_of_continuousWithinAt, MonotoneOn.dual, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousAt f (sInf A)
Mf : Monotone f
A_nonemp : A.Nonempty
A_bdd : BddBelow A
⊢ f (sInf A) = sInf (f '' A)

Tactic:
Monotone.map_csSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual A_nonemp A_bdd

Premises used: Monotone.map_csSup_of_continuousAt, Monotone.dual, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
rw₃ : sInf (range (f ∘ g)) = sInf (range fun (i : ι) ↦ f (g i))
rw₄ rw₅ : Eq.{u_2 + 1} (α := β) (sInf (range fun (x : ι) ↦ f (g x))) (sInf (range fun (i : ι) ↦ f (g i)))
⊢ f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)

Tactic:
rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]

Premises used: Set.range_comp, iInf, Function.comp_def, Monotone.map_csInf_of_continuousAt, Set.range_nonempty
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousWithinAt f A (sInf A)
Af : AntitoneOn f A
A_nonemp : A.Nonempty
A_bdd : BddBelow A
⊢ f (sInf A) = sSup (f '' A)

Tactic:
MonotoneOn.map_csInf_of_continuousWithinAt (β := βᵒᵈ) Cf Af.dual_right A_nonemp A_bdd

Premises used: MonotoneOn.map_csInf_of_continuousWithinAt, AntitoneOn.dual_right, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousAt f (sInf A)
Af : Antitone f
A_nonemp : A.Nonempty
A_bdd : BddBelow A
⊢ f (sInf A) = sSup (f '' A)

Tactic:
Monotone.map_csInf_of_continuousAt (β := βᵒᵈ) Cf Af.dual_right A_nonemp A_bdd

Premises used: Antitone.dual_right, Monotone.map_csInf_of_continuousAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
rw₄ rw₅ : Eq.{u_2 + 1} (α := β) (sSup (range fun (x : ι) ↦ f (g x))) (sSup (range fun (i : ι) ↦ f (g i)))
⊢ f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]

Premises used: Set.range_comp, iInf, iSup, Antitone.map_csInf_of_continuousAt, Function.comp_def, Set.range_nonempty
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousWithinAt f A (sSup A)
Af : AntitoneOn f A
A_nonemp : A.Nonempty
A_bdd : BddAbove A
⊢ f (sSup A) = sInf (f '' A)

Tactic:
MonotoneOn.map_csSup_of_continuousWithinAt (β := βᵒᵈ) Cf Af.dual_right A_nonemp A_bdd

Premises used: AntitoneOn.dual_right, MonotoneOn.map_csSup_of_continuousWithinAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
A : Set α
Cf : ContinuousAt f (sSup A)
Af : Antitone f
A_nonemp : A.Nonempty
A_bdd : BddAbove A
⊢ f (sSup A) = sInf (f '' A)

Tactic:
Monotone.map_csSup_of_continuousAt (β := βᵒᵈ) Cf Af.dual_right A_nonemp A_bdd

Premises used: Antitone.dual_right, Monotone.map_csSup_of_continuousAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
rw₃ : sInf (range (f ∘ g)) = sInf (range fun (i : ι) ↦ f (g i))
rw₄ rw₅ : Eq.{u_2 + 1} (α := β) (sInf (range fun (x : ι) ↦ f (g x))) (sInf (range fun (i : ι) ↦ f (g i)))
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)

Tactic:
rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]

Premises used: Set.range_comp, iInf, iSup, Antitone.map_csSup_of_continuousAt, Function.comp_def, Set.range_nonempty
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : s.Nonempty
⊢ sSup s ∈ closure[inst_1] s

Tactic:
(isLUB_sSup s).mem_closure hs

Premises used: Set.Mem, IsLUB.mem_closure, isLUB_sSup
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : s.Nonempty
⊢ sInf s ∈ closure[inst_1] s

Tactic:
(isGLB_sInf s).mem_closure hs

Premises used: Set.Mem, IsGLB.mem_closure, isGLB_sInf
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : s.Nonempty
hc : IsClosed[inst_1] s
⊢ sSup s ∈ s

Tactic:
(isLUB_sSup s).mem_of_isClosed hs hc

Premises used: Set.Mem, isLUB_sSup, IsLUB.mem_of_isClosed
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : s.Nonempty
hc : IsClosed[inst_1] s
⊢ sInf s ∈ s

Tactic:
(isGLB_sInf s).mem_of_isClosed hs hc

Premises used: IsGLB.mem_of_isClosed, Set.Mem, isGLB_sInf
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
inl : ∀ (h : s = ∅), f (sSup s) = sSup (f '' s)
inr : ∀ (h : s.Nonempty), f (sSup s) = sSup (f '' s)
⊢ f (sSup s) = sSup (f '' s)

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)

Tactic:
simp [h, fbot]
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
Mf.map_csSup_of_continuousWithinAt Cf h

Premises used: MonotoneOn.map_csSup_of_continuousWithinAt