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

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

pp: case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ¬ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
· exact ⟨y, Or.inl rfl, hy⟩

Goal state after:
case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ¬ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a
α : 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' : β
ht' : t' ∈ T₁
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t

Tactic:
hf.preimage_subset_preimage_iff,

Goal state after:
case a
α : 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' : β
ht' : t' ∈ T₁
⊢ {t'} ⊆ t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a
α : 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' : β
ht' : t' ∈ T₂
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t

Tactic:
hf.preimage_subset_preimage_iff,

Goal state after:
case a
α : 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' : β
ht' : t' ∈ T₂
⊢ {t'} ⊆ t
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ 𝓝 x

Tactic:
hf.isInducing.nhds_eq_comap x

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
⊢ ∃ k, ⋃ i, (C (k i))ᶜ = ⋃ i, (C i)ᶜ

Tactic:
exact eq_open_union_nat (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
hs : ∀ (i : ι'), IsGδ (s i)
⊢ IsGδ (⋂ i, s i)

Tactic:
by
  choose T hTo hTc hTs using hs
  obtain rfl : s = fun i => ⋂₀ T i := funext hTs
  refine ⟨⋃ i, T i, ?_, countable_iUnion hTc, (sInter_iUnion _).symm⟩
  simpa [@forall_comm ι'] using hTo

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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ IsMeagre (⋃ i, f i)

Tactic:
by
  rw [IsMeagre, compl_iUnion]
  exact countable_iInter_mem.mpr hs

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
⊢ ∃ U V, IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
have h :=
      (isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed
        _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h
    obtain ⟨fin_a, ha⟩ := h
    -- This clopen and its complement will separate the connected components of `a` and `b`
    set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i
    have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
    exact ⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩

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 Z
W : Type u_5
inst✝ : TopologicalSpace W
f✝ f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
⊢ IsHomeomorph ⋯.connectedComponentsMap

Tactic:
have hbij := hf.connectedComponentsMap_bijective hf'
    exact ⟨hf.continuous.connectedComponentsMap_continuous,
      hf.connectedComponentsMap.isOpenMap_of_injective hbij.injective, hbij⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
⊢ CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod.map_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i

Tactic:
by
  simp_rw [tendstoUniformlyOn_iff_tendsto, hβ.tendsto_right_iff, eventually_prod_principal_iff]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
⊢ ⋃ i, U.preimage (t i) ∈ ⨆ i, f i

Tactic:
← le_principal_iff,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))
⊢ ⨆ i, f i ≤ 𝓟 (⋃ i, U.preimage (t i))
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
biUnion_eq_iUnion,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite ↑I
⊢ TotallyBounded (⋃ x, s ↑x) ↔ ∀ i ∈ I, TotallyBounded (s i)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
have hb := @UniformContinuous.inf_dom_left _ _ id ub1 ub2 ub1 (@uniformContinuous_id _ (id _))

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
by
  -- proof essentially copied from `continuous_inf_dom_right₂`
  have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
  have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
  have h_unif_cont_id :=
    @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb
  exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ h h_unif_cont_id

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
⊢ TotallyBounded (f '' s)

Tactic:
simp only [← Filter.totallyBounded_principal_iff, ← Filter.map_principal] at hs ⊢
  exact hs.map hf

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s

Tactic:
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (x : α × α'), x.1 ∈ s ∧ x.2 ∈ s' → (Prod.map (F m.1.1) (F' m.1.2) x, Prod.map (F m.2.1) (F' m.2.2) x) ∈ u

Tactic:
and_imp,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (x : α × α'), x.1 ∈ s → x.2 ∈ s' → (Prod.map (F m.1.1) (F' m.1.2) x, Prod.map (F m.2.1) (F' m.2.2) x) ∈ u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α✝ : Type u
β : Type v
uniformSpace : UniformSpace α✝
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
f✝ : Filter α
hf : Cauchy f✝
⊢ ∃ x, f✝ ≤ 𝓝 x

Tactic:
simpa using (isCompact_iff_totallyBounded_isComplete.1 isCompact_univ).2 _ hf

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
⊢ N ∈ map f (cocompact α)

Tactic:
rw [mem_map, mem_cocompact']

Goal state after:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ ∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : ι → X → R
h✝ : LocallyFinite fun i ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
⊢ (s i • f i) x = 0

Tactic:
by rw [Pi.smul_apply', h, zero_smul]

Goal state after:
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
t : Set X
hS : IsCoherentWith S
⊢ IsClosed[inst✝] t ↔ ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)

Tactic:
by
  simp only [← isOpen_compl_iff, hS.isOpen_iff, preimage_compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousWithinAt f s x

Tactic:
by
  refine Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_
  obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
  obtain ⟨u₂, h₂, hsymm, u₂₁⟩ : ∃ u ∈ 𝓤 β, (∀ {a b}, (a, b) ∈ u → (b, a) ∈ u) ∧ u ○ u ⊆ u₁ :=
    comp_symm_of_uniformity h₁
  rcases L u₂ h₂ with ⟨t, tx, F, hFc, hF⟩
  have A : ∀ᶠ y in 𝓝[s] x, (f y, F y) ∈ u₂ := Eventually.mono tx hF
  have B : ∀ᶠ y in 𝓝[s] x, (F y, F x) ∈ u₂ := Uniform.continuousWithinAt_iff'_left.1 hFc h₂
  have C : ∀ᶠ y in 𝓝[s] x, (f y, F x) ∈ u₁ :=
    (A.and B).mono fun y hy => u₂₁ (prodMk_mem_comp hy.1 hy.2)
  have : (F x, f x) ∈ u₁ :=
    u₂₁ (prodMk_mem_comp (refl_mem_uniformity h₂) (hsymm (A.self_of_nhdsWithin hx)))
  exact C.mono fun y hy => u₁₀ <| prodMk_mem_comp hy this

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₀) ↔ ∀ (x : X), ContinuousAt (⇑ofFun ∘ swap F) x

Tactic:
equicontinuousAt_iff_continuousAt

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Map

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x ↦ e (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ uniformSpace α β = ⨅ i, UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (uniformSpace (δ i) β)

Tactic:
by
  ext : 1
  simp_rw [iInf_uniformity, uniformity_comap]
  refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_
  rcases h_cover with ⟨I, I_finite, I_cover⟩
  refine HasBasis.iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _)
      |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
  rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩
  exact mem_iInter.mp hfg ⟨i, hi⟩ y

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 α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun p ↦ (n p.1, id p.2)) (f ×ˢ g) = map (fun p ↦ m (n p.1) p.2) (f ×ˢ map id g)

Tactic:
map_id

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun p ↦ (n p.1, id p.2)) (f ×ˢ g) = map (fun p ↦ m (n p.1) p.2) (f ×ˢ g)
Module: Mathlib.Order.Filter.NAry

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

Tactic:
map_id

Goal state after:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
⊢ l = l
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
f : Filter α
⊢ map id f = f

Tactic:
map_id

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
f : Filter α
⊢ f = f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁ ∈ f, t₁ * univ ⊆ s) → s = univ

Tactic:
rintro ⟨t, ht, hs⟩

Goal state after:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ (∃ t₂ ∈ f, univ * t₂ ⊆ s) → s = univ

Tactic:
rintro ⟨t, ht, hs⟩

Goal state after:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)

Tactic:
simp [← Ici_inter_Iic, h, inter_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
H : ⋃ i, S i = Set.univ
i : ι
⊢ ContinuousOn (Set.liftCover S (fun i ↦ ⇑(φ i)) hφ H) (S i)

Tactic:
by
    rw [continuousOn_iff_continuous_domRestrict]
    simpa +unfoldPartialApp only [Set.domRestrict, Set.liftCover_coe]
      using map_continuous (φ i)

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

Goal state before:
pp: M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed[Pi.topologicalSpace] {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}

Tactic:
simp only [Set.ofPred_forall]

Goal state after:
M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed[Pi.topologicalSpace] (⋂ i, ⋂ i_1, {x | x (i • i_1) = σ i • x i_1})
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
hγ : ((fun x ↦ γ • x) '' (V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ) ∩ (V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ)).Nonempty
⊢ γ • x = x

Tactic:
obtain ⟨_, ⟨z, hz, rfl⟩, hγz⟩ := hγ

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
hγz : (fun x ↦ γ • x) z ∈ V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
⊢ γ • x = x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsOpen[inst✝²] t
⊢ IsOpen[inst✝²] (⋃ a ∈ s, (fun x ↦ a / x) '' t)

Tactic:
exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
l : Filter α
m : α → G
a : G
h : Tendsto (fun x ↦ (m x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto m l (𝓝 a)

Tactic:
by simpa only [inv_inv] using h.inv

Goal state after: