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

Goal state before:
pp: case inl
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a : α
⊢ {a}ᶜ ∈ 𝓝[≠] a

pp: case inr
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a x : α
hx : a ≠ x
⊢ {x}ᶜ ∈ 𝓝[≠] a

Tactic:
exacts [self_mem_nhdsWithin, eventually_ne_nhdsWithin hx]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅

Tactic:
split_ifs <;> simp [s.union_compl_self]

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

Goal state before:
pp: case insert.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U x) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
⊢ s = ⋃ i ∈ insert x t, update K x K₁ i

Tactic:
simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (univ.pi (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) fun x ↦ univ))

Tactic:
refine isPreconnected_univ_pi fun i ↦ ?_

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
⊢ Subsingleton ι

Tactic:
by
  rw [← not_nontrivial_iff_subsingleton]
  by_contra ⟨i, j, h_ne⟩
  replace h_ne : s i ∩ s j = ∅ := by
    simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne
  rcases isClopen_iff.mp (h_clopen i) with hi | hi
  · exact (h_nonempty i).ne_empty hi
  · rw [hi, univ_inter] at h_ne
    exact (h_nonempty j).ne_empty h_ne

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

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : Disjoint s ∅ → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof univ

Tactic:
hf.isInducing.isLindelof_iff,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (f '' univ)
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
r : X → X → Prop
inst✝ : LindelofSpace X
⊢ IsLindelof univ

Tactic:
rw [← range_quot_mk]
    exact isLindelof_range continuous_quot_mk

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)

Tactic:
by
  rw [biInter_eq_iInter]
  have := hs.to_subtype
  exact .iInter fun x => ht x x.2

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
⊢ IsGδ (⋃₀ S)

Tactic:
induction S, hS using Set.Finite.induction_on with

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
y : ConnectedComponents α
x : α
⊢ mk x = y

Tactic:
obtain ⟨y, rfl⟩ := surjective_coe y

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
x y : α
⊢ mk x = mk y
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 = ∅
V : Set (ConnectedComponents X)
hU : IsClopen (mk ⁻¹' V)
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU

Goal state after:
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 = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
this : Countable ↑S
⊢ Dense (⋂ x, f ↑x ⋯)

Tactic:
exact dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2

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

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : x ∈ ⋂ i, g i
⊢ x ∈ ⋃ i, interior (f i)

Tactic:
rw [mem_iInter] at hxg

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ i, interior (f i)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V

Tactic:
rintro ⟨u, v⟩ ⟨u_in, v_in⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).1 ∈ ball x w
v_in : (u, v).2 ∈ ball x w
⊢ (u, v) ∈ V
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K ↔ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
constructor
    · intro H
      have HKU : K ⊆ ⋃ _ : Unit, interior U := by
        simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
      obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU
      exact ⟨i, hpi, hi.trans interior_subset⟩
    · rintro ⟨i, hpi, hi⟩
      refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi
      exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi

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

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this : (mulSupport fun i ↦ f i z) ⊆ ↑hnf.toFinset
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
⊢ SeparableSpace α
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' x✝¹ ∈ p ×ˢ 𝓝[s] x✝³

Tactic:
mem_prod_iff_right,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    ∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (x : ι) in p, ∀ y ∈ t, (x, y) ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' x✝¹
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ TendstoLocallyUniformlyOn F f p (s ∪ s')

Tactic:
by
  rw [← sUnion_pair]
  refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_ <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ max a 1 / max a⁻¹ 1 = a

Tactic:
by
  rcases le_total a 1 with (h | h) <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
  rfl

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 → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀

Tactic:
rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_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 → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ ContinuousAt ((⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) x₀ ↔
    ContinuousAt (⇑ofFun ∘ swap ((fun x ↦ u ∘ x) ∘ F)) x₀
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 : x ∈ closure[tX] s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
mem_closure_iff_nhdsWithin_neBot

Goal state after:
ι : 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
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
⊢ 1 ≤ f / f

Tactic:
simpa using neBot_iff.mp h

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

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ c • closure[inst✝³] s = univ

Tactic:
hs,

Goal state after:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ c • univ = univ
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ TendstoUniformlyOn (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p t

Tactic:
rw [tendstoUniformlyOn_iff_restrict]
  apply UniformContinuousOn.comp_tendstoUniformly_eventually (by simpa using hF)
     (by simpa using hf) hg (tendstoUniformlyOn_iff_restrict.mp h)

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔
    Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
rw [isProperMap_iff_clusterPt]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_clusterPt]

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ Continuous[inst✝³, inst✝²] fun x ↦ ∏ᶠ (i : ι), f i x

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Goal state after:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
x : X
⊢ ContinuousAt (fun x ↦ ∏ᶠ (i : ι), f i x) x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
α : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace α
inst✝¹ : Zero α
inst✝ : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst✝⁵, inst✝²] f
⊢ f = 0 ∨ LocallyCompactSpace G

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_
  simp_rw [funext_iff, Pi.zero_apply] at h
  push Not at h
  obtain ⟨x, hx⟩ : ∃ x, f x ≠ 0 := h
  have : k ∈ 𝓝 x :=
    mem_of_superset (h'f.isOpen_support.mem_nhds hx) hf
  exact IsCompact.locallyCompactSpace_of_mem_nhds_of_group hk this

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1

Tactic:
show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x ↦ x * x₀⁻¹) ∘ fun x ↦ x₀ * x) (𝓝 1) = 𝓝 1
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ Tendsto f l atTop

Tactic:
by
  simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr

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

Goal state before:
pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ (fun y ↦ (y - b) / a) ((fun x ↦ a * x + b) x) = x

Tactic:
simp only [add_sub_cancel_right]
    exact mul_div_cancel_left₀ x h

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioo a (f i) = Ioo (update f i a) f

Tactic:
by simpa using image_update_Ioo f i a (f i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] (⋯.extend fun p ↦ (φ p.1) p.2)

Tactic:
refine continuous_extend_of_cauchy _ ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
⊢ ∀ (b : α × γ), Cauchy (map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 b)))
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
⊢ CompleteSpace (G ⧸ N)

Tactic:
let : UniformSpace G := IsTopologicalGroup.rightUniformSpace G

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
t : Set β
h : ⇑e '' s = t
x : β
hx : x ∈ t
⊢ e.symm x ∈ s

Tactic:
by
    subst t
    rcases hx with ⟨x, hx, rfl⟩
    rwa [e.symm_apply_apply]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
⊢ (𝓝 1).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ {b | |b|ₘ < ε}

Tactic:
by
  simpa using nhds_basis_mabs_div_lt (1 : α)

Goal state after: