mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ ((g₁ x).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) =
    (g₁ x).lift fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1

Tactic:
]

Goal state after:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ ((g₁ x).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) =
    (g₁ x).lift fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a c + toIocDiv hp a b • p) =
    toIocDiv hp a c • p - toIocDiv hp a b • p

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a c + toIocDiv hp a b • p) =
    toIocDiv hp a c • p - toIocDiv hp a b • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a c

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a c
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
n : ℤ
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ a + p = a + p

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b - toIocDiv hp a b • p = a + p

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b - toIocDiv hp a b • p = a + p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ ⋂ i ∈ S, interior i = ⋂ s ∈ S, interior s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ ⋂ y, interior (f y) = ⋂ i, interior (f i)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
x✝ : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this : u \ s ⊆ t
⊢ u \ s ⊆ t

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
x✝ : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this : u \ s ⊆ t
⊢ u \ s ⊆ t
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
x✝ : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this✝ : u \ s ⊆ t
this : u \ s ⊆ ∅
⊢ u \ s ⊆ ∅

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
x✝ : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this✝ : u \ s ⊆ t
this : u \ s ⊆ ∅
⊢ u \ s ⊆ ∅
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
⊢ interior (⋂ i ∈ S, i) = interior (⋂ s ∈ S, s)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ⊆ closure t ↔ s ⊆ closure t

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
x✝ : toIcoMod hp a b + p = toIocMod hp a b
h : toIcoMod hp a b + p = toIocMod hp a b := x✝
⊢ ¬p = 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
x✝ : toIcoMod hp a b + p = toIocMod hp a b
h : toIcoMod hp a b + p = toIocMod hp a b := x✝
⊢ ¬p = 0
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ ⋃ i ∈ S, closure i = ⋃ s ∈ S, closure s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ ⋃ y, closure (f y) = ⋃ i, closure (f i)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s).HasBasis (fun s ↦ x ∈ s ∧ IsOpen[inst✝] s) fun s ↦ s

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s).HasBasis (fun s ↦ x ∈ s ∧ IsOpen[inst✝] s) fun s ↦ s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ a < a + p ∧ ∃ z, b = a + p + z • p

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ a < a + p ∧ ∃ z, b = a + p + z • p
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s ≤ f

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s ≤ f
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ interior s = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ Dense s

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ Dense s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (x : X), x ∈ closure s) ↔ ∀ (x : X), x ∈ closure s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Tactic:
]

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + toIcoDiv hp a b • p

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + toIcoDiv hp a b • p
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = interior s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∉ interior {x | x ∉ s} ↔ x ∉ interior {x | x ∉ s}

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ ¬toIcoMod hp a b = a → ∃ x, b - x • p ∈ Set.Ioo a (a + p)

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ ¬toIcoMod hp a b = a → ∃ x, b - x • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ (∃ᶠ (x : X) in 𝓝 x, x ∈ s) → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ∩ (interior s)ᶜ = closure s ∩ (interior s)ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst✝] t
⊢ t = t

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed s ↔ IsClosed s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b = toIocDiv hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b = toIocDiv hp a b + 1 ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (∃ n, b - a = n • p) ↔ ∃ m, b - a = m • p

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ s \ interior s = s \ interior s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ closure s \ interior s = closure s \ s

Tactic:
hs.interior_eq

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ closure s \ s = closure s \ s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ closure s \ s = closure s \ s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint (frontier s) s ↔ Disjoint (frontier s) s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ Order.succ (toIocDiv hp a b) = toIcoDiv hp a b

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ Order.succ (toIocDiv hp a b) = toIcoDiv hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ 𝓝 x ⊓ F ≠ ⊥ ↔ ¬𝓝 x ⊓ F = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) = ∅
⊢ interior (frontier s) = ∅

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) = ∅
⊢ interior (frontier s) = ∅