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

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) → LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_connectedComponentIn_open]
    refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_
    rw [connectedComponentIn_eq hy]
    rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
    exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝¹ x✝ : β
⊢ ∀ i ∈ Ico x✝ x✝¹, (s (succ i) ∩ s i).Nonempty

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder β
inst✝² : SuccOrder β
inst✝¹ : IsSuccArchimedean β
inst✝ : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝¹ x✝ : β
⊢ ∀ i ∈ Ico x✝ x✝¹, (s (succ i) ∩ s i).Nonempty

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
B : IsOpen[inst✝¹] u
C : u.Nonempty
D : u = univ
⊢ y ∈ u

Tactic:
simp [D]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ Disjoint (Ioi b) (Iio b)

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ f '' s ⊆ Ioi b ∪ Iio b

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
hfx : ∃ x ∈ s, b < f x
x : α
hx : x ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), f x ∉ Iio b

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
hfx : ∃ x ∈ s, f x < b
x : α
hx : x ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), f x ∉ Ioi b

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ s) → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ t

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
z : X i
hz : z ∈ s i
⊢ ∀ (j : ι), j ≠ i → I.piecewise f g j ∈ s j

Tactic:
exact fun j _ => this j trivial

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ (a ∪ b) ∩ (a ∩ b) = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ∩ a ∩ b = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ⊆ b ∪ a

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ∩ b ∩ a = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s = s ∩ a ∪ s ∩ b

Tactic:
grind

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ

Tactic:
intro h x

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
intro h x

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ (connectedComponent x).Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton

pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α

Tactic:
· intro h x
    apply h.1
    · exact subset_univ _
    exact isPreconnected_connectedComponent

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ x ∈ S, x ∈ {t | IsOpen[inst✝] t ∧ Dense t}) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s

Tactic:
mem_ofPred,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ x ∈ S, IsOpen[inst✝] x ∧ Dense x) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
⊢ TotallyDisconnectedSpace (ConnectedComponents α)

Tactic:
rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
⊢ ∀ (x : ConnectedComponents α), connectedComponent x = {x}
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Finite X
f : ℕ → Set X
x✝¹ : ∀ (n : ℕ), IsOpen[inst✝¹] (f n)
x✝ : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, IsOpen[inst✝¹] t

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Finite X
f : ℕ → Set X
x✝¹ : ∀ (n : ℕ), IsOpen[inst✝¹] (f n)
x✝ : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, Dense t

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
f : ℕ → Set ↑s
V : ℕ → Set X
hV✝ : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
x✝ : X
hG : IsGδ (⋂ n, V n)
hd : Dense (⋂ n, V n)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
⊢ (∀ (i : ℕ), x✝ ∈ g i ∧ x✝ ∈ V i) ↔ ∃ (x : ∀ (i : ℕ), x✝ ∈ V i), ∀ (i : ℕ), ⟨x✝, ⋯⟩ ∈ f i

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ Dense (c n)

Tactic:
dense_iff_closure_eq,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ closure[inst✝²] (c n) = univ
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ univ ⊆ interior (closure[inst✝²] s) ∪ (interior (closure[inst✝²] s))ᶜ

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
this : univ ⊆ closure[inst✝²] (c n)
⊢ closure[inst✝²] (c n) ⊆ univ ∧ univ ⊆ closure[inst✝²] (c n)

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense (⋂ n, c n)
x : Y
h : ∀ (i : ℕ), x ∈ f i
i : ℕ
⊢ p x ∈ p '' f i ∨ p x ∉ closure[inst✝²] s

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case h
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x : α
i : ι
hi : x ∈ U i
⊢ Quotient.lift (mk ∘ Subtype.val) ⋯ (mk ⟨x, hi⟩) = mk x

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s (h.symm (h x))
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x

Tactic:
h.symm_apply_apply

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = (⇑h '' {x})ᶜ

Tactic:
Set.image_singleton

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = {h x}ᶜ
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : Monoid M
⊢ TopologicalSpace.induced (Prod.fst ∘ ⇑(embedProduct M)) inst✝¹ ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ⇑(embedProduct M)) inst✝¹ =
    TopologicalSpace.induced val inst✝¹ ⊓ TopologicalSpace.induced (fun u ↦ ↑u⁻¹) inst✝¹

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin n → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons (a ∪ b) U))
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1))
h₂ : ∀ (i_1 : Fin (n + 1)), (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1)).Nonempty
h₄ : ⋃ i_1, Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1) = univ
hi : ¬IsConnected (a ∪ b)
j : Fin n
⊢ Disjoint (U j) a ∧ Disjoint (U j) b

Tactic:
simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
by
  rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
this : ∀ p ∈ s, ∃ t ⊆ cl_d, IsOpen[instTopologicalSpaceProd] t ∧ p ∈ t
⊢ ∃ t, IsOpen[instTopologicalSpaceProd] t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
choose t ht using this

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
⊢ ∃ t, IsOpen[instTopologicalSpaceProd] t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun s ↦ g (Prod.mk x ⁻¹' s)

Tactic:
Function.comp_def

Goal state after:
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun s ↦ g {y | (y, x) ∈ s}

Tactic:
nhds_eq_comap_uniformity',

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (comap (fun y ↦ (y, x)) (𝓤 α)).lift g = (𝓤 α).lift fun s ↦ g {y | (y, x) ∈ s}
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p p'

Tactic:
rfl

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x ↦ (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x ↦ (s.domRestrict f x.1, s.domRestrict f x.2)) (𝓤 ↑s) (𝓤 β)

Tactic:
rfl

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ instTopologicalSpaceProd = instUniformSpaceProd.toTopologicalSpace

Tactic:
rfl

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β) =
    Filter.comap (Prod.fst ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α) ⊓
      Filter.comap (Prod.snd ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 β)

Tactic:
Function.comp_def

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

Goal state before:
pp: α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
x✝ : α × β
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ (a, x✝.1) ∈ u ∧ (b, x✝.2) ∈ v) ↔ (∃ a ∈ s, (a, x✝.1) ∈ u) ∧ ∃ a ∈ t, (a, x✝.2) ∈ v

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
⊢ t ∈ (map (Prod.map mk mk) (𝓤 α)).lift' fun s ↦ SetRel.comp s s

Tactic:
by
    rcases comp_open_symm_mem_uniformity_sets ht with ⟨U, hU, hUo, -, hUt⟩
    refine mem_of_superset (mem_lift' <| image_mem_map hU) ?_
    simp only [subset_def, Prod.forall, SetRel.mem_comp, mem_image, Prod.ext_iff]
    rintro _ _ ⟨_, ⟨⟨x, y⟩, hxyU, rfl, rfl⟩, ⟨⟨y', z⟩, hyzU, hy, rfl⟩⟩
    have : y' ⤳ y := (mk_eq_mk.1 hy).specializes
    exact @hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : SeparationQuotient α × SeparationQuotient β → γ
⊢ Tendsto
      (((fun x ↦ (f x.1, f x.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun p ↦
        (Prod.map mk mk p.1, Prod.map mk mk p.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔
    Tendsto ((fun x ↦ (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ (mk ∘ f) a = mk (f a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
⊢ map f = g

Tactic:
ext ⟨a⟩
  calc
    map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
    _ = g ⟦a⟧ := congr_fun comm a

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ (∀ (s : Set (α × α)), s ∈ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ↔ s ∈ 𝓤 α) ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ 𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α ↔
    𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 γ)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ comap (fun x ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 γ) = comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ)

Tactic:
Function.comp_def

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ comap (fun x ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 γ) =
    comap (fun x ↦ ((fun x ↦ g (f x)) x.1, (fun x ↦ g (f x)) x.2)) (𝓤 γ)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x ↦ (a, u x)) f (𝓤 α)

Tactic:
rfl

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x ↦ (u x, a)) f (𝓤 α)

Tactic:
nhds_eq_comap_uniformity',

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (comap (fun y ↦ (y, a)) (𝓤 α)) ↔ Tendsto (fun x ↦ (u x, a)) f (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y ↦ (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x ↦ (u x, a)) f (𝓤 α)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q ↦ (↑q.1, ↑q.2)) ∘ fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (𝓤 α) =
    comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)

Tactic:
rfl

Goal state after: