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

Goal state before:
pp: case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
⊢ ∀ (a : β) (u : Set β),
    a ∈ u → IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
· intro a u ha hu
    rcases (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf'
      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
    refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩ <;> simp only [Finite.mem_toFinset, mem_iInter]
    · exact fun i hi ↦ (hU i hi).1
    · exact fun i hi ↦ (hU i hi).2
    · exact hUu

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ⋂₀ f u ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}

Tactic:
sInter_eq_biInter

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ⋂ i ∈ f u, i ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ i, t i).Nonempty

Tactic:
contrapose! hst

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ cocompact X ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
rw [Filter.mem_cocompact]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsClosed[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), g x ⤳ f x
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
by
  simpa only [piecewise_compl] using hs.isOpen_compl.continuous_piecewise_of_specializes hg hf hspec

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x ↦ closure[inst✝] {x}) '' s) = s

Tactic:
· conv_rhs => rw [← H.Union_eq]
    simp

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f✝ : X → Y
inst✝ : IndiscreteTopology X
f : Filter X
hf : f.NeBot
⊢ f ≤ 𝓟 univ → ∃ x ∈ univ, ClusterPt x f

Tactic:
by simp [clusterPt_of_indiscreteTopology, nonempty_of_neBot f]

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

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact univ

Tactic:
Sigma.univ

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (⋃ a, range (Sigma.mk a))
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝 x ⊓ comap mk (𝓟 s)) = 𝓝[s] mk x

Tactic:
Filter.push_pull,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝 x) ⊓ 𝓟 s = 𝓝[s] mk x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x y : X
hd : Disjoint (𝓝 x) (𝓝 y)
he : x = y
⊢ False

Tactic:
simp [he, nhds_neBot.ne] at hd

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ

Tactic:
use Uᶜ, hU.compl_mem_nhds h₁x

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∀ y ∈ Uᶜ, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : ↑(irreducibleComponents Y)
⊢ (↑W ∩ range f).Nonempty

Tactic:
by simp [hf₄.range_eq, W.2.1.1]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := {y | y ∈ t ∩ s ∧ ¬y ⤳ p}
y : X
hy : y ∈ S
⊢ p ∈ (closure[inst✝] {y})ᶜ

Tactic:
simpa [specializes_iff_mem_closure] using hy.2

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ (Filter.comap f (𝓝 (f x))).HasBasis (fun s ↦ (IsOpen[inst✝²] s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) fun s ↦
    f ⁻¹' s

Tactic:
exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.isOpen_range.mem_nhds <| mem_range_self _) |>.comap _

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

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✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
x : α
y : β
U : Set (α × β)
hU : U ∈ 𝓝 (x, y)
⊢ ∃ V ∈ 𝓝 (x, y), IsPreconnected V ∧ V ⊆ U

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u✝ v✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
x : α
y : β
U : Set (α × β)
hU : U ∈ 𝓝 (x, y)
u : Set α
hu : u ∈ 𝓝 x
v : Set β
hv : v ∈ 𝓝 y
huv : u ×ˢ v ⊆ U
⊢ ∃ V ∈ 𝓝 (x, y), IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
obtain ⟨x | x, hx⟩ := hs.nonempty

Goal state after:
case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g

Tactic:
rcases h with ⟨S, Sg, Sct, hS⟩

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
P : α → α → Prop
inst✝ : Std.Symm P
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
x y : α
⊢ P x y

Tactic:
refine PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
P : α → α → Prop
inst✝ : Std.Symm P
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
x y z : α
⊢ ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
⊢ (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hsv

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ x ∈ s ∧ s ∈ B) closure[inst✝¹]

Tactic:
by
  simpa only [and_comm] using hB.nhds_hasBasis.nhds_closure

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
⊢ (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hsv

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
have hsU : s ⊆ ⋃ i, U i := by
    simp only [U, Pi.compl_apply]
    rw [← compl_iInter]
    apply disjoint_compl_left_iff_subset.mp
    simp only [compl_iInter, compl_iUnion, compl_compl]
    apply Disjoint.symm
    exact disjoint_iff_inter_eq_empty.mpr hst

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : ∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ i, t i).Nonempty

Tactic:
contrapose! hst

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
iSets : ∀ i_1 ∈ s, ∃ r, r.Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r, U i_2
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1

Tactic:
choose! r hr using iSets

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b

Tactic:
by
  refine ⟨?_, fun H a b ha hb hsab hsa hsb ↦ ?_⟩
  · contrapose!
    rintro ⟨a, b, ha, hb, ha', hb', hab, rfl⟩ H
    exact (H a b ha.isOpen hb.isOpen subset_rfl (by rwa [union_inter_cancel_left])
      (by rwa [union_inter_cancel_right])).ne_empty (by grind)
  · rw [nonempty_iff_ne_empty]
    intro h
    exact H (s ∩ a) (s ∩ b)
      (isClopen_inter_of_disjoint_cover_clopen' hs hsab ha hb (by grind))
      (isClopen_inter_of_disjoint_cover_clopen' hs (by grind) hb ha (by grind))
      hsa hsb (by grind [Set.disjoint_iff_inter_eq_empty]) (by grind)

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

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LindelofSpace (X i)
⊢ IsLindelof univ

Tactic:
Sigma.univ

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LindelofSpace (X i)
⊢ IsLindelof (⋃ a, range (Sigma.mk a))
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
c : Continuous[inst✝¹, inst✝] i
dense : ∀ (x : β), x ∈ closure[inst✝] (range i)
H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ (b : α), i b ∈ t → b ∈ s
a : α
⊢ comap i (𝓝 (i a)) ≤ 𝓝 a

Tactic:
simpa [Filter.le_def] using! H a

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 : β
⊢ IsConnected (f ⁻¹' connectedComponent t)

Tactic:
apply hcl.isConnected_preimage_of_isClosed
  · exact isClosed_connectedComponent
  · exact isConnected_connectedComponent
  · exact connected_fibers

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : s ∈ residual X
⊢ ¬IsMeagre s

Tactic:
rcases (mem_residual (X := X)).1 hs with ⟨t, ht_sub, htGδ, ht_dense⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : s ∈ residual X
t : Set X
ht_sub : t ⊆ s
htGδ : IsGδ t
ht_dense : Dense t
⊢ ¬IsMeagre s
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : s ∈ residual X
t : Set X
ht_sub : t ⊆ s
htGδ : IsGδ t
ht_dense : Dense t
hs_meagre : IsMeagre s
⊢ False

Tactic:
exact not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)

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
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
⊢ LocallyConnectedSpace X

Tactic:
by
  have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s)
      (h.symm '' ·) := fun x ↦ by
    rw [← h.symm_map_nhds_eq]
    exact (i.1 _).map _
  refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_
  exact hs.2.2.2.image _ h.symm.continuous.continuousOn

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

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y✝
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
ι : Type u_7
ι' : Type u_8
Y : ι' → Type u_9
inst✝ : (j : ι') → TopologicalSpace (Y j)
e : ι ≃ ι'
i : ι
⊢ Continuous[Pi.topologicalSpace, inst✝ (e i)] fun a ↦ (Equiv.piCongrLeft Y e).toFun a (e i)

Tactic:
simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using continuous_apply i

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : U ∈ UniformSpace.uniformity
x : α
⊢ Prod.mk x ⁻¹' U ∈ 𝓝 x

Tactic:
rw [UniformSpace.nhds_eq_comap_uniformity]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : U ∈ UniformSpace.uniformity
x : α
⊢ Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity
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}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ 𝓝 (x, y)

Tactic:
nhds_eq_uniformity_prod,

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}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ (𝓤 α).lift' fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ UniformContinuous id

Tactic:
by
  rw [uniformContinuous_iff_le_comap, uniformSpace_comap_id, id]

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

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ closure[inst✝] (mulSupport fun x ↦ 1) = ∅

Tactic:
mulSupport_fun_one,

Goal state after:
X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ closure[inst✝] ∅ = ∅
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1

Tactic:
by
  simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]

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

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f * f') x = 0 x

Tactic:
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p t

Tactic:
intro u hu x hx
  rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
  have : g ⁻¹' a ∈ 𝓝[t] x :=
    (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
  exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀

Tactic:
by
  simp only [EquicontinuousAt, forall_subtype_range_iff]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
(UniformFun.hasBasis_nhds ι α _).tendsto_right_iff

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
(UniformFun.hasBasis_nhds ι α _).tendsto_right_iff

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
by simp [neBot_iff, not_or]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x ↦ u ∘ x) ∘ F) S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff]

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ ContinuousWithinAt ((⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) S x₀ ↔
    ContinuousWithinAt (⇑ofFun ∘ swap ((fun x ↦ u ∘ x) ∘ F)) S x₀
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousAt F x ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x

Tactic:
hu.equicontinuousAt_iff

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x✝ : TopologicalSpace X := sInf ts
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun p ↦ p.1 • p.2

Tactic:
by
      -- Porting note: needs `( :)`
      rw [← (sInf_singleton (a := ‹TopologicalSpace M›) :)]
      exact
        continuous_sInf_rng.2 fun t ht =>
          continuous_sInf_dom₂ (Eq.refl _) ht
            (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))

Goal state after: