awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
rw : 𝓝[≥] a = 𝓝[<] a ⊔ 𝓝[≥] a
⊢ 𝓝[≥] a = 𝓝 a
have rw₁ : 𝓝[≥] a = ⊥ ⊔ 𝓝[≥] a
Tactic: rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
rw : 𝓝[≥] a = 𝓝[<] a ⊔ 𝓝[≥] a
rw₁ : 𝓝[≥] a = ⊥ ⊔ 𝓝[≥] a
⊢ 𝓝[≥] a = 𝓝 a
have rw₂ : 𝓝[≥] a = 𝓝[≥] a
Tactic: rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a ⋖ b
⊢ 𝓝[≤] b = pure b
have rw : 𝓝[insert b (Iio b)] b = pure b
Tactic: rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a ⋖ b
rw : 𝓝[insert b (Iio b)] b = pure b
⊢ 𝓝[≤] b = pure b
have rw₁ : pure b ⊔ 𝓝[<] b = pure b
Tactic: rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a ⋖ b
rw : 𝓝[insert b (Iio b)] b = pure b
rw₁ : pure b ⊔ 𝓝[<] b = pure b
⊢ 𝓝[≤] b = pure b
have rw₂ : Eq (α := Filter α) (pure b ⊔ ⊥) (pure b)
Tactic: rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a ⋖ b
rw : 𝓝[insert b (Iio b)] b = pure b
rw₁ : pure b ⊔ 𝓝[<] b = pure b
rw₂ : Eq (α := Filter α) (pure b ⊔ ⊥) (pure b)
⊢ 𝓝[≤] b = pure b
have rw₃ : Eq (α := Filter α) (pure b) (pure b)
Tactic: rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
b : α
inst_3 : PredOrder α
⊢ 𝓝[≤] b = pure b
have rw : 𝓝[insert b (Iio b)] b = pure b
Tactic: rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
b : α
inst_3 : PredOrder α
rw : 𝓝[insert b (Iio b)] b = pure b
⊢ 𝓝[≤] b = pure b
have rw₁ : pure b ⊔ 𝓝[<] b = pure b
Tactic: rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
b : α
inst_3 : PredOrder α
rw : 𝓝[insert b (Iio b)] b = pure b
rw₁ : pure b ⊔ 𝓝[<] b = pure b
⊢ 𝓝[≤] b = pure b
have rw₂ : Eq (α := Filter α) (pure b ⊔ ⊥) (pure b)
Tactic: rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
b : α
inst_3 : PredOrder α
rw : 𝓝[insert b (Iio b)] b = pure b
rw₁ : pure b ⊔ 𝓝[<] b = pure b
rw₂ : Eq (α := Filter α) (pure b ⊔ ⊥) (pure b)
⊢ 𝓝[≤] b = pure b
have rw₃ : Eq (α := Filter α) (pure b) (pure b)
Tactic: rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | MonotoneOn f s}
have simp : ∀ (a : β → α),
  (∃ᶠ (y : β → α) in 𝓝 a, Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} y) →
    Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} a
Tactic: simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
g : β → α
hg : ∃ᶠ (y : β → α) in 𝓝 g, Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} y
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ g a ≤ g b
have hmain : ∀ (x : β), Tendsto (fun (f' : β → α) ↦ f' x) (𝓝 g) (𝓝 (g x))
Tactic: have hmain (x) : Tendsto (fun f' ↦ f' x) (𝓝 g) (𝓝 (g x)) := continuousAt_apply x _
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | Monotone f}
have simp_rw : IsClosed[Pi.topologicalSpace] {f : β → α | MonotoneOn f univ}
Tactic: simp_rw [← monotoneOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
⊢ DiscreteTopology α
have refine : ∀ (a : α), 𝓝 a = pure a
Tactic: refine discreteTopology_iff_nhds.mpr fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
⊢ 𝓝 a = pure a
have rw : 𝓝[univ] a = pure a
Tactic: rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
rw : 𝓝[univ] a = pure a
⊢ 𝓝 a = pure a
have rw₁ : 𝓝[Iic a ∪ Ioi a] a = pure a
Tactic: rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
rw : 𝓝[univ] a = pure a
rw₁ : 𝓝[Iic a ∪ Ioi a] a = pure a
rw₂ : α
⊢ 𝓝 a = pure a
have rw₃ : 𝓝[≤] a ⊔ 𝓝[>] a = pure a
Tactic: rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
rw : 𝓝[univ] a = pure a
rw₁ : 𝓝[Iic a ∪ Ioi a] a = pure a
rw₂ : α
rw₃ : 𝓝[≤] a ⊔ 𝓝[>] a = pure a
rw₄ : α
⊢ 𝓝 a = pure a
have rw₅ : pure a ⊔ 𝓝[>] a = pure a
Tactic: rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
rw : 𝓝[univ] a = pure a
rw₁ : 𝓝[Iic a ∪ Ioi a] a = pure a
rw₂ : α
rw₃ : 𝓝[≤] a ⊔ 𝓝[>] a = pure a
rw₄ : α
rw₅ : pure a ⊔ 𝓝[>] a = pure a
⊢ 𝓝 a = pure a
have rw₆ : Eq (α := Filter α) (pure a ⊔ ⊥) (pure a)
Tactic: rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
rw : 𝓝[univ] a = pure a
rw₁ : 𝓝[Iic a ∪ Ioi a] a = pure a
rw₂ : α
rw₃ : 𝓝[≤] a ⊔ 𝓝[>] a = pure a
rw₄ : α
rw₅ : pure a ⊔ 𝓝[>] a = pure a
rw₆ : Eq (α := Filter α) (pure a ⊔ ⊥) (pure a)
⊢ 𝓝 a = pure a
have rw₇ : Eq (α := Filter α) (pure a) (pure a)
Tactic: rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
⊢ Subset.{v} (α := Set β) (frontier {b : β | f b ≤ g b}) {b : β | f b = g b}
have rw : Subset.{v} (α := Set β) ({b : β | f b ≤ g b} ∩ closure[inst_3] {b : β | f b ≤ g b}ᶜ) {b : β | f b = g b}
Tactic: rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
⊢ Membership.mem (γ := Set β) {b : β | f b = g b} b
have refine : Membership.mem (γ := Set β) (closure[inst_3] {b : β | g b < f b}) b
Tactic: refine le_antisymm hb₁ (closure_lt_subset_le hg hf ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
⊢ Membership.mem (γ := Set β) (closure[inst_3] {b : β | g b < f b}) b
have h : Eq.{v + 1} (α := Set β) {b : β | g b < f b} {b : β | f b ≤ g b}ᶜ
Tactic: convert! hb₂ using 2
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
⊢ Eq.{v + 1} (α := Set β) {b : β | g b < f b} {b : β | f b ≤ g b}ᶜ
have h : Eq.{v + 1} (α := Set β) {b : β | ¬f b ≤ g b} {b : β | f b ≤ g b}ᶜ
Tactic: simp only [not_le.symm]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
⊢ Continuous[inst_3, inst_4] fun (x : β) ↦ if f x ≤ g x then f' x else g' x
have refine_1 : ContinuousOn f' (closure[inst_3] {x : β | f x ≤ g x})
Tactic: refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
refine_1 : ContinuousOn f' (closure[inst_3] {x : β | f x ≤ g x})
⊢ Continuous[inst_3, inst_4] fun (x : β) ↦ if f x ≤ g x then f' x else g' x
have refine_2 : Subset.{v} (α := Set β) (closure[inst_3] {x : β | ¬f x ≤ g x}) {x : β | g x ≤ f x}
Tactic: refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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 : β | ¬f x ≤ g x}) {x : β | g x ≤ f x}
have refine_2 : Subset.{v} (α := Set β) (closure[inst_3] {x : β | g x < f x}) {x : β | g x ≤ f x}
Tactic: simp only [not_le]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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 : β) ↦ max (f b) (g b)
have simp : Continuous[inst_3, inst] fun (b : β) ↦ if f b ≤ g b then g b else f b
Tactic: simp only [max_def]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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 (f i) a) l (𝓝 a)
have simp_rw : Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝 a)
Tactic: simp_rw [max_comm _ a]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (hypothesis)
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)
have h₁ : Tendsto f l (𝓝 a)
Tactic: obtain ⟨h₁, h₂⟩ := tendsto_nhdsWithin_iff.mp h
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (hypothesis)
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)
⊢ Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)
have h₂ : ∀ᶠ (n : β) in l, f n ∈ Ioi a
Tactic: obtain ⟨h₁, h₂⟩ := tendsto_nhdsWithin_iff.mp h
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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 (f i) a) l (𝓝[>] a)
have simp_rw : Tendsto (fun (i : β) ↦ max a (f i)) l (𝓝[>] a)
Tactic: simp_rw [max_comm _ a]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
have refine : ∀ (z : α) (hz : z ∈ Ioi x), Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z
Tactic: refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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
⊢ Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z
have rcases : ∀ (y : α) (hys : y ∈ s) (hy : y ∈ Ioo x z), Membership.mem (γ := Set α) (⋃ y ∈ s ∩ Ioi x, Ioi y) z
Tactic: rcases hs.exists_between hz with ⟨y, hys, hy⟩
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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)
⊢ OrderClosedTopology ((i : ι) → α i)
have isClosed_le' : IsClosed[instTopologicalSpaceProd] {p : ((i : ι) → α i) × ((i : ι) → α i) | p.1 ≤ p.2}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
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] {p : ((i : ι) → α i) × ((i : ι) → α i) | p.1 ≤ p.2}
have isClosed_le' : IsClosed[instTopologicalSpaceProd] (⋂ (i : ι), {x : ((i : ι) → α i) × ((i : ι) → α i) | x.1 i ≤ x.2 i})
Tactic: simp only [Pi.le_def, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Order.PartialSups (goal)
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) ((partialSups f : (a : ℕ) → α → L) n : α → L) l (𝓝 ((partialSups g : (a : ℕ) → L) n) : Filter L)
have simp : Tendsto ((Finset.range (n + 1)).sup' sorry f) l (𝓝 ((Finset.range (n + 1)).sup' sorry g))
Tactic: simp only [partialSups_eq_sup'_range]
-- Lean 4 proof step from Mathlib.Topology.Order.PartialSups (goal)
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))
have refine : ∀ i ∈ Finset.range (n + 1), Tendsto (f i) l (𝓝 (g i))
Tactic: refine finset_sup'_nhds _ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Priestley (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h : x ≠ y
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
have inl : ∀ (h : ¬x ≤ y), ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
Tactic: obtain h | h := h.not_le_or_not_ge
-- Lean 4 proof step from Mathlib.Topology.Order.Priestley (goal)
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
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
have inr : ∀ (h : ¬y ≤ x), ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
Tactic: obtain h | h := h.not_le_or_not_ge
-- Lean 4 proof step from Mathlib.Topology.Order.Priestley (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h_1 : x ≠ y
h : ¬y ≤ x
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
have inr : ∀ (U : Set α) (hU : IsClopen U) (hU' : IsLowerSet U) (hy : y ∉ U) (hx : x ∈ U),
  ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
Tactic: obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h
-- Lean 4 proof step from Mathlib.Topology.Order.ProjIcc (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set (↑(Icc a b) : Type u_1)
hs : IsOpen[inst_1] (projIcc a b h ⁻¹' s)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) ⁻¹' projIcc a b h ⁻¹' s = s
have h₁ : ∀ (x : { x : α // x ∈ Icc a b }),
  Membership.mem (γ := Set { x : α // x ∈ Icc a b })
      (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) ⁻¹' projIcc a b h ⁻¹' s) x ↔
    x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have ne : (Icc a b).Nonempty
Tactic: have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have obtain : ∀ (c : X) (cmem : c ∈ Icc a b) (cle : ∀ x ∈ Icc a b, f c ≤ f x), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
    isCompact_Icc.exists_isMinOn ne hfc
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have obtain : ∀ (C : X) (Cmem : C ∈ Icc a b) (Cge : ∀ x ∈ Icc a b, f x ≤ f C), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
    isCompact_Icc.exists_isMaxOn ne hfc
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have pos : ∀ (hc : f c = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: by_cases hc : f c = f a
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
pos : ∀ (hc : f c = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have neg : ∀ (hc : ¬f c = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: by_cases hc : f c = f a
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have pos : ∀ (hC : f C = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: by_cases hC : f C = f a
-- Lean 4 proof step from Mathlib.Topology.Order.Rolle (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
pos : ∀ (hC : f C = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have neg : ∀ (hC : ¬f C = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: by_cases hC : f C = f a