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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : Tendsto g l (𝓝 y)
hl : ∀ (x : X), f x ⤳ g x
⊢ Tendsto f l (𝓝 y)

Tactic:
by
  simp_all only [specializes_iff_forall_open, tendsto_nhds]
  refine fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_
  exact mem_preimage.2 (hl x s ho (mem_preimage.1 hx))

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : x ⤳ y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ f x ⤳ f y

Tactic:
specializes_iff_pure

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ pure (f x) ≤ 𝓝 (f y)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact univ

Tactic:
rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a

Tactic:
rwa [ite_inter_of_inter_eq _ H]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ IsClosed[inst✝] s

Tactic:
rw [← closure_eq_iff_isClosed, eq_comm]
  exact subset_closure.antisymm (H.2 H.1.closure subset_closure)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s

Tactic:
use t \ (s \ {x})

Goal state after:
case h
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsOpen[inst✝¹] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ {x}ᶜ ∈ codiscreteWithin s

Tactic:
by
  rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
  intro z hz
  use univ \ {x}
  exact ⟨nhdsNE_of_nhdsNE_sdiff_finite univ_mem Finite.of_subsingleton, by aesop⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜᶜ)) ↔ IsClosed[inst✝] S ∧ IsDiscrete S

Tactic:
compl_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)) ↔ IsClosed[inst✝] S ∧ IsDiscrete S
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case pos
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
rcases hTd with ⟨t, htT, htd⟩

Goal state after:
case pos
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
t : TopologicalSpace X
htT : t ∈ T
htd : Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ∪ t)

Tactic:
rcases H with ⟨x, hxs, hxt⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ ∀ (x : α × β), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
rintro ⟨x, y⟩ U hU

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
x : α
y : β
U : Set (α × β)
hU : U ∈ 𝓝 (x, y)
⊢ ∃ V ∈ 𝓝 (x, y), IsPreconnected V ∧ V ⊆ U
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)}
i : ι
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
by_cases hi : i ∈ K

Goal state after:
case pos
ι : 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 : ι
hi : i ∈ K
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)

case neg
ι : 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 : ι
hi : i ∉ K
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ ∀ (x : { x // x ∈ s }), ∀ᶠ (y : { x // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x

pp: case h'
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ IsTrans { x // x ∈ s } Q

Tactic:
· rintro ⟨x, hx⟩
    have Z := h x hx
    rwa [nhdsWithin_eq_map_subtype_coe] at Z

Goal state after:
case h'
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ IsTrans { x // x ∈ s } Q
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ ((a ∪ b) ∩ a).Nonempty

Tactic:
union_inter_cancel_left

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ a.Nonempty
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
⊢ IsOpenMap ⇑(map f)

Tactic:
rintro _ ⟨U, hU, rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
⊢ IsOpen[instTopologicalSpaceUnits] (⇑(map f) '' ⇑(embedProduct M) ⁻¹' U)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mk
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace =
    u₂.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ } =
    u₂

Tactic:
cases u₂

Goal state after:
case mk.mk
α : Type ua
toTopologicalSpace✝¹ : TopologicalSpace α
uniformity✝¹ : Filter (α × α)
symm✝¹ : Tendsto Prod.swap uniformity✝¹ uniformity✝¹
comp✝¹ : (uniformity✝¹.lift' fun s ↦ s ○ s) ≤ uniformity✝¹
nhds_eq_comap_uniformity✝¹ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝¹
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f

Tactic:
delta UniformContinuous
  rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
⊢ (map f (𝓟 s)).TotallyBounded ↔ (𝓟 s).TotallyBounded

Tactic:
totallyBounded_map_iff hf

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

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ (∃ x_1 ∈ 𝓝 x, x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1

Tactic:
← disjoint_iff_inter_eq_empty,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ (∃ x_1 ∈ 𝓝 x, Disjoint x_1 (mulSupport f)) ↔ f =ᶠ[𝓝 x] 1
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ (ball x U ∩ ⋃ n, ⋃ x, range (o n x)).Nonempty

Tactic:
refine ⟨o n ⟨y, hy⟩ ⟨x, hyx, hx⟩, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ o n ⟨y, hy⟩ ⋯ ∈ ball x U

case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ o n ⟨y, hy⟩ ⋯ ∈ ⋃ n, ⋃ x, range (o n x)
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 : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p s
hG : TendstoLocallyUniformlyOn G g p s
⊢ TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ s ∈ map₂ m f (map₂ n g h)

Tactic:
refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩

Goal state after:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun f ↦ (u f x₀, u f x)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U

Tactic:
refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prodMk ?_).trans (preimage_mono hVU)

Goal state after:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun f ↦ (u f x₀, u f x)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun f ↦ u f x
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 : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (Prod.map (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)

Tactic:
rw [← uniformity_comap] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ[𝔖] γ) = 𝓤 (α →ᵤ[𝔖] γ)
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]

Goal state after:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] {f | ∀ (x y : M₁), f (x * y) = f x * f y}

Tactic:
simp only [ofPred_forall]

Goal state after:
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)

Tactic:
by
  rw [mul_singleton]
  exact smul_mem_nhds_smul (op a) h

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

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

Tactic:
simp only [ofPred_forall]

Goal state after:
G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] (⋂ i, {x | x i⁻¹ = (x i)⁻¹})
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
⊢ Tendsto (g * x * g⁻¹) l (𝓝 1)

Tactic:
have : Tendsto (fun i ↦ (g i, x i)) l (comap Prod.snd (𝓝 1)) := by
    rwa [tendsto_comap_iff]
  -- `exact` works but is quite slow...
  convert! tendsto_conj_nhds_one.comp this

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
apply Finite.of_preimage _ (equivOp S).surjective

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
⊢ (⇑S.equivOp ⁻¹' {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}).Finite
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
⊢ SetRel.comp ((fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) ((fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) ⊆ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U

Tactic:
rintro ⟨x, y⟩ ⟨z, hz₁, hz₂⟩

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : (x, z) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
hz₂ : (z, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
⊢ (x, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
⊢ SetRel.comp ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' V) ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' V) ⊆ (fun p ↦ p.1⁻¹ * p.2) ⁻¹' U

Tactic:
rintro ⟨x, y⟩ ⟨z, hz₁, hz₂⟩

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : (x, z) ∈ (fun p ↦ p.1⁻¹ * p.2) ⁻¹' V
hz₂ : (z, y) ∈ (fun p ↦ p.1⁻¹ * p.2) ⁻¹' V
⊢ (x, y) ∈ (fun p ↦ p.1⁻¹ * p.2) ⁻¹' U
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
n : ℕ
a : A
⊢ (f ^ n) a = f a ^ n

Tactic:
induction n

Goal state after:
case zero
A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
⊢ (f ^ 0) a = f a ^ 0

case succ
A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n✝ : ℕ
a✝ : (f ^ n✝) a = f a ^ n✝
⊢ (f ^ (n✝ + 1)) a = f a ^ (n✝ + 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Group G
u : UniformSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]
  exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
      (h u hu x)⟩

Goal state after: