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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b

Tactic:
by
  simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsLE h]

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hV₁ : IsOpen[inst✝] V
hxV : x ∈ V
hV₂ : IsConnected V
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inl.refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ IsConnected (inl ⁻¹' s)

Tactic:
exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h

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

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

Tactic:
exact subset_trans (fun s => CountableGenerateSets.basic) h

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
⊢ False

Tactic:
have yt : y ∉ t := (h' ys).resolve_right (absurd yt')

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (Subtype.val '' Subtype.val ⁻¹' s)

Tactic:
rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : (∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, ↑i).Nonempty) → ((u ∪ v)ᶜ ∩ ⋂ i, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
⊢ ⋂ s, ↑s ⊆ b

Tactic:
· have h1 : x ∈ v :=
        (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
      suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
        from (huv.symm.mono this hau).left_le_of_le_sup_left hab
      · refine Subset.trans ?_ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
⊢ Dense (⋂₀ S)

Tactic:
rcases S.eq_empty_or_nonempty with h | h
  · simp [h]
  · rcases hS.exists_eq_range h with ⟨f, rfl⟩
    exact dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f ∧ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst✝, inst✝¹] g
hf : Continuous[inst✝¹, inst✝] f
g : Y → X
hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst✝, inst✝¹] g
⊢ IsHomeomorph f

Tactic:
· exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ Cauchy (f ×ˢ g)

Tactic:
by
  have := hf.1; have := hg.1
  simpa [cauchy_prod_iff, hf.1] using ⟨hf, hg⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
| IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp

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

Goal state before:
pp: β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
p : β × β
⊢ p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Tactic:
obtain ⟨x, y⟩ := p

Goal state after:
β : 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
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
by
    rw [cauchySeq_iff] at hu
    rcases hu _ (hV n) with ⟨N, H⟩
    exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
i : γ
hi : p i
⊢ ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i

Tactic:
exact (h i hi).imp fun N hN n hn => hN n hn N le_rfl

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

Goal state before:
pp: case h
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ w ∈ {V | V ∈ 𝓤 α ∧ SetRel.IsSymm V}

Tactic:
exact ⟨w_in, w_symm⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
⊢ x ∈ U.preimage (range g)

Tactic:
simp_rw [SetRel.preimage, exists_range_iff]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
⊢ x ∈ {a | ∃ i, (a, g i) ∈ U}
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
⊢ U.preimage (⋃ i, t i) ∈ ⨆ i, f i

Tactic:
simp_rw [U.preimage_iUnion, ← le_principal_iff, ← iSup_principal] at ht ⊢

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 ≤ ⨆ x, 𝓟 (U.preimage (t x))
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α × β → γ
⊢ UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f

Tactic:
by
  rw [UniformContinuous₂, uncurry_curry]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map g g ∘ Prod.map f f) (𝓤 γ)

Tactic:
← comap_comap

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩

Goal state after:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f • f') x = 0 x

Tactic:
Pi.smul_apply',

Goal state after:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x • f' x = 0 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f • f') x = 0 x

Tactic:
Pi.smul_apply',

Goal state after:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ f x • f' x = 0 x
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
i : ι
hi : i ∈ mulSupport fun i ↦ f i z
⊢ x ∈ U i

Tactic:
specialize hz i ⟨z, ⟨hi, hzn⟩⟩

Goal state after:
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
this : (mulSupport fun i ↦ f i z) ⊆ ↑hnf.toFinset
i : ι
hz : x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
hi : i ∈ mulSupport fun i ↦ f i z
⊢ x ∈ U i
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:
Pi.smul_apply',

Goal state after:
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 x • f i x = 0
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 M
inst✝ : SMulZeroClass R M
f : ι → X → M
h✝ : LocallyFinite fun i ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ (s i • f i) x = 0

Tactic:
Pi.smul_apply',

Goal state after:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝² : TopologicalSpace X
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : ι → X → M
h✝ : LocallyFinite fun i ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ s i x • f i x = 0
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F

Tactic:
simp_rw +instances [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace]
  rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ uniformSpace α β =
    UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) (uniformSpace δ₁ β) ⊓
      UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) (uniformSpace δ₂ β)

Tactic:
ext : 1
  refine le_antisymm (le_inf ?_ ?_) ?_
  · exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
  · exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
  · refine
      (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
    rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩ | ⟨y, rfl⟩)
    · exact hfg.1 y
    · exact hfg.2 y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ topologicalSpace α β 𝔖 =
    ⨅ s ∈ 𝔖,
      TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)

Tactic:
simp only [UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf]
  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₂
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

Tactic:
exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩

Goal state after:
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₂ m (map n f) g = map₂ (fun a b ↦ m (n a) b) f g

Tactic:
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, 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.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
⊢ UniformContinuousOn f S

Tactic:
by
  intro U hU; rw [mem_map]
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)]
  rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
  exact hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prodMk_nhds (h₁ y hyS)) <|
    Eventually.of_forall hxy

Goal state after:
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 : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p
⊢ TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p

Tactic:
rw [tendstoUniformly_iff_tendsto] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
⊢ TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
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
⊢ ∀ᶠ (i : ι) in p, ∀ (x : ↑t), t.domRestrict (F i) x ∈ s

Tactic:
by simpa using hF

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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
⊢ Continuous[instTopologicalSpaceProd, inst✝] fun p ↦ p.1 * p.2

Tactic:
by
    rw [continuous_iff_continuousAt]
    rintro ⟨x₀, y₀⟩
    have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) =
        ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) := by
      ext p
      simp [uncurry, mul_assoc]
    have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x := by
      ext x
      simp [mul_assoc]
    calc
      map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by
        rw [nhds_prod_eq]
      _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) := by
        unfold uncurry
        rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
      _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by
        rw [key, ← Filter.map_map]
      _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := map_mono hmul
      _ = 𝓝 (x₀ * y₀) := by
        rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z ℱ g
⊢ ∃ x, g x = z ∧ ClusterPt x ℱ

Tactic:
← ℱ.map_comap_of_surjective f_surj,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z (map f (comap f ℱ)) g
⊢ ∃ x, g x = z ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
⊢ closure[inst✝²] U ⊆ U * U

Tactic:
by
  intro x hx
  rw [mem_closure_iff_nhds] at hx
  have hkey : (fun y => x / y) ⁻¹' U ∈ 𝓝 x :=
    ContinuousAt.preimage_mem_nhds (by fun_prop) (by simpa)
  obtain ⟨a, ha_mem, ha_s⟩ := hx _ hkey
  exact Set.mem_mul.mpr ⟨x / a, ha_mem, a, ha_s, div_mul_cancel x a⟩

Goal state after: