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

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
⊢ IsTopologicalBasis ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
subst t; let := generateFrom s
  refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
  · rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
    exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
  · rw [sUnion_image, iUnion₂_eq_univ_iff]
    exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
  · rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
    exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs
  · rw [← sInter_singleton t]
    exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (Homeomorph.refl X).sumCongr (Homeomorph.refl Y) = Homeomorph.refl (X ⊕ Y)

Tactic:
ext i
  cases i <;> rfl

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
⊢ (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)

Tactic:
ext i
  cases i <;> rfl

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃ i, ↑i

Tactic:
rw [← sUnion_eq_iUnion]

Goal state after:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
Module: Mathlib.Topology.Compactness.LocallyCompact

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✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.h₂
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ ⋃ i, a ↑i ⊆ u

Tactic:
simp
    grind

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

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✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∃ s ∈ l, q s) ↔ ∃ i, p i ∧ q (s i)

Tactic:
hl.exists_iff hq

Goal state after:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∃ i, p i ∧ q (s i)) ↔ ∃ i, p i ∧ q (s i)
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)

Tactic:
Filter.frequently_smallSets' hq,

Goal state after:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
⊢ (∀ t ∈ l, q t) ↔ ∀ (i : ι), p i → q (s i)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inl
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : IsEmpty ι
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
simp only [iUnion_of_empty, isSigmaCompact_empty]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst✝ : f.NeBot
hf : f ≤ 𝓟 t
x : X
hxs : x ∈ s
hxf : ClusterPt x f
y : X
hyt : y ∈ t
hxy : x ⤳ y
⊢ ∃ x ∈ t, ClusterPt x f

Tactic:
exact ⟨y, hyt, hxy.clusterPt hxf⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
⊢ T0Space X

Tactic:
by
  refine ⟨fun x y hxy => ?_⟩
  rcases h x y hxy with ⟨s, hxs, hys, hs⟩
  lift x to s using hxs; lift y to s using hys
  rw [← subtype_inseparable_iff] at hxy
  exact congr_arg Subtype.val hxy.eq

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
x x' : X
y : Y
hne : x' ≠ x
⊢ ContinuousAt (update f x y) x' ↔ ContinuousAt f x'

Tactic:
simp only [← continuousWithinAt_univ, continuousWithinAt_update_of_ne hne]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t

Tactic:
simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self {x},
    nhdsWithin_union, eventually_sup, nhdsWithin_singleton,
    eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ (∀ x ∈ S, S ⊆ closure[inst✝¹] {x}) → IsPreirreducible S

Tactic:
intro h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩
    exact ⟨x, hxs, hxu, (specializes_iff_mem_closure.mpr (h x hxs hys)).mem_open hv hyv⟩

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
a : α
⊢ closure[inst✝²] s ⊆ Iic a ↔ s ⊆ Iic a

Tactic:
isClosed_Iic.closure_subset_iff

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen[inst✝²] (Ioi a)

Tactic:
rw [← compl_Iic]
  exact isClosed_Iic.isOpen_compl

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
by
  simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsLT h]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∩ s ∪ f ⁻¹' v ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
v'_eq,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∩ s ∪ v' ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
⊢ Subsingleton ι

Tactic:
refine subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨?_, h_open i⟩)
  rw [← isOpen_compl_iff, compl_eq_univ_sdiff, ← h_Union, iUnion_sdiff]
  refine isOpen_iUnion (fun j ↦ ?_)
  rcases eq_or_ne i j with rfl | h_ne
  · simp
  · simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_open j

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
contrapose! hf
  simp only [notMem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢
  exact hs inf_le_right

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ ¬IsPreconnected s ↔ ∃ a b, IsClopen a ∧ IsClopen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b

Tactic:
simp [hs.isPreconnected_iff]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (range f)

Tactic:
rw [← image_univ]; exact isLindelof_univ.image hf

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Tactic:
refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

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

Tactic:
by
  obtain ⟨U, hU1, hU2⟩ := hs.eq_iInter_nat
  simp_all only [preimage_iInter]
  exact IsGδ.iInter_of_isOpen (fun i => hf.isOpen_preimage (U i) (hU1 i))

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing ⋯.connectedComponentsMap

Tactic:
by
  rw [← ConnectedComponents.isQuotientMap_coe.isCoinducing.of_comp_iff]
  exact ConnectedComponents.isQuotientMap_coe.isCoinducing.comp hf

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)

Tactic:
rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S

Tactic:
refine ⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩

Goal state after:
case isNowhereDense
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

case cover
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
this : Countable ↑t
hc : ∀ (x : ↑t), IsClosed[inst✝¹] (f ↑x)
hU : s ⊆ ⋃ x, f ↑x
⊢ Dense (⋃ x, interior (f ↑x))

Tactic:
exact hs.dense_iUnion_interior_of_closed hd hc hU

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 Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h ⁻¹' s) ↔ IsCompact s

Tactic:
rw [← image_symm]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s
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 Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s

Tactic:
rw [← image_symm]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)

Tactic:
by
        let _ : TopologicalSpace α := ⊥; have := discreteTopology_bot α
        simp [SetRel.id]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)

Tactic:
ext1

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)

Tactic:
exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : SetRel β β
f : α → α → β
hf : UniformContinuous fun p ↦ f p.1 p.2
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
by
  rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf
  rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩
  exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩

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 : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ mk ∘ g ∘ f = (map g ∘ map f) ∘ mk

Tactic:
simp only [Function.comp_def, map_mk, hf, hg]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ comap (fun x ↦ (g x.1, g x.2)) (𝓤 γ) ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Tactic:
← map_le_iff_le_comap,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x ↦ (g x.1, g x.2)) (map (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S))) ≤ 𝓤 γ ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
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 ↦ (a, u x)) f (𝓤 α)

Tactic:
rw [nhds_eq_comap_uniformity, tendsto_comap_iff]

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x ↦ (a, u x)) f (𝓤 α)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
⊢ closure[inst✝¹] (⇑f ⁻¹' mulSupport g) = ⇑f ⁻¹' closure[inst✝] (mulSupport g)

Tactic:
Homeomorph.preimage_closure

Goal state after:
X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
⊢ closure[inst✝¹] (⇑f ⁻¹' mulSupport g) = closure[inst✝¹] (⇑f ⁻¹' mulSupport g)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen[inst✝³] U
f : ↑U → β
cont : Continuous[instTopologicalSpaceSubtype, inst✝] f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt (extend Subtype.val f 1) x

Tactic:
rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _
      (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,
      ← (hU.isOpenEmbedding_subtypeVal).continuousAt_iff, extend_comp Subtype.val_injective]
    exact cont.continuousAt

Goal state after:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f

Tactic:
rw [compl_subset_comm]

Goal state after:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (mulTSupport f)ᶜ ⊆ f ⁻¹' N
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ (x : ↥t), ∀ᶠ (n : ι) in p, ∀ y ∈ U ↑↑x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
← eventually_all

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Tactic:
by
  refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
  choose U hU using h V hV
  obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
  replace hU := fun x : t => (hU x).2
  rw [← eventually_all] at hU
  refine hU.mono fun i hi x => ?_
  specialize ht (mem_univ x)
  simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht
  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
  exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))

Tactic:
← nhdsWithin_univ

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (UniformFun.basis α β 𝓕).filter ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets

Tactic:
← FilterBasis.generate,

Goal state after:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ generate (UniformFun.basis α β 𝓕).sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map (fun x ↦ f x b) l = l

Tactic:
funext h,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map (fun x ↦ x) l = l