awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
hC : f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have this : ∀ x ∈ Icc a b, f x = f a
Tactic: have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
-- 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
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have pos : ∀ (c' : X) (hc' : c' ∈ Ioo a b), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic: rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
-- 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
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have pos : ∀ (x : X) (hx : x ∈ Icc a b), Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f c' ≤ f x) x} x
Tactic: refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
-- 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
hC : ¬f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have neg : a = C → f C = f a
Tactic: refine ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt ?_ hC, lt_of_le_of_ne Cmem.2 <| mt ?_ hC⟩, Or.inr Cge⟩
-- 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
hC : ¬f C = f a
neg : a = C → f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have neg₁ : C = b → f C = f a
Tactic: refine ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt ?_ hC, lt_of_le_of_ne Cmem.2 <| mt ?_ hC⟩, Or.inr Cge⟩
-- 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
hC : ¬f C = f a
h : a = C
⊢ f C = f a
have rw : f C = f C
Tactic: rw [h]
-- 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
hC : ¬f C = f a
h : C = b
⊢ f C = f a
have rw : f b = f a
Tactic: rw [h, hfI]
-- 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
hC : ¬f C = f a
h : C = b
rw : f b = f a
⊢ f C = f a
have rw₁ : f b = f b
Tactic: rw [h, hfI]
-- 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 neg : a = c → f c = f a
Tactic: refine ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩
-- 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
neg : a = c → f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
have neg₁ : c = b → f c = f a
Tactic: refine ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩
-- 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
h : a = c
⊢ f c = f a
have rw : f c = f c
Tactic: rw [h]
-- 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
h : c = b
⊢ f c = f a
have rw : f b = f a
Tactic: rw [h, hfI]
-- 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
h : c = b
rw : f b = f a
⊢ f c = f a
have rw₁ : f b = f b
Tactic: rw [h, hfI]
-- 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
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 l)
hb : Tendsto f (𝓝[<] b) (𝓝 l)
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
Tactic: have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends 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
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 l)
hb : Tendsto f (𝓝[<] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
have obtain : ∀ (c : X) (hc : c ∈ Ioo a b) (hfc : IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c),
  ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
Tactic: obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
    exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hfc ha hb)
      ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
-- 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
l : Y
hab : a ≠ b
hfc : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 l)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 l)
⊢ ∃ c ∈ uIoo a b, IsExtrOn f (uIoo a b) c
have h : EqOn (extendFrom (uIoo a b) f) f (uIoo a b)
Tactic: have h : EqOn (extendFrom (uIoo a b) f) f (uIoo a b) := extendFrom_extends 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
l : Y
hab : a ≠ b
hfc : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 l)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 l)
h : EqOn (extendFrom (uIoo a b) f) f (uIoo a b)
⊢ ∃ c ∈ uIoo a b, IsExtrOn f (uIoo a b) c
have obtain : ∀ (c : X) (hc : c ∈ uIoo a b) (hfc : IsExtrOn (extendFrom (uIoo a b) f) (uIcc a b) c),
  ∃ c ∈ uIoo a b, IsExtrOn f (uIoo a b) c
Tactic: obtain ⟨c, hc, hfc⟩ : ∃ c ∈ uIoo a b, IsExtrOn (extendFrom (uIoo a b) f) (uIcc a b) c :=
    exists_uIoo_isExtrOn_uIcc hab (continuousOn_uIcc_extendFrom_uIoo hfc ha hb)
      ((eq_lim_at_left_extendFrom_uIoo hab ha).trans (eq_lim_at_right_extendFrom_uIoo hab hb).symm)
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst : Preorder α
s t : Set α
hs :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
ht :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
ha : a ∈ s ∩ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
have obtain : ∀ (b₁ : α) (hb₁d : b₁ ∈ d) (hb₁ds : Ici b₁ ∩ d ⊆ s), ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
Tactic: obtain ⟨b₁, hb₁d, hb₁ds⟩ := hs hd₀ hd₁ hd₂ hd₃ ha.1
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst : Preorder α
s t : Set α
hs :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
ht :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
ha : a ∈ s ∩ t
b₁ : α
hb₁d : b₁ ∈ d
hb₁ds : Ici b₁ ∩ d ⊆ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
have obtain : ∀ (b₂ : α) (hb₂d : b₂ ∈ d) (hb₂dt : Ici b₂ ∩ d ⊆ t), ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
Tactic: obtain ⟨b₂, hb₂d, hb₂dt⟩ := ht hd₀ hd₁ hd₂ hd₃ ha.2
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst : Preorder α
s t : Set α
hs :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
ht :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
ha : a ∈ s ∩ t
b₁ : α
hb₁d : b₁ ∈ d
hb₁ds : Ici b₁ ∩ d ⊆ s
b₂ : α
hb₂d : b₂ ∈ d
hb₂dt : Ici b₂ ∩ d ⊆ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
have obtain : ∀ (c : α) (hcd : c ∈ d) (hc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b₁ c ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b₂ c),
  ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
Tactic: obtain ⟨c, hcd, hc⟩ := hd₂ b₁ hb₁d b₂ hb₂d
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
h :
  ∀ t ∈ s,
    ∀ ⦃d : Set α⦄,
      d ∈ D →
        d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
h_1 : a ∈ ⋃₀ s
s₀ : Set α
hs₀s : s₀ ∈ s
has₀ : a ∈ s₀
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s
have obtain : ∀ (b : α) (hbd : b ∈ d) (hbds₀ : Ici b ∩ d ⊆ s₀), ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s
Tactic: obtain ⟨b, hbd, hbds₀⟩ := h s₀ hs₀s hd₀ hd₁ hd₂ hd₃ has₀
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsOpen[t] s ↔ DirSupInaccOn D s
have rw : (∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) ↔
  DirSupInaccOn D s
Tactic: rw [isOpen_iff (D := D), dirSupInaccOn_iff_inter_subset hDL]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
rw :
  (∀ ⦃d : Set α⦄,
      d ∈ D →
        d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) ↔
    DirSupInaccOn D s
⊢ IsOpen[t] s ↔ DirSupInaccOn D s
have rw₁ : (∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) ↔
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
Tactic: rw [isOpen_iff (D := D), dirSupInaccOn_iff_inter_subset hDL]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsClosed[t] s ↔ DirSupClosedOn D s
have rw : IsOpen[t] sᶜ ↔ DirSupClosedOn D s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_dirSupInaccOn hDL, dirSupInaccOn_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
rw : IsOpen[t] sᶜ ↔ DirSupClosedOn D s
⊢ IsClosed[t] s ↔ DirSupClosedOn D s
have rw₁ : DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_dirSupInaccOn hDL, dirSupInaccOn_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
rw : IsOpen[t] sᶜ ↔ DirSupClosedOn D s
rw₁ : DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s
⊢ IsClosed[t] s ↔ DirSupClosedOn D s
have rw₂ : DirSupClosedOn D s ↔ DirSupClosedOn D s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_dirSupInaccOn hDL, dirSupInaccOn_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α univ
⊢ IsOpen[t] s ↔ DirSupInacc s
have rw : DirSupInaccOn univ s ↔ DirSupInacc s
Tactic: rw [isOpen_iff_dirSupInaccOn isLowerSet_univ, dirSupInaccOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α univ
rw : DirSupInaccOn univ s ↔ DirSupInacc s
⊢ IsOpen[t] s ↔ DirSupInacc s
have rw₁ : DirSupInacc s ↔ DirSupInacc s
Tactic: rw [isOpen_iff_dirSupInaccOn isLowerSet_univ, dirSupInaccOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α univ
⊢ IsClosed[t] s ↔ DirSupClosed s
have rw : DirSupClosedOn univ s ↔ DirSupClosed s
Tactic: rw [isClosed_iff_dirSupClosedOn isLowerSet_univ, dirSupClosedOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α univ
rw : DirSupClosedOn univ s ↔ DirSupClosed s
⊢ IsClosed[t] s ↔ DirSupClosed s
have rw₁ : DirSupClosed s ↔ DirSupClosed s
Tactic: rw [isClosed_iff_dirSupClosedOn isLowerSet_univ, dirSupClosedOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
⊢ IsOpen[inst_1] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s
have rw : IsOpen[scott α D] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s
Tactic: rw [topology_eq α D]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
⊢ IsOpen[inst_1] s ↔ IsUpperSet s ∧ DirSupInaccOn D s
have rw : IsUpperSet s ∧ IsOpen[scottHausdorff α D] s ↔ IsUpperSet s ∧ DirSupInaccOn D s
Tactic: rw [isOpen_iff_isUpperSet_and_scottHausdorff_open (D := D)]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
⊢ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s ↔ IsUpperSet s ∧ DirSupInaccOn D s
have refine : ∀ (h : IsUpperSet s) (h' : DirSupInaccOn D s) (d : Set α) (d₀ : d ∈ D) (d₁ : d.Nonempty)
  (d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (x : α) (d₃ : IsLUB d x) (ha : x ∈ s), ∃ b ∈ d, Ici b ∩ d ⊆ s
Tactic: refine and_congr_right fun h ↦
    ⟨IsScottHausdorff.dirSupInaccOn_of_isOpen (t := scottHausdorff α D),
      fun h' d d₀ d₁ d₂ _ d₃ ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
h : IsUpperSet s
h' : DirSupInaccOn D s
d : Set α
d₀ : d ∈ D
d₁ : d.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
x : α
d₃ : IsLUB d x
ha : x ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s
have obtain : ∀ (b : α) (hbd : b ∈ d) (hbu : b ∈ s), ∃ b ∈ d, Ici b ∩ d ⊆ s
Tactic: obtain ⟨b, hbd, hbu⟩ := h' d₀ d₁ d₂ d₃ ha
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ IsClosed[inst_1] s ↔ IsLowerSet s ∧ DirSupClosed s
have rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
    dirSupInaccOn_univ, dirSupInacc_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s ∧ DirSupClosed s
have rw₁ : IsUpperSet sᶜ ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
    dirSupInaccOn_univ, dirSupInacc_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
rw₁ : IsUpperSet sᶜ ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s ∧ DirSupClosed s
have rw₂ : IsLowerSet s ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
    dirSupInaccOn_univ, dirSupInacc_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
rw₁ : IsUpperSet sᶜ ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
rw₂ : IsLowerSet s ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s ∧ DirSupClosed s
have rw₃ : IsLowerSet s ∧ DirSupInacc sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
    dirSupInaccOn_univ, dirSupInacc_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
rw₁ : IsUpperSet sᶜ ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
rw₂ : IsLowerSet s ∧ DirSupInaccOn univ sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
rw₃ : IsLowerSet s ∧ DirSupInacc sᶜ ↔ IsLowerSet s ∧ DirSupClosed s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s ∧ DirSupClosed s
have rw₄ : IsLowerSet s ∧ DirSupClosed s ↔ IsLowerSet s ∧ DirSupClosed s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
    dirSupInaccOn_univ, dirSupInacc_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s
have h : (↑(lowerClosure s) : Set α) = closure[upperSet α] s
Tactic: convert! closure.mono (@upperSet_le_scott α _)
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
h : (↑(lowerClosure s) : Set α) = closure[upperSet α] s
⊢ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s
have h₁ : inst_1 = scott α univ
Tactic: convert! closure.mono (@upperSet_le_scott α _)