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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) s x

Tactic:
rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
h : ∀ P ⊆ S, ⋃₀ P = univ → ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ
⊢ ∀ P ⊆ S, univ ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ univ ⊆ ⋃₀ Q

Tactic:
simpa

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
h : ∀ (ι : Type u) (U : ι → ↑S), ⋃ i, ↑(U i) = univ → ∃ J, J.Finite ∧ ⋃ i ∈ J, ↑(U i) = univ
⊢ ∀ (ι : Type u) (U : ι → ↑S), univ ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ univ ⊆ ⋃ i ∈ J, ↑(U i)

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
⊢ y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)

Tactic:
rw [mem_closure_iff_clusterPt, principal_singleton]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
by rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅

Tactic:
suffices univ ∩ ⋂ i, (fun i : I ↦ s ↓∩ t i) i = ∅ by
    simpa [eq_empty_iff_forall_notMem] using
      (isCompact_iff_isCompact_univ.mp ks).elim_finite_subfamily_closed
      (fun i : I ↦ s ↓∩ t i) (fun i ↦ htc i.val i.prop) this

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
⊢ univ ∩ ⋂ i, (fun i ↦ s ↓∩ t ↑i) i = ∅
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ x ⤳ y ∧ y ⤳ x ↔ x ∈ closure[inst✝] {y} ∧ y ∈ closure[inst✝] {x}

Tactic:
by simp only [specializes_iff_mem_closure, and_comm]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ a ∈ univ ∩ frontier {a | p a}, Tendsto f (𝓝[univ ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ a ∈ univ ∩ frontier {a | p a}, Tendsto g (𝓝[univ ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn f (univ ∩ {a | p a})

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn g (univ ∩ {a | ¬p a})

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hp
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ∀ a ∈ univ ∩ frontier {a | p a}, f a = g a

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn f (univ ∩ closure[inst✝²] {a | p a})

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn g (univ ∩ closure[inst✝²] {a | ¬p a})

Tactic:
simpa

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

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsClosed[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
this : s \ U = s
⊢ False

Tactic:
exact (this.symm.subset hx).2 hxU

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
⊢ IsClosed[inst✝] s

Tactic:
by
  obtain ⟨_, rp, rt⟩ := isDiscrete_iff_forall_mem_exists_isClosed.mp ht s sd
  rw [← rt]
  exact rp.inter tc

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
by
  rcases eq_or_ne x y with rfl | hy
  · exact Eq.le rfl
  · rw [Ne.nhdsWithin_compl_singleton hy]
    exact nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst✝¹] s
⊢ (f ⁻¹' (s ∩ range f)).Nonempty

Tactic:
simpa

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
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Tactic:
by
  refine ⟨?_, fun h => monotone_nhdsSet h⟩
  simp_rw [Filter.le_def]; intro h x hx
  specialize h {x}ᶜ
  simp_rw [compl_singleton_mem_nhdsSet_iff] at h
  by_contra hxt
  exact h hxt hx

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
hs : S.Finite
⊢ Sᶜ ∈ cofinite

Tactic:
simpa

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ SeparatedNhds K L

Tactic:
simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
    disjoint_nhds_nhds_iff_not_inseparable]
  intro x hx y hy h
  exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s U : Set X
⊢ ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)

Tactic:
continuousOn_iff_continuous_domRestrict,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s U : Set X
⊢ Continuous[instTopologicalSpaceSubtype, _] (s.domRestrict U.boolIndicator) ↔ IsClopen (Subtype.val ⁻¹' U)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id →
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
intro h U hU
    rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩
    exact ⟨V, hVU, hV⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
⊢ IsOpen[inst✝¹] (connectedComponentIn F x)

Tactic:
by
  rw [isOpen_iff_mem_nhds]
  intro y hy
  rw [connectedComponentIn_eq hy]
  exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

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

Goal state before:
pp: case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
i : ι
hi : i ∈ {i | ¬PreconnectedSpace (X i)}
hiJ : i ∉ J
⊢ PreconnectedSpace (X i)

Tactic:
suffices himg : Function.eval i '' connectedComponent x = univ from
      ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩

Goal state after:
case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
i : ι
hi : i ∈ {i | ¬PreconnectedSpace (X i)}
hiJ : i ∉ J
⊢ Function.eval i '' connectedComponent x = univ
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ g

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.sInter
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
ih : ∀ s ∈ S, ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
| @sInter S Sct _ 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 ⋯)
⊢ ∀ i ∈ r, interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
intro i hi

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 : ↑s
hi : i ∈ r
⊢ interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯
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 → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
this : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Tactic:
← this

Goal state after:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
this : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x
⊢ s ⊆ ⋃ x ∈ t, U ↑x
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)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected (s i)

Tactic:
← eval_image_univ_pi hne

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected ((fun f ↦ f i) '' univ.pi s)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case h.right
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
⊢ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ ⋃ i_2 ∈ s, r i_2, U i_1

Tactic:
· refine iUnion₂_subset ?h.right.h
    intro i is
    simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
    intro x hx
    exact mem_biUnion is ((hr i is).2 hx)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (⋃ b, bif b then s else t)

Tactic:
exact isLindelof_iUnion fun b => by cases b <;> assumption

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

Goal state before:
pp: case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∀ i ∈ t, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
intro i hi

Goal state after:
case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
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
⊢ IsConnected (f ⁻¹' t)

Tactic:
refine ⟨Nonempty.preimage ht'.nonempty hf, ?_⟩

Goal state after:
α : 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
⊢ IsPreconnected (f ⁻¹' t)
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
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst✝²] (U i)
⊢ t ⊆ ⋃ i, U i → ∃ t_1, t_1.Countable ∧ t ⊆ ⋃ i ∈ t_1, U i

Tactic:
hcover

Goal state after:
X : Type u
Y : Type v
ι✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝ : Set X
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst✝²] (U i)
hcover : t ⊆ ⋃ i, U i
⊢ ∃ t_1, t_1.Countable ∧ t ⊆ ⋃ i ∈ t_1, U i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : IsMeagre (⋃ i, f ↑i)
⊢ IsMeagre (⋃ i ∈ I, f i)

Tactic:
simpa

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ ∀ t ∈ {s}, IsNowhereDense t

Tactic:
simpa

Goal state after:
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 ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
mem_residual_iff

Goal state after:
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
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : 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✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i : ι
x : ConnectedComponents ↑(U i)
j : ι
y : ConnectedComponents ↑(U j)
⊢ (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        ⟨i, x⟩ =
      (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        ⟨j, y⟩ →
    ⟨i, x⟩ = ⟨j, y⟩

Tactic:
intro hxy
    obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
    obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y
    replace hxy : ConnectedComponents.mk x.val = ConnectedComponents.mk y.val := hxy
    rw [ConnectedComponents.coe_eq_coe] at hxy
    obtain rfl : i = j := by
      apply hdisj.eq
      rw [Set.not_disjoint_iff]
      exact ⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩
    simp [← Set.image_val_inj, heq, hxy]

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
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ Continuous[inst✝, inst✝¹] ⇑e.symm

Tactic:
rw [e.continuous_symm_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ IsOpenMap ⇑e
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ IsHomeomorph f ↔ Continuous[inst✝³, inst✝²] f ∧ Bijective f

Tactic:
rw [isHomeomorph_iff_continuous_isClosedMap_bijective]
  refine and_congr_right fun hf ↦ ?_
  rw [eq_true hf.isClosedMap, true_and]

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

Goal state before:
pp: β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
by
  unfold Cauchy
  rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

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

Goal state before:
pp: case zero
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[0] t ⊆ s

Tactic:
simpa

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

Goal state before:
pp: case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)), Monotone fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

pp: case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
· exact fun s => monotone_const.set_prod monotone_preimage

Goal state after:
case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t

Tactic:
refine ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ closure[instTopologicalSpaceProd] w ⊆ t
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ SetRel.id ∈ (fun u ↦ 𝓤 α) u

Tactic:
SetRel.id,

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ {(a₁, a₂) | a₁ = a₂} ∈ (fun u ↦ 𝓤 α) u
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (x, y) ≤ 𝓤 α

Tactic:
h.prod rfl

Goal state after:
α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (y, y) ≤ 𝓤 α
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
x y : α
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V
⊢ ∀ {i : SetRel α α}, i ∈ 𝓤 α ∧ i.IsSymm → (x, y) ∈ id i

Tactic:
simpa

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Filter α)
hS : S.Finite
⊢ (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded

Tactic:
by
  rw [sSup_eq_iSup, totallyBounded_biSup hS]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
⊢ 𝓟 ((fun x ↦ (f x.1, f x.2)) ⁻¹' SetRel.id) = 𝓟 SetRel.id

Tactic:
SetRel.id,

Goal state after:
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
⊢ 𝓟 ((fun x ↦ (f x.1, f x.2)) ⁻¹' {x | x.1 = x.2}) = 𝓟 {x | x.1 = x.2}