mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [isOpen_iff_mem_nhds]

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
⊢ ∀ x_1 ∈ connectedComponentIn F x, connectedComponentIn F x ∈ 𝓝 x_1
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ Filter α

Tactic:
refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
⊢ ⋂₀ S ∈ {s | sᶜ ∈ l}

case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}
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 β
⊢ LocallyConnectedSpace (α × β)

Tactic:
by
  rw [locallyConnectedSpace_iff_connected_subsets]
  rintro ⟨x, y⟩ U hU
  obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
  exact ⟨connectedComponentIn u x ×ˢ connectedComponentIn v y,
    prod_mem_nhds (connectedComponentIn_mem_nhds hu) (connectedComponentIn_mem_nhds hv),
    isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn,
    (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s t : Set α
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
by
  simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (x : Set X) {a : X}, IsClosed[inst✝] xᶜ → a ∉ xᶜ → Disjoint (𝓝ˢ xᶜ) (𝓝 a)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x

Tactic:
forall_comm

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (b : X) (a : Set X), IsClosed[inst✝] aᶜ → b ∉ aᶜ → Disjoint (𝓝ˢ aᶜ) (𝓝 b)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s) →
    ∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  (∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x)) →
    ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝] s
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x].TFAE

Tactic:
tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s) →
    ∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  (∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x)) →
    ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝] s
tfae_3_to_1 : (∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝] s) → RegularSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x].TFAE
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case right
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 := ⋯
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
u : Set ι
hucount : u.Countable
husub : s ⊆ ⋃ i ∈ u, U i
⊢ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
← disjoint_compl_left_iff_subset

Goal state after:
case right
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 : Set ι
hucount : u.Countable
husub : Disjoint (⋃ i ∈ u, U i)ᶜ s
⊢ s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
apply H1 (hu.inter hs) (hv.inter hs)

Goal state after:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∩ s ∪ v ∩ s

case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case h.left
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_1 ∈ s, r i_1).Countable

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 (Countable.biUnion_iff hs).mpr ?h.left.a
    exact fun s hs ↦ (hr s hs).1

Goal state after:
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
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)
⊢ t ⊆ (e ⁻¹' closure[inst✝¹] (e '' s))ᶜ

Tactic:
← he.closure_eq_preimage_closure_image,

Goal state after:
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)
⊢ t ⊆ (closure[inst✝²] s)ᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_2
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)
⊢ s ⊆ (e ⁻¹' closure[inst✝¹] (e '' t))ᶜ

Tactic:
← he.closure_eq_preimage_closure_image,

Goal state after:
case refine_2
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)
⊢ s ⊆ (closure[inst✝²] t)ᶜ
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}
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
have fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v := by
    intro t' ht'
    apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu hv
    · exact Subset.trans (preimage_mono (singleton_subset_iff.2 ht')) huv
    rw [uv_disj.inter_eq, inter_empty]

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
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
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst✝¹] (f i)
⊢ ⋂ i, f i = ⋂₀ range f

Tactic:
rw [sInter_range]

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
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
have T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v := by
    apply eq_of_subset_of_subset
    · rw [← biUnion_preimage_singleton]
      refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
      rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
      exact ht'.1
    rintro a ⟨hat, hav⟩
    constructor
    · exact mem_preimage.1 hat
    · refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_left fun h => ?_
      exact uv_disj.subset_compl_left hav (h rfl)

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
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
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
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
h : ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S

Tactic:
obtain ⟨T, isNowhereDense, countable, cover⟩ := h

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
this : Continuous[?m.18, ?m.19] ⇑(Fin.appendEquiv m n)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun p ↦ Fin.append p.1 p.2

Tactic:
by exact this

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
⊢ y ∈ ⇑(embedProduct N) ⁻¹' Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) '' U ↔
    y ∈ ⇑(map f) '' ⇑(embedProduct M) ⁻¹' U

Tactic:
simp only [embedProduct, OneHom.coe_mk, Set.mem_preimage, Set.mem_image, Prod.mk.injEq,
    Prod.map, Prod.exists, MulOpposite.exists, MonoidHom.coe_mk]

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
⊢ (∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹) ↔
    ∃ x, (↑x, op ↑x⁻¹) ∈ U ∧ (map f) x = y
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ 𝓝 x✝ = comap (Prod.mk x✝) (𝓤 α ⊓ 𝓤 α)

Tactic:
rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] s)

Tactic:
closure_eq_cluster_pts

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded {a | ClusterPt a (𝓟 s)}
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
by
  have := hI.to_subtype
  rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
f : Filter α
hf : f.NeBot
⊢ f ≤ g → ∃ c ≤ f, Cauchy c

Tactic:
hfs

Goal state after:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
f : Filter α
hf : f.NeBot
hfs : f ≤ g
⊢ ∃ c ≤ f, Cauchy c
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : Set α
⊢ CompleteSpace ↑s ↔ IsComplete s

Tactic:
by
  rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,
    Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ {x | (f x, ℓ) ∈ s} ∈ p'

Tactic:
← eventually_iff

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst✝¹] K
hfK : ∀ x ∉ K, f x = 1
⊢ HasCompactMulSupport f

Tactic:
have : mulTSupport f ⊆ K := by
    rw [← h'K.closure_eq]
    apply closure_mono (mulSupport_subset_iff'.2 hfK)

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst✝¹] K
hfK : ∀ x ∉ K, f x = 1
this : mulTSupport f ⊆ K
⊢ HasCompactMulSupport f
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝² : UniformSpace β
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), (𝓤 (α i)).IsCountablyGenerated
⊢ (𝓤 ((i : ι) → α i)).IsCountablyGenerated

Tactic:
by
  rw [Pi.uniformity]
  infer_instance

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
⊢ UniformContinuous Equiv.ulift.invFun

Tactic:
by
      have hf : IsUniformInducing (@Equiv.ulift.{v, u} α).toFun := ⟨rfl⟩
      simp_rw [hf.uniformContinuous_iff]
      exact uniformContinuous_id

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔ UniformContinuous (⇑ofFun ∘ swap F)

Tactic:
by
  rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
i₁ : ι
his₁ : s₁ ⊆ t i₁
i₂ : ι
his₂ : s₂ ⊆ t i₂
⊢ ∃ z ∈ 𝔖, (fun x1 x2 ↦ x1 ⊆ x2) s₁ z ∧ (fun x1 x2 ↦ x1 ⊆ x2) s₂ z

Tactic:
rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
i₁ : ι
his₁ : s₁ ⊆ t i₁
i₂ : ι
his₂ : s₂ ⊆ t i₂
i : ι
hi₁ : t i₁ ⊆ t i
hi₂ : t i₂ ⊆ t i
⊢ ∃ z ∈ 𝔖, (fun x1 x2 ↦ x1 ⊆ x2) s₁ z ∧ (fun x1 x2 ↦ x1 ⊆ x2) s₂ z
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map₂ m (pure a) g = map (m a) g

Tactic:
by
  rw [← map_prod_eq_map₂, pure_prod, map_map]; rfl

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 α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
i : ι
hi : i ∈ (fun x ↦ F x y) ⁻¹' ball (f y) V
⊢ (F i x, z) ∈ id U

Tactic:
exact hVU ⟨_, ⟨_, hFy i, mem_ball_symmetry.2 hi⟩, hfy⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * y ≤ b

Tactic:
mul_right_comm,

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * y * c ≤ b * c
⊢ a * y ≤ b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d

Tactic:
rwa [mul_assoc, mul_le_mul_iff_left] at hxbd

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst✝¹, inst✝] f
⊢ (mkD f g) x = f x

Tactic:
mkD_of_continuous hf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst✝¹, inst✝] f
⊢ { toFun := f, continuous_toFun := hf } x = f x
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
hne : c ≠ 0
⊢ IsClosedMap fun x ↦ c • x

Tactic:
exact (Homeomorph.smulOfNeZero c hne).isClosedMap

Goal state after: