awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hf' : ContinuousOn f' {x : β | f x ≤ g x}
hg' : ContinuousOn g' {x : β | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Subset.{v} (α := Set β) (closure[inst_3] {x : β | g x < f x}) {x : β | g x ≤ f x}

Tactic:
closure_lt_subset_le hg hf

Premises used: closure_lt_subset_le, setOf
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hf' : ContinuousOn f' {x : β | f x ≤ g x}
hg' : ContinuousOn g' {x : β | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Subset.{v} (α := Set β) (closure[inst_3] {x : β | g x < f x}) {x : β | g x ≤ f x}

Tactic:
exact closure_lt_subset_le hg hf

Premises used: closure_lt_subset_le
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf' : Continuous[inst_3, inst_4] f'
hg' : Continuous[inst_3, inst_4] g'
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Continuous[inst_3, inst_4] fun (x : β) ↦ if f x ≤ g x then f' x else g' x

Tactic:
continuous_if_le hf hg hf'.continuousOn hg'.continuousOn hfg

Premises used: Continuous.continuousOn, continuous_if_le
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
l : Filter γ
f g : γ → α
y z : α
hf : Tendsto f l (𝓝 y)
hg : Tendsto g l (𝓝 z)
hyz : y < z
⊢ ∀ᶠ (x : γ) in l, f x < g x

Tactic:
let ⟨_a, ha, _b, hb, h⟩ := hyz.exists_disjoint_Iio_Ioi
  (hg.eventually (Ioi_mem_nhds hb)).mp <| (hf.eventually (Iio_mem_nhds ha)).mono fun _ h₁ h₂ =>
    h _ h₁ _ h₂

Premises used: Ioi_mem_nhds, Iio_mem_nhds, Filter.Eventually, LT.lt.exists_disjoint_Iio_Ioi, Filter.Eventually.mono, _private.0.Filter.Tendsto.eventually_lt.match_1, Filter.Eventually.mp, LT.lt, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
x₀ : β
hf : ContinuousAt f x₀
hg : ContinuousAt g x₀
hfg : f x₀ < g x₀
⊢ ∀ᶠ (x : β) in 𝓝 x₀, f x < g x

Tactic:
hf.eventually_lt hg hfg

Premises used: Filter.Tendsto.eventually_lt
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
simp : Continuous[inst_3, inst] fun (b : β) ↦ if f b ≤ g b then g b else f b
⊢ Continuous[inst_3, inst] fun (b : β) ↦ max (f b) (g b)

Tactic:
simp only [max_def]

Premises used: max_def
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
⊢ Continuous[inst_3, inst] fun (b : β) ↦ if f b ≤ g b then g b else f b

Tactic:
hg.if_ge hf hg hf fun x => id

Premises used: id, Continuous.if_ge
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
⊢ Continuous[inst_3, inst] fun (b : β) ↦ if f b ≤ g b then g b else f b

Tactic:
exact hg.if_ge hf hg hf fun x => id

Premises used: id, Continuous.if_ge
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : α × α) ↦ max p.1 p.2

Tactic:
continuous_fst.max continuous_snd

Premises used: continuous_snd, continuous_fst, Continuous.max
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
b : Filter β
a₁ a₂ : α
hf : Tendsto f b (𝓝 a₁)
hg : Tendsto g b (𝓝 a₂)
⊢ Tendsto (fun (b : β) ↦ max (f b) (g b)) b (𝓝 (max a₁ a₂))

Tactic:
(continuous_max.tendsto (a₁, a₂)).comp (hf.prodMk_nhds hg)

Premises used: Prod.mk, Continuous.tendsto, Filter.Tendsto.comp, continuous_max, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝 a)

Tactic:
simpa only [sup_idem] using (tendsto_const_nhds (x := a)).max h

Premises used: tendsto_const_nhds, Filter.Tendsto.max, sup_idem
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
simp_rw : Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝 a)
⊢ Tendsto (fun (i : β) ↦ max (f i) a) l (𝓝 a)

Tactic:
simp_rw [max_comm _ a]

Premises used: max_comm
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝 a)

Tactic:
h.max_right

Premises used: Filter.Tendsto.max_right
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝 a)

Tactic:
exact h.max_right

Premises used: Filter.Tendsto.max_right
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto f l (𝓝 a)

Tactic:
obtain ⟨h₁, h₂⟩ := tendsto_nhdsWithin_iff.mp h

Premises used: tendsto_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
h₁ : Tendsto f l (𝓝 a)
⊢ ∀ᶠ (n : β) in l, f n ∈ Ioi a

Tactic:
obtain ⟨h₁, h₂⟩ := tendsto_nhdsWithin_iff.mp h

Premises used: tendsto_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
h₁ : Tendsto f l (𝓝 a)
h₂ : ∀ᶠ (n : β) in l, f n ∈ Ioi a
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)

Tactic:
tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, Filter.Tendsto.max_right, lt_max_of_lt_right, Filter.Eventually.mono, And.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
h₁ : Tendsto f l (𝓝 a)
h₂ : ∀ᶠ (n : β) in l, f n ∈ Ioi a
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)

Tactic:
exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, Filter.Tendsto.max_right, lt_max_of_lt_right, Filter.Eventually.mono, And.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
simp_rw : Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)
⊢ Tendsto (fun (i : β) ↦ max (f i) a) l (𝓝[>] a)

Tactic:
simp_rw [max_comm _ a]

Premises used: max_comm
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)

Tactic:
Filter.tendsto_nhds_max_right h

Premises used: Filter.tendsto_nhds_max_right
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)

Tactic:
exact Filter.tendsto_nhds_max_right h

Premises used: Filter.tendsto_nhds_max_right
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
x y : α
h : x < y
⊢ ∃ z ∈ s, z ∈ Ioo x y

Tactic:
hs.exists_mem_open isOpen_Ioo (nonempty_Ioo.2 h)

Premises used: Iff.mpr, isOpen_Ioo, Set.nonempty_Ioo, Dense.exists_mem_open
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
x : α
⊢ Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset, le_of_lt, And.right, Set.Ioi_subset_Ioi
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
x : α
refine : ∀ (z : α) (hz : z ∈ Ioi x), Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z
⊢ Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset, le_of_lt, Set.Ioi_subset_Ioi
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
rcases : ∀ (y : α) (hys : y ∈ s) (hy : y ∈ Ioo x z), Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z
⊢ Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z

Tactic:
rcases hs.exists_between hz with ⟨y, hys, hy⟩

Premises used: Dense.exists_between
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
y : α
hys : y ∈ s
hy : y ∈ Ioo x z
⊢ Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z

Tactic:
mem_iUnion₂.2 ⟨y, ⟨hys, hy.1⟩, hy.2⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
y : α
hys : y ∈ s
hy : y ∈ Ioo x z
⊢ Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z

Tactic:
exact mem_iUnion₂.2 ⟨y, ⟨hys, hy.1⟩, hy.2⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
⊢ OrderClosedTopology (α × β)

Tactic:
⟨(isClosed_le continuous_fst.fst continuous_snd.fst).inter
    (isClosed_le continuous_fst.snd continuous_snd.snd)⟩

Premises used: Continuous.snd, isClosed_le, continuous_snd, continuous_fst, OrderClosedTopology.mk, Continuous.fst, IsClosed.inter
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderClosedTopology.{u_2} (α i)
isClosed_le' : IsClosed[instTopologicalSpaceProd] {p : ((i : ι) → α i) × ((i : ι) → α i) | p.1 ≤ p.2}
⊢ OrderClosedTopology ((i : ι) → α i)

Tactic:
constructor
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderClosedTopology.{u_2} (α i)
isClosed_le' : IsClosed[instTopologicalSpaceProd] (⋂ (i : ι), {x : ((i : ι) → α i) × ((i : ι) → α i) | x.1 i ≤ x.2 i})
⊢ IsClosed[instTopologicalSpaceProd] {p : ((i : ι) → α i) × ((i : ι) → α i) | p.1 ≤ p.2}

Tactic:
simp only [Pi.le_def, setOf_forall]

Premises used: Pi.le_def, Set.setOf_forall
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderClosedTopology.{u_2} (α i)
⊢ IsClosed[instTopologicalSpaceProd] (⋂ (i : ι), {x : ((i : ι) → α i) × ((i : ι) → α i) | x.1 i ≤ x.2 i})

Tactic:
isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

Premises used: Continuous.fst', Continuous.snd', isClosed_le, continuous_apply, isClosed_iInter
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderClosedTopology.{u_2} (α i)
⊢ IsClosed[instTopologicalSpaceProd] (⋂ (i : ι), {x : ((i : ι) → α i) × ((i : ι) → α i) | x.1 i ≤ x.2 i})

Tactic:
exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

Premises used: Continuous.fst', isClosed_le, continuous_apply, isClosed_iInter
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : TopologicalSpace β
inst_2 : OrderClosedTopology β
⊢ OrderClosedTopology (α → β)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.OrderClosedExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
β : Type u_2
inst_3 : Preorder β
a b c : α
g₀ : a < b
g₁ : b < c
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
⊢ IsLocalMax f b

Tactic:
(isMaxOn_Ioo_of_mono_anti h₀ h₁).isLocalMax (Ioo_mem_nhds g₀ g₁)

Premises used: IsMaxOn.isLocalMax, Ioo_mem_nhds, isMaxOn_Ioo_of_mono_anti
-- Module: Mathlib.Topology.Order.OrderClosedExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
β : Type u_2
inst_3 : Preorder β
a b c : α
g₀ : a < b
g₁ : b < c
f : α → β
h₀ : AntitoneOn f (Ioc a b)
h₁ : MonotoneOn f (Ico b c)
⊢ IsLocalMin f b

Tactic:
isLocalMax_of_mono_anti (β := βᵒᵈ) g₀ g₁ h₀ h₁

Premises used: IsMinFilter, IsLocalMin, isLocalMax_of_mono_anti
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
simp : Tendsto ((Finset.range (n + 1)).sup' ⋯ f) l (𝓝 ((Finset.range (n + 1)).sup' ⋯ g))
⊢ Tendsto (β := L) ((partialSups f : (a : ℕ) → α → L) n : α → L) l (𝓝 ((partialSups g : (a : ℕ) → L) n) : Filter L)

Tactic:
simp only [partialSups_eq_sup'_range]

Premises used: partialSups_eq_sup'_range
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto ((Finset.range (n + 1)).sup' ⋯ f) l (𝓝 ((Finset.range (n + 1)).sup' ⋯ g))

Tactic:
finset_sup'_nhds _ ?_

Premises used: Filter.Tendsto.finset_sup'_nhds
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
refine : ∀ i ∈ Finset.range (n + 1), Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((Finset.range (n + 1)).sup' ⋯ f) l (𝓝 ((Finset.range (n + 1)).sup' ⋯ g))

Tactic:
refine finset_sup'_nhds _ ?_

Premises used: Filter.Tendsto.finset_sup'_nhds
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ ∀ i ∈ Finset.range (n + 1), Tendsto (f i) l (𝓝 (g i))

Tactic:
simpa [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto (β := L) (fun (a : α) ↦ ((partialSups fun (x : ℕ) ↦ f x a : (a : ℕ) → L) n : L)) l
    (𝓝 ((partialSups g : (a : ℕ) → L) n) : Filter L)

Tactic:
simpa only [← Pi.partialSups_apply] using Tendsto.partialSups hf

Premises used: Filter.Tendsto.partialSups, Pi.partialSups_apply
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
x : X
hf : ∀ k ≤ n, ContinuousAt (f k) x
⊢ ContinuousAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ (partialSups fun (x : ℕ) ↦ f x a : (a : ℕ) → L) n) x

Tactic:
Tendsto.partialSups_apply hf

Premises used: Filter.Tendsto.partialSups_apply, ContinuousAt
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
x : X
hf : ∀ k ≤ n, ContinuousAt (f k) x
⊢ ContinuousAt.{u_2, u_1} (Y := L) ((partialSups f : (a : ℕ) → X → L) n) x

Tactic:
simpa only [← Pi.partialSups_apply] using ContinuousAt.partialSups_apply hf

Premises used: ContinuousAt.partialSups_apply, Pi.partialSups_apply
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
s : Set X
x : X
hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ (partialSups fun (x : ℕ) ↦ f x a : (a : ℕ) → L) n) s x

Tactic:
Tendsto.partialSups_apply hf

Premises used: Filter.Tendsto.partialSups_apply, ContinuousWithinAt
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
s : Set X
x : X
hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) ((partialSups f : (a : ℕ) → X → L) n) s x

Tactic:
simpa only [← Pi.partialSups_apply] using ContinuousWithinAt.partialSups_apply hf

Premises used: ContinuousWithinAt.partialSups_apply, Pi.partialSups_apply
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
s : Set X
hf : ∀ k ≤ n, ContinuousOn (f k) s
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ (partialSups fun (x : ℕ) ↦ f x a : (a : ℕ) → L) n) s

Tactic:
fun x hx ↦
  ContinuousWithinAt.partialSups_apply fun k hk ↦ hf k hk x hx

Premises used: ContinuousWithinAt.partialSups_apply, ContinuousOn
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
s : Set X
hf : ∀ k ≤ n, ContinuousOn (f k) s
⊢ ContinuousOn.{u_2, u_1} (Y := L) ((partialSups f : (a : ℕ) → X → L) n) s

Tactic:
fun x hx ↦
  ContinuousWithinAt.partialSups fun k hk ↦ hf k hk x hx

Premises used: ContinuousWithinAt.partialSups, ContinuousOn
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
hf : ∀ k ≤ n, Continuous[inst_3, inst_1] (f k)
⊢ Continuous[inst_3, inst_1] fun (a : X) ↦ (partialSups fun (x : ℕ) ↦ f x a : (a : ℕ) → L) n

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.partialSups_apply fun k hk ↦
    (hf k hk).continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.partialSups_apply, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.PartialSups
Goal:
L : Type u_1
inst : SemilatticeSup L
inst_1 : TopologicalSpace L
inst_2 : ContinuousSup L
X : Type u_2
inst_3 : TopologicalSpace X
f : ℕ → X → L
n : ℕ
hf : ∀ k ≤ n, Continuous[inst_3, inst_1] (f k)
⊢ Continuous[inst_3, inst_1] ((partialSups f : (a : ℕ) → X → L) n)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.partialSups fun k hk ↦ (hf k hk).continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.partialSups, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : PriestleySpace α
x y : α
⊢ ¬x ≤ y → ∃ (U : Set α), IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U

Tactic:
PriestleySpace.priestley

Premises used: PriestleySpace.priestley
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : PriestleySpace α
x y : α
h : ¬x ≤ y
⊢ ∃ (U : Set α), IsClopen U ∧ IsLowerSet U ∧ x ∉ U ∧ y ∈ U

Tactic:
let ⟨U, hU, hU', hx, hy⟩ := exists_isClopen_upper_of_not_le h
  ⟨Uᶜ, hU.compl, hU'.compl, Classical.not_not.2 hx, hy⟩

Premises used: Iff.mpr, IsUpperSet.compl, Classical.not_not, Compl.compl, exists_isClopen_upper_of_not_le, Membership.mem, Exists, IsClopen.compl, And, IsLowerSet, And.intro, Exists.intro, IsClopen, Not, _private.0.exists_isClopen_lower_of_not_le.match_1
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h : x ≠ y
inl : ∀ (h : ¬x ≤ y), ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
inr : ∀ (h : ¬y ≤ x), ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
obtain h | h := h.not_le_or_not_ge

Premises used: Ne.not_le_or_not_ge
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h_1 : x ≠ y
h : ¬x ≤ y
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
(exists_isClopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl

Premises used: exists_isClopen_upper_of_not_le, And.imp_left, Exists.imp, Or.inl, And.imp_right
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h_1 : x ≠ y
h : ¬x ≤ y
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
exact (exists_isClopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl

Premises used: exists_isClopen_upper_of_not_le, And.imp_left, Exists.imp, Or.inl, And.imp_right