awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Rolle
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_1 : 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 : 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:
⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩

Premises used: Set.Ioo_subset_Icc_self, IsExtrFilter.congr, IsExtrOn.on_subset, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Rolle
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_1 : 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 : 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:
exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩
-- Module: Mathlib.Topology.Order.Rolle
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, IsLocalExtr f c

Tactic:
let ⟨c, cmem, hc⟩ := exists_isExtrOn_Ioo_of_tendsto hab hfc ha hb
  ⟨c, cmem, hc.isLocalExtr <| Ioo_mem_nhds cmem.1 cmem.2⟩

Premises used: exists_isExtrOn_Ioo_of_tendsto, IsLocalExtr, Membership.mem, Exists, IsExtrOn.isLocalExtr, Ioo_mem_nhds, And, And.right, And.left, And.intro, Exists.intro, _private.0.exists_isLocalExtr_Ioo_of_tendsto.match_1, Set.Ioo
-- Module: Mathlib.Topology.Order.Rolle
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 (uIcc a b)
hfI : f a = f b
⊢ min a b < max a b

Tactic:
simp [hab.symm]

Premises used: Ne.symm
-- Module: Mathlib.Topology.Order.Rolle
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 (uIcc a b)
hfI : f a = f b
⊢ f (min a b) = f (max a b)

Tactic:
grind
-- Module: Mathlib.Topology.Order.Rolle
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)
⊢ 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
-- Module: Mathlib.Topology.Order.Rolle
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 (extendFrom (uIoo a b) f) (uIcc a b) c

Tactic:
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)

Premises used: eq_lim_at_right_extendFrom_uIoo, eq_lim_at_left_extendFrom_uIoo, continuousOn_uIcc_extendFrom_uIoo, Eq.symm, exists_uIoo_isExtrOn_uIcc, Eq.trans
-- Module: Mathlib.Topology.Order.Rolle
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)
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
⊢ ∃ 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)

Premises used: eq_lim_at_right_extendFrom_uIoo, eq_lim_at_left_extendFrom_uIoo, continuousOn_uIcc_extendFrom_uIoo, Set.uIoo, Eq.symm, exists_uIoo_isExtrOn_uIcc, Eq.trans
-- Module: Mathlib.Topology.Order.Rolle
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_1 : 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 : 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:
⟨c, hc, (hfc.on_subset uIoo_subset_uIcc_self).congr h (h hc)⟩

Premises used: IsExtrFilter.congr, IsExtrOn.on_subset, Set.uIoo_subset_uIcc_self, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Rolle
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_1 : 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 : 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:
exact ⟨c, hc, (hfc.on_subset uIoo_subset_uIcc_self).congr h (h hc)⟩
-- Module: Mathlib.Topology.Order.Rolle
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, IsLocalExtr f c

Tactic:
let ⟨c, cmem, hc⟩ := exists_isExtrOn_uIoo_of_tendsto hab hfc ha hb
  ⟨c, cmem, hc.isLocalExtr <| Ioo_mem_nhds cmem.1 cmem.2⟩

Premises used: IsLocalExtr, Membership.mem, Exists, exists_isExtrOn_uIoo_of_tendsto, IsExtrOn.isLocalExtr, Ioo_mem_nhds, Set.uIoo, And, And.right, And.left, And.intro, Exists.intro, _private.0.exists_isLocalExtr_uIoo_of_tendsto.match_1
-- Module: Mathlib.Topology.Order.ScottTopology
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
obtain : ∀ (b₁ : α) (hb₁d : b₁ ∈ d) (hb₁ds : Ici b₁ ∩ d ⊆ s), ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t

Tactic:
obtain ⟨b₁, hb₁d, hb₁ds⟩ := hs hd₀ hd₁ hd₂ hd₃ ha.1

Premises used: And.left
-- Module: Mathlib.Topology.Order.ScottTopology
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
obtain : ∀ (b₂ : α) (hb₂d : b₂ ∈ d) (hb₂dt : Ici b₂ ∩ d ⊆ t), ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t

Tactic:
obtain ⟨b₂, hb₂d, hb₂dt⟩ := ht hd₀ hd₁ hd₂ hd₃ ha.2

Premises used: And.right
-- Module: Mathlib.Topology.Order.ScottTopology
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
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
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t

Tactic:
obtain ⟨c, hcd, hc⟩ := hd₂ b₁ hb₁d b₂ hb₂d
-- Module: Mathlib.Topology.Order.ScottTopology
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
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:
⟨c, hcd, fun e ⟨hce, hed⟩ ↦ ⟨hb₁ds ⟨hc.1.trans hce, hed⟩, hb₂dt ⟨hc.2.trans hce, hed⟩⟩⟩

Premises used: Membership.mem, _private.0.Topology.scottHausdorff.match_3, Inter.inter, And.right, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Topology.Order.ScottTopology
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
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:
exact ⟨c, hcd, fun e ⟨hce, hed⟩ ↦ ⟨hb₁ds ⟨hc.1.trans hce, hed⟩, hb₂dt ⟨hc.2.trans hce, hed⟩⟩⟩
-- Module: Mathlib.Topology.Order.ScottTopology
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₀
obtain : ∀ (b : α) (hbd : b ∈ d) (hbds₀ : Ici b ∩ d ⊆ s₀), ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s

Tactic:
obtain ⟨b, hbd, hbds₀⟩ := h s₀ hs₀s hd₀ hd₁ hd₂ hd₃ has₀
-- Module: Mathlib.Topology.Order.ScottTopology
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 : α
hbd : b ∈ d
hbds₀ : Ici b ∩ d ⊆ s₀
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s

Tactic:
⟨b, hbd, Set.subset_sUnion_of_subset s s₀ hbds₀ hs₀s⟩

Premises used: Set.subset_sUnion_of_subset, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.ScottTopology
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 : α
hbd : b ∈ d
hbds₀ : Ici b ∩ d ⊆ s₀
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s

Tactic:
exact ⟨b, hbd, Set.subset_sUnion_of_subset s s₀ hbds₀ hs₀s⟩
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ IsScottHausdorff α D

Tactic:
@IsScottHausdorff.mk _ _ _ (scottHausdorff α D) rfl

Premises used: Topology.IsScottHausdorff.mk, rfl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
⊢ t = scottHausdorff α D

Tactic:
topology_eq_scottHausdorff

Premises used: Topology.IsScottHausdorff.topology_eq_scottHausdorff
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
⊢ IsOpen[t] 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:
simp +instances [topology_eq_scottHausdorff (α := α) (D := D), IsOpen, scottHausdorff]

Premises used: Topology.scottHausdorff, Topology.IsScottHausdorff.topology_eq_scottHausdorff, IsOpen
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
h : IsOpen[t] s
⊢ DirSupInaccOn D s

Tactic:
.of_inter_subset (isOpen_iff.1 h)

Premises used: DirSupInaccOn.of_inter_subset, Topology.IsScottHausdorff.isOpen_iff, Iff.mp
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
h : IsClosed[t] s
⊢ DirSupClosedOn D s

Tactic:
.of_compl (dirSupInaccOn_of_isOpen h.isOpen_compl)

Premises used: Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen, IsClosed.isOpen_compl, DirSupClosedOn.of_compl
-- Module: Mathlib.Topology.Order.ScottTopology
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
rw₁ 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
⊢ IsOpen[t] s ↔ DirSupInaccOn D s

Tactic:
rw [isOpen_iff (D := D), dirSupInaccOn_iff_inter_subset hDL]

Premises used: dirSupInaccOn_iff_inter_subset, Topology.IsScottHausdorff.isOpen_iff
-- Module: Mathlib.Topology.Order.ScottTopology
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
rw₂ rw₃ : DirSupClosedOn D s ↔ DirSupClosedOn D s
⊢ IsClosed[t] s ↔ DirSupClosedOn D s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_dirSupInaccOn hDL, dirSupInaccOn_compl]

Premises used: dirSupInaccOn_compl, Topology.IsScottHausdorff.isOpen_iff_dirSupInaccOn, isOpen_compl_iff
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
h : IsLowerSet s
⊢ IsOpen[t] s

Tactic:
(isOpen_iff_dirSupInaccOn hDL).2 h.dirSupInaccOn

Premises used: Iff.mpr, Topology.IsScottHausdorff.isOpen_iff_dirSupInaccOn, IsLowerSet.dirSupInaccOn
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α D
hDL : IsLowerSet D
h : IsUpperSet s
⊢ IsClosed[t] s

Tactic:
(isClosed_iff_dirSupClosedOn hDL).2 h.dirSupClosedOn

Premises used: Iff.mpr, IsUpperSet.dirSupClosedOn, Topology.IsScottHausdorff.isClosed_iff_dirSupClosedOn
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α univ
rw : DirSupInaccOn univ s ↔ DirSupInacc s
rw₁ rw₂ : DirSupInacc s ↔ DirSupInacc s
⊢ IsOpen[t] s ↔ DirSupInacc s

Tactic:
rw [isOpen_iff_dirSupInaccOn isLowerSet_univ, dirSupInaccOn_univ]

Premises used: isLowerSet_univ, Topology.IsScottHausdorff.isOpen_iff_dirSupInaccOn, dirSupInaccOn_univ
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
s : Set α
inst : Preorder α
t : TopologicalSpace α
inst_1 : IsScottHausdorff α univ
rw : DirSupClosedOn univ s ↔ DirSupClosed s
rw₁ rw₂ : DirSupClosed s ↔ DirSupClosed s
⊢ IsClosed[t] s ↔ DirSupClosed s

Tactic:
rw [isClosed_iff_dirSupClosedOn isLowerSet_univ, dirSupClosedOn_univ]

Premises used: isLowerSet_univ, dirSupClosedOn_univ, Topology.IsScottHausdorff.isClosed_iff_dirSupClosedOn
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ upperSet α ≤ scott α univ

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ scottHausdorff α univ ≤ scott α univ

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α D
⊢ inst_1 = scott α D

Tactic:
topology_eq_scott

Premises used: Topology.IsScott.topology_eq_scott
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
rw : IsOpen[scott α D] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s
⊢ IsOpen[inst_1] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Tactic:
rw [topology_eq α D]

Premises used: Topology.IsScott.topology_eq
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
⊢ IsOpen[scott α D] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Tactic:
rfl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
rw : IsUpperSet s ∧ IsOpen[scottHausdorff α D] s ↔ IsUpperSet s ∧ DirSupInaccOn D s
⊢ IsOpen[inst_1] s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Tactic:
rw [isOpen_iff_isUpperSet_and_scottHausdorff_open (D := D)]

Premises used: Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open
-- Module: Mathlib.Topology.Order.ScottTopology
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

Tactic:
and_congr_right fun h ↦
    ⟨IsScottHausdorff.dirSupInaccOn_of_isOpen (t := scottHausdorff α D),
      fun h' d d₀ d₁ d₂ _ d₃ ha ↦ ?_⟩

Premises used: Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen, and_congr_right, Iff.intro
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
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
⊢ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Tactic:
refine and_congr_right fun h ↦
    ⟨IsScottHausdorff.dirSupInaccOn_of_isOpen (t := scottHausdorff α D),
      fun h' d d₀ d₁ d₂ _ d₃ ha ↦ ?_⟩

Premises used: Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen, and_congr_right, Iff.intro
-- Module: Mathlib.Topology.Order.ScottTopology
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
obtain : ∀ (b : α) (hbd : b ∈ d) (hbu : b ∈ s), ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
obtain ⟨b, hbd, hbu⟩ := h' d₀ d₁ d₂ d₃ ha
-- Module: Mathlib.Topology.Order.ScottTopology
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 : α
hbd : b ∈ d
hbu : b ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
⟨b, hbd, Subset.trans inter_subset_left (h.Ici_subset hbu)⟩

Premises used: Set.Subset.trans, IsUpperSet.Ici_subset, Set.inter_subset_left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.ScottTopology
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 : α
hbd : b ∈ d
hbu : b ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
exact ⟨b, hbd, Subset.trans inter_subset_left (h.Ici_subset hbu)⟩
-- Module: Mathlib.Topology.Order.ScottTopology
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
rw₄ rw₅ : IsLowerSet s ∧ DirSupClosed s ↔ IsLowerSet s ∧ DirSupClosed s
⊢ IsClosed[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]

Premises used: dirSupInacc_compl, isUpperSet_compl, dirSupInaccOn_univ, Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn, isOpen_compl_iff
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α D
⊢ IsOpen[inst_1] s → IsUpperSet s

Tactic:
fun h ↦
  (isOpen_iff_isUpperSet_and_scottHausdorff_open (D := D).mp h).left

Premises used: And.left, Iff.mp, Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open