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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
union_eq_iUnion,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (⋃ b, bif b then s else t) ↔ TotallyBounded s ∧ TotallyBounded t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded ({a} ∪ s) ↔ TotallyBounded s

Tactic:
totallyBounded_union,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded {a} ∧ TotallyBounded s ↔ TotallyBounded s
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : (x : α) → x ∈ K → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ⊆ U ↑y ⋯

Tactic:
by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds' hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ x ∉ s.preimage t, ∀ᶠ (y : α) in nhds x, y ∉ s.preimage t

Tactic:
SetRel.mem_preimage,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ (x : α), (¬∃ b ∈ t, (x, b) ∈ s) → ∀ᶠ (y : α) in nhds x, ¬∃ b ∈ t, (y, b) ∈ s
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : insert x (range u) ∩ s = insert x (range u) ∩ t
⊢ x ∈ t

Tactic:
Set.ext_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ t
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ Equicontinuous (S.domRestrict ∘ F) ↔ EquicontinuousOn F S

Tactic:
simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ GaloisConnection (fun 𝓐 ↦ map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 ↦ UniformFun.filter α β 𝓕

Tactic:
intro 𝓐 𝓕

Goal state after:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun 𝓐 ↦ map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕 ↔ 𝓐 ≤ (fun 𝓕 ↦ UniformFun.filter α β 𝓕) 𝓕
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
constructor <;> intro H U hU
  · rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
    refine ⟨_, H V hV, fun x hx y hy i => hVU (SetRel.prodMk_mem_comp ?_ (hy i))⟩
    exact SetRel.symm V (hx i)
  · rcases H U hU with ⟨V, hV, hVU⟩
    filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformly (⇑toFun ∘ F) (toFun f) p

Tactic:
rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ (x : α), (toFun f x, (⇑toFun ∘ F) n x) ∈ u
Module: Mathlib.Topology.UniformSpace.Equicontinuity

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

Tactic:
equicontinuousAt_iff_continuousAt,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
⊢ ContinuousAt (⇑ofFun ∘ swap F) x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

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

Tactic:
equicontinuousAt_iff_continuousAt,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ ContinuousAt (⇑ofFun ∘ swap F) x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

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

Tactic:
equicontinuousAt_iff_continuousAt,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ ContinuousAt (⇑ofFun ∘ swap F) x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀

Tactic:
equicontinuousAt_iff_continuousAt,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ ContinuousAt (⇑ofFun ∘ swap F) x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ ContinuousAt (⇑ofFun ∘ swap F) x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀

Tactic:
equicontinuousAt_iff_continuousAt,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ ContinuousAt (⇑ofFun ∘ swap F) x₀ ↔ ContinuousAt (⇑ofFun ∘ swap ((fun x ↦ u ∘ x) ∘ F)) x₀
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ u v, IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

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:
simp [← Ici_inter_Iic, inter_comm]

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 c : α
⊢ (fun x ↦ a / x) ⁻¹' Icc b c = Icc (a / c) (a / b)

Tactic:
simp [← Ici_inter_Iic, inter_comm]

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap (Pi.uniformSpace fun i ↦ α →ᵤ[𝔖] δ i) = uniformSpace α ((i : ι) → δ i) 𝔖

Tactic:
Pi.uniformSpace,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap
      (UniformSpace.ofCoreEq (⨅ i, UniformSpace.comap (Function.eval i) (uniformSpace α (δ i) 𝔖)).toCore
        Pi.topologicalSpace ⋯) =
    uniformSpace α ((i : ι) → δ i) 𝔖
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap (⨅ i, UniformSpace.comap (Function.eval i) (uniformSpace α (δ i) 𝔖)) =
    uniformSpace α ((i : ι) → δ i) 𝔖

Tactic:
Pi.uniformSpace,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap (⨅ i, UniformSpace.comap (Function.eval i) (uniformSpace α (δ i) 𝔖)) =
    uniformSpace α ((i : ι) → δ i) 𝔖
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) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)

Tactic:
rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]

Goal state after:
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
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

Tactic:
rw [← image_subset_iff, image_mul_prod] at 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 ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case left
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun x i ↦ f i (x i)

Tactic:
exact continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)

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

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝² : TopologicalSpace α := ⊥
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
this : DiscreteTopology β
⊢ Tendsto (fun i ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
← cocompact_eq_cofinite

Goal state after:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
this✝² : TopologicalSpace α := ⊥
hf : Tendsto f (cocompact α) (𝓝 0)
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
hg : Tendsto g (cocompact β) (𝓝 0)
this : DiscreteTopology β
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
Module: Mathlib.Topology.Algebra.Monoid

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

Tactic:
simp only [← finprod_subtype_eq_finprod_cond]

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

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
exact uniformity_eq_comap_mul_inv_nhds_one Gᵣ

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
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ 𝓝 (f x) ≤ map (⇑f) (𝓝 x)

Tactic:
← map_mul_left_nhds_one x,

Goal state after:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ 𝓝 (f x) ≤ map (⇑f) (map (fun x_1 ↦ x * x_1) (𝓝 1))
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n

Tactic:
intro n

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n : ℕ
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t ×ˢ s ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
rw [← image_subset_iff, image_mul_prod] at h

Goal state after:
case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)

Tactic:
intro n

Goal state after:
case refine_1
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
n : ℕ
⊢ IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y

Tactic:
← map_mul_left_nhds_one x,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun x_1 ↦ x * x_1) (𝓝 1) * 𝓝 y
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

Tactic:
· fun_prop

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : x ∈ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
h'x : ¬IsTop x
⊢ x ∈ t ∪ {x | IsTop x}

Tactic:
simpa [-sep_and, t, h'x]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)

Tactic:
← neg_pos,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : 0 < -n
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
rw [mem_nhdsGT_iff_exists_Ioo_subset]
  constructor
  · rintro ⟨u, au, as⟩
    rcases exists_between au with ⟨v, hv⟩
    exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
  · rintro ⟨u, au, as⟩
    exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩

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

Goal state before:
pp: case hgf
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, 0 ≤ (abs ∘ fun x ↦ f x * g x) b

pp: case hfh
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun x ↦ f x * g x) b ≤ |C * g b|

Tactic:
· filter_upwards [hf] with x _ using abs_nonneg _

Goal state after:
case hfh
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun x ↦ f x * g x) b ≤ |C * g b|
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_1.ofNat
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x ↦ c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0

Tactic:
| ofNat n =>

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ e.trans f ≈ e'.trans f'

Tactic:
by
  constructor
  · rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]
    exact (he.symm'.eqOn.mono inter_subset_left).image_eq
  · intro x hx
    rw [trans_source] at hx
    simp [Function.comp_apply, PartialEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ e.symm.source

Tactic:
rw [symm_source, t]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Mono f
hN : N.isFinite
⊢ M.isFinite

Tactic:
rw [AddCommGrpCat.mono_iff_injective] at hf
    simp only [prop_isFinite_iff] at hN ⊢
    exact Finite.of_injective _ hf

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ n.toNat • p = n • p

Tactic:
by rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ S = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range

Tactic:
rw [← hom_comp, ofMkLEMk_comp]
          exact (Submodule.range_subtype _).symm

Goal state after: