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

Goal state before:
pp: X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
⊢ t = t'

Tactic:
ext

Goal state after:
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (s₁ ∪ s₂)

Tactic:
by
  rw [union_eq_iUnion]; exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Tactic:
constructor

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty) → Dense s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ ↔ ¬IsOpen {x}

Tactic:
constructor

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ¬IsOpen {x} → Dense {x}ᶜ
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
⊢ t = t'

Tactic:
ext

Goal state after:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F

Tactic:
rw [disjoint_iff, ClusterPt, neBot_iff]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝[s \ {x}] x).NeBot

Tactic:
nhdsWithin

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
constructor

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)

case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst✝] ↔ (pure x ⊓ F.lift' closure[inst✝]).NeBot

Tactic:
constructor

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst✝] → (pure x ⊓ F.lift' closure[inst✝]).NeBot

case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (pure x ⊓ F.lift' closure[inst✝]).NeBot → pure x ≤ F.lift' closure[inst✝]
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₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Tactic:
constructor

Goal state after:
case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

case right
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ 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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
by
      have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
      have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
      rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'
      exact toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')

Goal state after:
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 : α
⊢ b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)

Tactic:
Set.mem_Ioc,

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
by rw [h.isOpen_compl.nhdsSet_eq]

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

Goal state before:
pp: 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
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U) ↔ ∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
constructor

Goal state after:
case mp
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
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U) → ∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

case 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
⊢ (∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U) → ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp
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 ∈ g ⁻¹' q '' V ↔ p x ∈ U

Tactic:
constructor

Goal state after:
case mp.mp
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 ∈ g ⁻¹' q '' V → p x ∈ U

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
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t 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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ (∀ (x : X), ContinuousAt f x) ↔ ∀ (x : X), ContinuousAt (g ∘ f) x

Tactic:
hg.continuousAt_iff

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ induced ofTopology t = ⊤ ↔ t = ⊤

Tactic:
constructor

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
⊢ induced ofTopology t = ⊤ → t = ⊤

case mpr
α : Type u
t : TopologicalSpace α
⊢ t = ⊤ → induced ofTopology t = ⊤
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.trans h.symm = Homeomorph.refl X

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : X
⊢ (h.trans h.symm) x✝ = (Homeomorph.refl X) x✝
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.symm.trans h = Homeomorph.refl Y

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : Y
⊢ (h.symm.trans h) x✝ = (Homeomorph.refl Y) x✝
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ t = ⊤ ↔ ∀ (x y : α), Inseparable x y

Tactic:
rw [← TopologicalSpace.indiscrete_iff_forall_inseparable, indiscreteTopology_iff]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔ ∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := ⋯
⊢ (∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) → ∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

case mpr
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := ⋯
⊢ (∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) → ∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : Y ≃ₜ Z
f : X → Y
h : IsOpenQuotientMap (⇑e ∘ f)
⊢ IsOpenQuotientMap f

Tactic:
simpa [← Function.comp_assoc] using e.symm.isOpenQuotientMap.comp h

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝[range f] f a

Tactic:
nhdsWithin

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝 (f a) ⊓ 𝓟 (range f)
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
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
f_surj : Surjective f
h : IsOpenMap (g ∘ f)
s : Set Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (g '' s)

Tactic:
by
  rw [← f_surj.image_preimage s, ← image_comp]
  exact h _ (hs.preimage hf)

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
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
constructor

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

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)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ (∃ i, ((x ∈ i.1 ∧ IsOpen[inst✝¹] i.1) ∧ y ∈ i.2 ∧ IsOpen[inst✝] i.2) ∧ i.1 ×ˢ i.2 ⊆ s) ↔
    ∃ u v, IsOpen[inst✝¹] u ∧ x ∈ u ∧ IsOpen[inst✝] v ∧ y ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (s.domRestrict f) x) → ∀ x ∈ s, ContinuousWithinAt f s x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) ↔ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ (⨅ i, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i) =
    (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x ↦ x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))

Tactic:
rw [iInf_split _ fun i => i ∈ I, inf_right_comm]

Goal state after:
ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ ((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i)) =
    (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x ↦ x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr
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[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
constructor

Goal state after:
case inr.mp
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[instTopologicalSpaceProd] (s ×ˢ t) → IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

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)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔
    ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) →
    ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite

Tactic:
constructor

Goal state after:
case mp
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) → U ∈ pure x ⊔ cofinite

case mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
refine ⟨fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_, fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
x✝ : ∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

case refine_2
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
x✝ : ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
v v' : Set β
hv' : IsOpen[t] v' ∧ f '' s ⊆ v' ∧ v' ⊆ v
hv : f ⁻¹' v ⊆ u
⊢ ∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsOpen[inst✝] (f ⁻¹' {b}ᶜ) ∧ IsOpen[inst✝] (f ⁻¹' {b})

Tactic:
Bool.compl_singleton,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsOpen[inst✝] (f ⁻¹' {!b}) ∧ IsOpen[inst✝] (f ⁻¹' {b})
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f ↔ (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)

Tactic:
constructor

Goal state after:
case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f → (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)

case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ ((IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)) → IsClosedMap f
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst✝²] (inl ⁻¹' Z) ∧ IsClosed[inst✝¹] (inr ⁻¹' Z)
⊢ f '' Z = (fun a ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun b ↦ f (inr b)) '' inr ⁻¹' Z

Tactic:
ext

Goal state after:
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst✝²] (inl ⁻¹' Z) ∧ IsClosed[inst✝¹] (inr ⁻¹' Z)
x✝ : Z✝
⊢ x✝ ∈ f '' Z ↔ x✝ ∈ (fun a ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun b ↦ f (inr b)) '' inr ⁻¹' Z
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
s✝ : Set β
⊢ s✝ ∈ map f (𝓝[s] x) ↔ s✝ ∈ 𝓝[f '' s] f x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ ((IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) ↔
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
constructor

Goal state after:
case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ ((IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) →
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g)) →
    (IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst✝¹, inst✝] f
h' : EqOn f (fun x ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝 b)

Tactic:
rw [← nhdsSet_singleton]
  exact h.tendsto_nhdsSet h'

Goal state after: