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

Goal state before:
pp: ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), R1Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact (closure[topologicalSpace] s) ↔ ∀ (i : ι), IsCompact (closure[inst✝¹ i] (eval i '' s))

Tactic:
simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x ↔ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
constructor <;> intro hfg

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
⊢ f x ≠ g x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
constructor <;> intro hfg

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝 x] g

case mpr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ U, IsOpen[inst✝] U ∧ U ∩ s = {x}

Tactic:
obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hs hx

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
⊢ ∃ U, IsOpen[inst✝] U ∧ U ∩ s = {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst✝¹] O₁
h1O₂ : IsOpen[inst✝¹] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
exact ⟨K \ O₁, K \ O₂, hK.diff h1O₁, hK.diff h1O₂, sdiff_subset_comm.mp h2O₁,
    sdiff_subset_comm.mp h2O₂, by rw [← sdiff_inter, hO.inter_eq, sdiff_empty]⟩

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ IsClopen (s ∩ a)

Tactic:
rw [show s ∩ a = s ∩ (s ∩ a) by simp]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ IsClopen (s ∩ (s ∩ a))
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ frontier {b | f b ≤ g b} ⊆ {b | f b = g b}

Tactic:
rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]
  rintro b ⟨hb₁, hb₂⟩
  refine le_antisymm hb₁ (closure_lt_subset_le hg hf ?_)
  convert! hb₂ using 2; simp only [not_le.symm]; rfl

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

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ (∃ i t, IsConnected t ∧ s = mk i '' t) → IsConnected s

Tactic:
rintro ⟨i, t, ht, rfl⟩

Goal state after:
case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
t : Set (X i)
ht : IsConnected t
⊢ IsConnected (mk i '' t)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.insert
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u : Set α
U : Finset (Set α)
uU : u ∉ U
IH :
  (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
    (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU : ∀ (u_1 v : Set α), u_1 ∈ insert u U → v ∈ insert u U → (s ∩ (u_1 ∩ v)).Nonempty → u_1 = v
hUo : ∀ u_1 ∈ insert u U, IsOpen[inst✝] u_1
hsU : s ⊆ ⋃₀ ↑(insert u U)
⊢ ∃ u_1 ∈ insert u U, s ⊆ u_1

Tactic:
| insert u U uU IH =>

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

Goal state before:
pp: case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
⊢ s ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
apply Subset.trans hs

Goal state after:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
⊢ ⋃ i ∈ r, interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
replace hs := mt (hs hsu)

Goal state after:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ¬(s ∩ (u ∩ v)).Nonempty → ¬(s ∩ v).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ i ∈ Subtype.val '' d, c i

Tactic:
biUnion_image

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ y ∈ d, c ↑y
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (F ∩ s)

Tactic:
inter_eq_right.mpr hsF

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩
⊢ s ⊆ F ∩ s

Tactic:
inter_eq_right.mpr hsF

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩
⊢ s ⊆ s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
connectedComponentIn_eq_empty hx

Goal state after:
case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ ∅ ⊆ connectedComponentIn G x
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ Disjoint (closure[inst✝¹] (e '' s)) (e '' t)

Tactic:
rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]

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

Goal state before:
pp: case insert
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsGδ s) → IsGδ (⋃₀ s✝)
h : ∀ s ∈ insert a✝¹ s✝, IsGδ s
⊢ IsGδ (⋃₀ insert a✝¹ s✝)

Tactic:
simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable) ∧
        (⋃ i ∈ x, i)ᶜ ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S

Tactic:
compl_subset_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable) ∧
        s ⊆ ⋃ i ∈ x, i) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsOpen[inst✝¹] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s) → ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
rintro ⟨S, hSo, hSd, Sct, Ss⟩

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen[inst✝¹] t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ ∃ t ⊆ s, IsGδ t ∧ Dense t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
IH :
  ∃ U,
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
| succ n IH =>

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst✝] (connectedComponent x)

Tactic:
by
  simp_rw [discreteTopology_iff_isOpen_singleton, ← connectedComponents_preimage_singleton,
    isQuotientMap_coe.isOpen_preimage, surjective_coe.forall]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
rw [cauchySeq_iff_tendsto] at hu
  exact ((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
by
  rw [UniformSpace.mem_nhds_iff]
  constructor
  · rintro ⟨V, V_in, V_sub⟩
    use SetRel.symmetrize V, symmetrize_mem_uniformity V_in, inferInstance
    exact Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub
  · rintro ⟨V, V_in, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
x : α
⊢ 𝓝 x = Filter.comap (Prod.mk x) (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β))

Tactic:
by
    simp only [nhds_induced, nhds_eq_comap_uniformity, comap_comap, Function.comp_def]

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ i, u i) = ⨅ i, comap f (u i)

Tactic:
ext : 1
  simp [uniformity_comap, iInf_uniformity]

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : ↑(S b)) (y : ↑(S !b)),
    U b x ≤ U (!b) y → Disjoint (ball (↑x) (B (U b x))) (ball (↑y) (B (U (!b) y)))
⊢ Disjoint (⋃ x, ball (↑x) (B (U false x))) (⋃ x, ball (↑x) (B (U true x)))

Tactic:
simp_rw [disjoint_iUnion_left, disjoint_iUnion_right]

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : ↑(S b)) (y : ↑(S !b)),
    U b x ≤ U (!b) y → Disjoint (ball (↑x) (B (U b x))) (ball (↑y) (B (U (!b) y)))
⊢ ∀ (i : ↑(S false)) (i_1 : ↑(S true)), Disjoint (ball (↑i) (B (U false i))) (ball (↑i_1) (B (U true i_1)))
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ (x : (ι × ι) × α),
    (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈
          t ∧
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈
          t →
      (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp only [and_imp, Prod.forall]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Tactic:
rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}

Tactic:
biUnion_image

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ Kᶜ ⊆ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f

Tactic:
compl_subset_compl,

Goal state after:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ mulSupport f ⊆ K) ↔ HasCompactMulSupport f
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩
  rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩
  exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a)
    (iUnion₂_mono fun b _ => ball_mono hiV b)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this✝ : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
this : Subtype.val ∘ fwd = SeparationQuotient.mk ∘ hid.extend f
⊢ IsUniformInducing (Subtype.val ∘ fwd)

Tactic:
exact (isUniformInducing_val _).comp hfu

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
φ : ι' → ι
⊢ UniformSpace.comap (fun g i' ↦ g (φ i')) (uniformSpace fun i' ↦ α (φ i')) =
    ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i'))

Tactic:
by
  simp [Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
⊢ IsUniformInducing (hid.extend f)

Tactic:
by
  let sf := SeparationQuotient.mk ∘ f
  have : CompleteSpace (closure (range sf)) :=
    isClosed_closure.isComplete.completeSpace_coe
  let ff : α → closure (range sf) := inclusion subset_closure ∘ rangeFactorization sf
  have hgu : IsUniformInducing ff :=
    (isUniformEmbedding_set_inclusion subset_closure).isUniformInducing.comp
      (SeparationQuotient.isUniformInducing_mk.comp h).rangeFactorization
  have hgd : DenseRange ff :=
    ((denseRange_inclusion_iff subset_closure).2 subset_rfl).comp
      rangeFactorization_surjective.denseRange (continuous_inclusion subset_closure)
  have hg : IsDenseInducing ff := hgu.isDenseInducing hgd
  let fwd := hid.extend ff
  have hfwd : UniformContinuous fwd :=
    uniformContinuous_uniformly_extend hi hid.dense hgu.uniformContinuous
  have hg' : UniformContinuous (hg.extend i) :=
    uniformContinuous_uniformly_extend hgu hgd hi.uniformContinuous
  have key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk := by
    ext x
    induction x using isClosed_property hid.dense
    · exact isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous)
        SeparationQuotient.continuous_mk
    · simpa [fwd, hid.extend_eq hgu.uniformContinuous.continuous]
        using hg.inseparable_extend hi.uniformContinuous.continuous.continuousAt
  have hfu : IsUniformInducing fwd := by
    refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_
    rw [Function.comp_assoc, key]
    exact SeparationQuotient.isUniformInducing_mk
  have hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆
      closure (range (SeparationQuotient.mk ∘ f)) := by
    refine ((SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense).trans
      (closure_mono (subset_of_eq ?_))
    rw [← range_comp]
    apply congrArg range
    funext x
    simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt)
  suffices Subtype.val ∘ fwd = SeparationQuotient.mk ∘ hid.extend f by
    rw [← SeparationQuotient.isUniformInducing_mk.of_comp_iff, ← this]
    exact (isUniformInducing_val _).comp hfu
  rw [← coe_comp_rangeFactorization (SeparationQuotient.mk ∘ hid.extend f),
    ← val_comp_inclusion hrr, Function.comp_assoc, Subtype.val_injective.comp_left.eq_iff]
  refine hid.extend_unique ?_ ?_
  · simp [ff, hid.inseparable_extend h.uniformContinuous.continuous.continuousAt, sf]
  · exact (continuous_inclusion hrr).comp
      (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
        h.uniformContinuous).continuous).rangeFactorization

Goal state after: