mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∀ u ∈ {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}, IsOpen[ts] u

pp: case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}} ⊆
    {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}

Tactic:
·

Goal state after:
case refine_1
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∀ u ∈ {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}, IsOpen[ts] u
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1.hs
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ f, Ioi a)

pp: case ht
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)

Tactic:
·

Goal state after:
case refine_1.hs
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ f, Ioi a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case ht
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)

Tactic:
·

Goal state after:
case ht
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

pp: case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
·

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∃ x, ¬b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∀ (x : α), b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∃ x, ¬b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∀ (x : α), b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∀ (x : α), b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
·

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∃ x, ¬f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∃ x, ¬f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y < a✝, b✝ ≤ f y

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y < a✝, b✝ ≤ f y
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : IsMax a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : IsMax a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
·

Goal state after:
case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

pp: case inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
·

Goal state after:
case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ Icc a a ∪ ∅ = Icc a a

Tactic:
union_empty

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ Icc a a = Icc a a
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
·

Goal state after:
case inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIcoDiv hp a =ᶠ[𝓝[≥] x] fun x_1 ↦ toIcoDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]
  apply Ico_mem_nhdsGE_of_mem
  rw [← sub_mem_Ico_iff_left, ← toIcoDiv_eq_iff]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

pp: case inr.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
hy : x ≠ x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

pp: case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
hy : x ≠ x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

pp: case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
·

Goal state after:
case inr.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
hy : x ≠ x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
·

Goal state after:
case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ x ∈ {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ x ∈ {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ x ∈ {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Tactic:
·

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Tactic:
·

Goal state after:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case inl
⊢ (int.divByNat 0) ↑0 = 0

pp: case inr
n : ℕ
h0 : n ≠ 0
⊢ (int.divByNat n) ↑n = 0

Tactic:
·

Goal state after:
case inl
⊢ (int.divByNat 0) ↑0 = 0
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case pos
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) ↑(addOrderOf a) = 0

pp: case neg
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : ¬addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a))) ↑(addOrderOf a) = 0

Tactic:
·

Goal state after:
case pos
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) ↑(addOrderOf a) = 0
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case neg
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : ¬addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a))) ↑(addOrderOf a) = 0

Tactic:
·

Goal state after:
case neg
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : ¬addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a))) ↑(addOrderOf a) = 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Ioi '' s ∪ Iio '' s ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}

pp: case refine_2
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ ∀ s_1 ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] s_1

Tactic:
·

Goal state after:
case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Ioi '' s ∪ Iio '' s ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ ∀ s_1 ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] s_1

Tactic:
·

Goal state after:
case refine_2
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ ∀ s_1 ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] s_1
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Ioi a)

pp: case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Ioi a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)