mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
m : ℤ
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b + m • p) = toIocMod 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 : α
m : ℤ
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + m • p) b = m • p + toIocMod hp a b
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
s : Set β
⊢ f.lift' h ⊓ 𝓟 s = f.lift' fun t ↦ h t ∩ s

Tactic:
simp only [Filter.lift', Filter.lift, (· ∘ ·), ← inf_principal, iInf_subtype', ← iInf_inf]

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 : α
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b + p) = toIcoMod 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 : α
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (a + p) b = p + toIcoMod 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 : α
⊢ toIocMod hp a (p + b) = toIocMod hp a b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (b + p) = toIocMod 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 : α
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b

Tactic:
add_comm,

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen[inst✝] {x} ↔ 𝓝[≠] x = ⊥

Tactic:
isOpen_singleton_iff_nhds_eq_pure,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x = pure x ↔ 𝓝[≠] x = ⊥
Module: Mathlib.Topology.Closure

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

Tactic:
exact IsClosed.inter isClosed_closure isClosed_closure

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
hs : Dense s
⊢ f '' univ ⊆ closure[inst✝] (f '' s)

Tactic:
← hs.closure_eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
hs : Dense s
⊢ f '' closure[inst✝¹] s ⊆ closure[inst✝] (f '' 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 : α
⊢ toIcoMod hp a b = toIcoMod hp a b - a + a

Tactic:
sub_add_cancel

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIcoMod 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 : α
⊢ toIocMod hp a b = toIocMod hp a b - a + a

Tactic:
sub_add_cancel

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod 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 : α
⊢ p - toIocMod hp 0 (b - a) + toIocMod hp 0 (b - a) = p

Tactic:
sub_add_cancel

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ p = 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
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
have h₃₂ : x₃' - p < x₂' := sub_lt_iff_lt_add.2 (toIcoMod_lt_right _ _ _)

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∉ closure[inst✝] s ↔ 𝓝[s] x = ⊥

Tactic:
by
  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ (comap Subtype.val (𝓝 x)).NeBot

Tactic:
comap_neBot_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ ∀ t ∈ 𝓝 x, ∃ a, ↑a ∈ t
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : x ∈ closure[inst✝] (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure[inst✝] s₂

Tactic:
by
  rw [mem_closure_iff_nhds_ne_bot] at *
  rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ ↑(toIcoDiv hp a b) * p + toIcoMod hp a b = b

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ toIcoMod hp a b + ↑(toIcoDiv hp a b) * p = b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ ↑(toIocDiv hp a b) * p + toIocMod hp a b = b

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ toIocMod hp a b + ↑(toIocDiv hp a b) * p = b
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ (∀ f ∈ 𝓝 '' t, s ∈ f) ↔ ∀ x ∈ t, s ∈ 𝓝 x

Tactic:
forall_mem_image

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp (↑m * p + a) b = ↑m * p + toIcoMod hp a b

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp (a + ↑m * p) b = ↑m * p + toIcoMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a (↑m * p + b) = toIocMod hp a b

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a (b + ↑m * p) = toIocMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp (↑m * p + a) b = ↑m * p + toIocMod hp a b

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp (a + ↑m * p) b = ↑m * p + toIocMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - ↑⌊(b - a) / p⌋ * p - a ∧ b - ↑⌊(b - a) / p⌋ * p < a + p

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - ↑⌊(b - a) / p⌋ * p - a ∧ b - ↑⌊(b - a) / p⌋ * p < p + a
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp.mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
⊢ p x ∈ U → p x ∈ g ⁻¹' q '' V

Tactic:
intro H

Goal state after:
case mp.mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H✝ : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
H : p x ∈ U
⊢ p x ∈ g ⁻¹' q '' V
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
nhds_discrete,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ pure x ↔ x ∈ s
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Function.LeftInverse g ⇑f

Tactic:
convert! f.left_inv

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpenMap f ↔ ∀ {s : Set X}, closure[inst✝] (kernImage f s) ⊆ kernImage f (closure[inst✝¹] s)

Tactic:
rw [isOpenMap_iff_image_interior, compl_surjective.forall]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (x : Set X), f '' interior xᶜ ⊆ interior (f '' xᶜ)) ↔
    ∀ {s : Set X}, closure[inst✝] (kernImage f s) ⊆ kernImage f (closure[inst✝¹] s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})) → ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
intro H

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
⊢ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
by
  rw [Tendsto, ← map_map, hf.map_nhds_eq]; rfl

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ ⨆ s_1 ∈ range s, 𝓝[s_1] a = ⨆ i, 𝓝[s i] a

Tactic:
iSup_range

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ ⨆ i, 𝓝[s i] a = ⨆ i, 𝓝[s i] a
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅ → IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
intro H

Goal state after:
case inr.mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
closure_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[inst✝¹] s ×ˢ closure[inst✝] t
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝 x.1 ×ˢ 𝓝 x.2 ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
nhds_discrete,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (pure x.1 ×ˢ 𝓝 x.2 ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝 x.1 ×ˢ 𝓝 x.2 ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
nhds_discrete,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝 x.1 ×ˢ pure x.2 ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map f (𝓝 a ×ˢ 𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x ↦ f (a, x)) (𝓝 x)

Tactic:
nhds_discrete,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map f (pure a ×ˢ 𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x ↦ f (a, x)) (𝓝 x)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map f (𝓝 a ×ˢ 𝓝 b)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)

Tactic:
nhds_discrete,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map f (𝓝 a ×ˢ pure b)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 ↦ x_1 ∈ Ico x ⊤) y
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 ↦ x_1 ∈ Ico x ⊤) y
z : α
hyz : y < z
hz : z < ⊤
⊢ False
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t✝] cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure[inst✝] ct
⊢ s ×ˢ t ⊆ closure[instTopologicalSpaceProd] (cs ×ˢ ct)

Tactic:
closure_prod_eq

Goal state after:
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t✝] cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure[inst✝] ct
⊢ s ×ˢ t ⊆ closure[t✝] cs ×ˢ closure[inst✝] ct
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), f.NeBot → f ≤ g → p f

Tactic:
intro H

Goal state after:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
⊢ ∀ (f : Filter α), f.NeBot → f ≤ g → p f
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}

Tactic:
convert! IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S
  constructor <;> rintro ⟨U, F, hUT, hSU⟩
  · exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩
  · choose! U' hU' hUU' using hUT
    exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

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

Goal state before:
pp: α : Type u_1
⊢ ⊤.smallSets = ⊤

Tactic:
rw [smallSets, lift'_top, powerset_univ, principal_univ]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι ⊕ ι' → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)

Tactic:
by
  simp only [locallyFinite_iff_smallSets, ← forall_and, ← finite_preimage_inl_and_inr,
    preimage_ofPred_eq, (· ∘ ·), eventually_and]

Goal state after:
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ (univ.pi fun i ↦ ⋃ j, compactCovering (X i) j) = univ

pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ∀ (i : ι), Monotone (compactCovering (X i))

Tactic:
· simp only [iUnion_compactCovering, pi_univ]

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ∀ (i : ι), Monotone (compactCovering (X i))
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ s ⊆ ⋃ i, (interior ∘ ⇑K) i

Tactic:
intro x _

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
a✝ : x ∈ s
⊢ x ∈ ⋃ i, (interior ∘ ⇑K) i
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s

Tactic:
rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure]

Goal state after:
case hts
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ {a} ⊆ ↑s

case hst
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, b ≤ c → b ∈ {a}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst✝¹, inst✝] g
hf : Disjoint f (cocompact X)
⊢ Disjoint (map g f) (cocompact Y)

Tactic:
by
  rw [← Filter.disjoint_comap_iff_map, disjoint_iff_inf_le]
  calc
    f ⊓ (comap g (cocompact Y))
    _ ≤ f ⊓ Filter.cocompact X := inf_le_inf_left f (Filter.comap_cocompact_le hg)
    _ = ⊥ := disjoint_iff.mp hf

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier t = s ∩ frontier t

Tactic:
eq_comm

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s ∩ frontier t = s' ∩ frontier t