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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rw [inter_comm s v', ← v'_eq] at this

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t✝ : Set X
h : t✝.Finite
τ : X
t : Set X
hτ : τ ∉ t
h₁t : t.Finite
h₂t : tᶜ ∈ codiscreteWithin s
⊢ (insert τ t)ᶜ ∈ codiscreteWithin s

Tactic:
have : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ := by aesop

Goal state after:
case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t✝ : Set X
h : t✝.Finite
τ : X
t : Set X
hτ : τ ∉ t
h₁t : t.Finite
h₂t : tᶜ ∈ codiscreteWithin s
this : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ
⊢ (insert τ t)ᶜ ∈ codiscreteWithin s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Std.Symm Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y

Tactic:
· -- TODO is there are better way to do this,
    -- so the case split produces `SeparationQuotient.mk` directly, rather than `Quot.mk`?
    -- Currently we need the `change` statement to recover this.
    rintro h ⟨x⟩ ⟨y⟩ sxspecsy
    change mk _ = mk _
    have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy
    have yspecx : y ⤳ x := h.symm x y xspecy
    rw [mk_eq_mk, inseparable_iff_specializes_and]
    exact ⟨xspecy, yspecx⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
⊢ y ∈ closure[inst✝¹] K ↔ ∃ x ∈ K, Inseparable x y

Tactic:
refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : y ∈ closure[inst✝¹] K
⊢ ∃ x ∈ K, Inseparable x y
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this✝ : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
this : SeparatedNhds (K \ U) (K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst✝¹] O₁
h1O₂ : IsOpen[inst✝¹] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i ↦ max a (f i)) l (𝓝[>] a)

Tactic:
by
  obtain ⟨h₁, h₂⟩ := tendsto_nhdsWithin_iff.mp h
  exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩

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

Goal state before:
pp: case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
have h : s ⊆ range Sum.inr :=
        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
      refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩
      · exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h
      · exact (image_preimage_eq_of_subset h).symm

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

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

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

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Set ι✝
ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨t, ?_⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Set ι✝
ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left✝ : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ t
⊢ s.Countable

Tactic:
exact ht.mono hssubt

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
Filter.map_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map (h ∘ g) (comap g (𝓝 d)) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
⊢ ⋂ Z, ↑Z ⊆ connectedComponent x

Tactic:
refine IsPreconnected.subset_connectedComponent ?_ (mem_iInter.2 fun s => s.2.2)

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
⊢ IsPreconnected (⋂ Z, ↑Z)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (coclosedCompact X) = coclosedCompact Y

Tactic:
rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ u '' univ ⊆ K

Tactic:
by rwa [image_univ, range_subset_iff]

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 ∈ {a | ∃ i, (a, g i) ∈ U}

Tactic:
set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩

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
z : ↑u := ⟨y, ⋯⟩
⊢ x ∈ {a | ∃ i, (a, g i) ∈ U}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.21
β : Type ?u.25
γ : Type ?u.29
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
⊢ Sort ?u.30

Tactic:
by haveI := ua1; haveI := ub1; exact UniformContinuous fun p : α × β => f p.1 p.2

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 : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x ↦ (g x.1, g x.2)) (map (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S))) ≤ 𝓤 γ ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Tactic:
Filter.map_map,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Tactic:
comp_def

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun x ↦ ((fun x ↦ g (f x)) x.1, (fun x ↦ g (f x)) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
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 ∈ 𝓤 α
⊢ ∃ a, closure[inst✝.toTopologicalSpace] (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ :
    ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
      rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
  rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩
  refine ⟨a, mem_of_superset ?_ (closure_mono <| image_mono <| UniformSpace.ball_mono hs a)⟩
  have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
  refine mem_of_superset (ho.mem_nhds <| UniformSpace.mem_ball_symmetry.2 ha) fun y hy => ?_
  refine mem_closure_iff_nhds.2 fun V hV => ?_
  rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩
  exact ⟨e x, hxV, mem_image_of_mem e hxU⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x : α
⊢ x ∈ ⋃ x ∈ A, ball x V → x ∉ ⋃ x ∈ B, ball x V

Tactic:
simp only [mem_iUnion₂]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x : α
⊢ (∃ i, ∃ (_ : i ∈ A), x ∈ ball i V) → ¬∃ i, ∃ (_ : i ∈ B), x ∈ ball i V
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
w✝ : x ∈ s
k : ℕ
⊢ IsOpen[uniformSpace.toTopologicalSpace] (ball x (t k))

Tactic:
exact isOpen_ball x (hto k)

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
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
obtain ⟨n, hn, hnf⟩ := hlf x
  classical
    let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_ofPred_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        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]
      intro i hi
      simp only [Finite.coe_toFinset, mem_ofPred_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
by
  simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuous (S.domRestrict ∘ F) ↔ UniformEquicontinuousOn F S

Tactic:
by
  rw [UniformEquicontinuous, UniformEquicontinuousOn]
  conv in _ ⊓ _ => rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]
  rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ map (⇑e) atTop = atTop

Tactic:
rw [← e.comap_atTop, map_comap_of_surjective e.surjective]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

Tactic:
by simp [← Ici_inter_Iic, inter_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
by
  refine ⟨fun hfg => ?_, ?_⟩
  · obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm ▸ one_mem_one
    have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
    rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
    obtain ⟨a, b, rfl, rfl, h⟩ := h
    refine ⟨a, b, ?_, ?_, h⟩
    · rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
    · rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
  · rintro ⟨a, b, rfl, rfl, h⟩
    rw [pure_mul_pure, h, pure_one]

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 : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ ∃ s ∈ p, EqOn (fun i x ↦ g (F i x)) (fun i x ↦ g (F' i x)) s

Tactic:
refine ⟨s', hs', fun i hi => by grind⟩

Goal state after:
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
x : T
⊢ {γ | γ • x ∈ {x}}.Finite

Tactic:
← singleton_inter_nonempty,

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : SMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
x : T
⊢ {γ | ({γ • x} ∩ {x}).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : ContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : ContinuousMul N
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ p.1 * p.2

Tactic:
apply Continuous.prodMk <;> fun_prop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun x ↦ x✝ * x

Tactic:
apply Continuous.prodMk <;> fun_prop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun x ↦ x * x✝

Tactic:
apply Continuous.prodMk <;> fun_prop

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)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun a ↦ (fun x1 x2 ↦ x1 * x2) a.1 a.2) (map (fun p ↦ (x₀ * p.1, p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)) =
    map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)

Tactic:
Filter.map_map,

Goal state after:
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)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map ((fun a ↦ (fun x1 x2 ↦ x1 * x2) a.1 a.2) ∘ fun p ↦ (x₀ * p.1, p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) =
    map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)
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)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun x ↦ x₀ * x) (map (fun x ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)

Tactic:
Filter.map_map,

Goal state after:
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)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
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
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf : IsProperMap (g ∘ f)
⊢ IsProperMap f

Tactic:
isProperMap_iff_ultrafilter_of_t2

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
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf : IsProperMap (g ∘ f)
⊢ Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 0, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
rcases this with ⟨t, ht, s, hs, h⟩

Goal state after:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t ×ˢ s ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U