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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
y : Y
e : y ⤳ f x
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x y : X
e : f y ⤳ f x
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = f y
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun x y ↦ ¬Inseparable x y

Tactic:
simp only [t0Space_iff_inseparable, Ne, not_imp_not, Pairwise]

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
h : x ≠ y
s : Set X
⊢ 𝓝[s \ {y}] x = 𝓝[s] x

Tactic:
sdiff_eq,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ 𝓝[s ∩ {y}ᶜ] x = 𝓝[s] x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))

Tactic:
by
  simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
    Set.mem_sdiff, mem_inter_iff, mem_compl_iff]
  congr! 7 with x - u y
  tauto

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ ⋃₀ (irreducibleComponents X \ {Z} ∪ {Z}) = univ

Tactic:
Set.sdiff_union_of_subset,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ ⋃₀ irreducibleComponents X = univ

X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ {Z} ⊆ irreducibleComponents X
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F) → ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l

Tactic:
intro cond x hx f h

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
hx : x ∈ U
f : Ultrafilter X
h : ↑f ≤ 𝓝 x
⊢ U ∈ f
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
⊢ (f ⁻¹' Z).Nonempty

Tactic:
obtain ⟨x, hx⟩ := hV.1.1; exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
⊢ ReflTransGen r n (succ m)

Tactic:
have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩

Goal state after:
case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
⊢ ReflTransGen r n (succ m)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen[inst✝¹] {x}

Tactic:
have D : {x} ∈ 𝓝 x := by simpa only [← sdiff_eq, sdiff_sdiff_cancel_left A] using inter_mem hs C

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
⊢ IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
rcases isEmpty_or_nonempty (∀ i, X i) with he | hne

Goal state after:
case refine_1.inl
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
he : IsEmpty ((i : ι) → X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
hne : Nonempty ((i : ι) → X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets

Tactic:
constructor <;> intro h
  · exact subset_trans (fun s => CountableGenerateSets.basic) h
  intro s hs
  induction hs with
  | basic hs => exact h hs
  | univ => exact univ_mem
  | superset _ st ih => exact mem_of_superset ih st
  | sInter Sct _ ih => exact (countable_sInter_mem Sct).mpr ih

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 : s ∩ (u ∩ v) = ∅ → s ∩ v = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
← Set.disjoint_iff_inter_eq_empty,

Goal state after:
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 (u ∩ v) → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)

Tactic:
simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using! hU

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

Goal state before:
pp: case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : (insert i I).piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
rw [Finset.piecewise_insert] at hI

Goal state after:
case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
hSv : (S ∩ v).Nonempty
⊢ S ∩ (u ∩ v) ⊆ univ.pi s ∩ (u ∩ v)

Tactic:
exact inter_subset_inter_left _ hsub

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
⊢ Dense (⋂ n, f n)

Tactic:
let s := range p

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
⊢ Dense (⋂ n, f n)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.symmetrize ∈ 𝓤 α

Tactic:
by
  apply (𝓤 α).inter_sets h
  rw [← comap_swap_uniformity]
  exact preimage_mem_comap h

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

Goal state before:
pp: case mp
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y : β
⊢ (x, y) ∈ V ○ M ○ W → (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

pp: case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y : β
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W

Tactic:
· rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
    exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry]⟩, hwz⟩

Goal state after:
case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y : β
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
induction n generalizing s with

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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun i ↦ ball x (s i)

Tactic:
rw [nhds_eq_comap_uniformity]
  exact h.comap (Prod.mk x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p (comap g p')

Tactic:
by
  rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢
  exact h.comp (tendsto_id.prodMap tendsto_comap)

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
m n : β
hmn : (N, N) ≤ (m, n)
⊢ (m, n) ∈ Prod.map f f ⁻¹' s

Tactic:
exact hN (hf hmn.1 hmn.2)

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ ∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y

Tactic:
simp only [t0Space_iff_inseparable, inseparable_iff_ker_uniformity, mem_ker]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x ↦ (f x, f b)) (𝓝 b) (𝓤 α)

Tactic:
by
  rw [ContinuousAt, tendsto_nhds_left]

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 : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
⊢ TendstoUniformlyOn F f l s

Tactic:
by
  rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]
  intro u hu
  rw [tendsto_prod_iff'] at hu
  specialize h (fun n => (u n).fst) hu.1
  rw [tendstoUniformlyOn_iff_tendsto] at h
  exact h.comp (tendsto_id.prodMk hu.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst✝².toTopologicalSpace] (e '' {x | p x})
c : γ
hc : Tendsto (fun x ↦ f ↑x) (comap (IsDenseEmbedding.subtypeEmb p e) (𝓝 ⟨b, this⟩)) (𝓝 c)
⊢ Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)

Tactic:
simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using! hc

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

Goal state before:
pp: α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (1 x) (f₂ x) = 1 x

Tactic:
hx₂,

Goal state after:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (1 x) (1 x) = 1 x
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this✝ : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
this : Subtype.val ∘ fwd = SeparationQuotient.mk ∘ hid.extend f
⊢ IsUniformInducing (hid.extend f)

Tactic:
by
    rw [← SeparationQuotient.isUniformInducing_mk.of_comp_iff, ← this]
    exact (isUniformInducing_val _).comp hfu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous[inst✝, inst✝²] g
⊢ TendstoLocallyUniformly (fun n ↦ F n ∘ g) (f ∘ g) p

Tactic:
← tendstoLocallyUniformlyOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous[inst✝, inst✝²] g
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p univ
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformly F f p
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformly (fun x ↦ g ∘ F x) (g ∘ f) p

Tactic:
← tendstoLocallyUniformlyOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformlyOn (fun x ↦ g ∘ F x) (g ∘ f) p univ
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformly F f p
hG : TendstoLocallyUniformly G g p
⊢ TendstoLocallyUniformly (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p

Tactic:
← tendstoLocallyUniformlyOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p univ
hG : TendstoLocallyUniformlyOn G g p univ
⊢ TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p univ
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F S x₀
⊢ EquicontinuousWithinAt F S x₀

Tactic:
by
  simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢
  unfold ContinuousWithinAt nhdsWithin at hk ⊢
  rw [nhds_iInf]
  exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (𝓤 (α → β)) = 𝓤 (α →ᵤ[{s | s.Finite}] β)

Tactic:
simp_rw [Pi.uniformity, comap_iInf, comap_comap]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ ⨅ i, comap ((fun a ↦ (a.1 i, a.2 i)) ∘ fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (𝓤 β) =
    𝓤 (α →ᵤ[{s | s.Finite}] β)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map (fun p ↦ n p.1 p.2) (f ×ˢ g)) h = map₂ m' f (map₂ n' g h)

Tactic:
← map_prod_eq_map₂ n',

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map (fun p ↦ n p.1 p.2) (f ×ˢ g)) h = map₂ m' f (map (fun p ↦ n' p.1 p.2) (g ×ˢ h))
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
⊢ map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h)

Tactic:
by
  rintro s ⟨t₁, ⟨u, hu, w₁, hw₁, ht₁⟩, t₂, ⟨v, hv, w₂, hw₂, ht₂⟩, hs⟩
  refine ⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩
  refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)
  · exact (image2_subset_left inter_subset_left).trans ht₁
  · exact (image2_subset_left inter_subset_right).trans ht₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)

Tactic:
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (fun x ↦ ((⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ F) ((toFun 𝔖) f) p s

Tactic:
by
  simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal, TendstoUniformlyOn,
    Function.comp_apply, mem_ofPred]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)

Tactic:
rw [pow_succ]
    exact mul_mem_mul (pow_mem_pow hs n) hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : 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
i : ι
x : ↑(S i)
⊢ Set.liftCover S (fun i ↦ ⇑(φ i)) hφ ⋯ ↑x = (φ i) x

Tactic:
Set.liftCover_coe _

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : 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
i : ι
x : ↑(S i)
⊢ (φ i) x = (φ i) x
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: case inl
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
s : Set E
⊢ closure[inst✝²] (0 • s) = 0 • closure[inst✝²] s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)
    · simp
    · rw [zero_smul_set hs, zero_smul_set hs.closure]
      exact closure_singleton

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

Goal state before:
pp: G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
hf.uniformContinuous_iff,

Goal state after:
G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous (⇑f ∘ fun p ↦ p.1 / p.2)