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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
⊢ ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ T

Tactic:
obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
⊢ ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ T
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s ↔ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n

Tactic:
refine ⟨?_, ?_⟩
  · rintro ⟨T, hT, T_count, rfl⟩
    rcases Set.eq_empty_or_nonempty T with rfl | hT
    · exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩
    · obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
      exact ⟨f, by simp_all, by simp [hf]⟩
  · rintro ⟨f, hf, rfl⟩
    exact .iInter_of_isOpen hf

Goal state after:
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
h1 : x ∈ v
⊢ ⋂ s, ↑s ⊆ b

Tactic:
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
        from (huv.symm.mono this hau).left_le_of_le_sup_left hab

Goal state after:
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
h1 : x ∈ v
⊢ ⋂ s, ↑s ⊆ v
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ Continuous[inst✝, inst✝¹] ⇑e.symm

Tactic:
rw [e.continuous_symm_iff]
  exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩

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

Goal state before:
pp: α : Type ua
u : UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
u.nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
u : UniformSpace α
a : α
⊢ 𝓝 a = comap (Prod.mk a) UniformSpace.uniformity
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f

Tactic:
rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
⊢ s ∈ f
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
⊢ range u ⊆ K

Tactic:
range_subset_iff

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ ∀ (y : β), u y ∈ K
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i

Tactic:
simp_rw [tendstoUniformlyOn_iff_tendsto, hβ.tendsto_right_iff, eventually_prod_principal_iff]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α

Tactic:
refine ((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_

Goal state after:
α : Type u
inst✝ : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
⊢ ∃ i ∈ 𝓤 α, Prod.map mk mk ⁻¹' Prod.map mk mk '' id i ⊆ id U
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) =
    comap (fun x ↦ (f x.1, f x.2)) (comap (fun x ↦ (g x.1, g x.2)) (𝓤 γ))

Tactic:
comap_comap

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 γ)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α

Tactic:
by rw [← hf.1, ← hg.1, comap_comap]; rfl

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)) =
    comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)

Tactic:
comap_comap

Goal state after:
α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q ↦ (↑q.1, ↑q.2)) ∘ fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (𝓤 α) =
    comap (fun q ↦ (↑q.1, ↑q.2)) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun n ↦ F (u n)) f atTop

Tactic:
by
  simp_rw [← tendstoUniformlyOn_univ]
  exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

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

Goal state before:
pp: case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
x : α
x✝ : x ∈ K
⊢ ball x (V i) ∈ 𝓝 x

Tactic:
exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ UniformContinuous g

Tactic:
by convert! f.symm.uniformContinuous

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 β
s : Set α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst✝²] s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
h : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
v : Set α
hv1 : v ∈ 𝓝[s] x
hv2 : TendstoUniformlyOn G g p v
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u

Tactic:
exact ⟨v, hv1, hv2 u hu⟩

Goal state after:
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 → α
x₀ : X
⊢ EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀

Tactic:
EquicontinuousWithinAt,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔ EquicontinuousAt F x₀
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

Tactic:
comap_comap

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        (fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 (α →ᵤ[𝔖] γ))) =
    𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
comap_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))

Tactic:
exact UniformOnFun.precomp_uniformContinuous h_image₁

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

Goal state before:
pp: M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n : ℕ
⊢ (a ^ Nat.zero) ⤳ (b ^ Nat.zero)

Tactic:
by simp only [pow_zero, specializes_rfl]

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:
continuous_iff_continuousAt

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 : M × M), ContinuousAt (fun p ↦ p.1 * p.2) x
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) (𝓝 y₀) = 𝓝 (x₀ * y₀)

Tactic:
hleft y₀,

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) (map (fun x ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ (f x)⁻¹

Tactic:
by
  have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
  simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ Tendsto (Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) 𝓕 (𝓤 α)

Tactic:
← (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_left,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ Tendsto ((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) 𝓕 (𝓤 α)
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
⊢ U ∈ map (fun p ↦ p.2 * p.1⁻¹) ((comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)).lift' fun s ↦ SetRel.comp s s)

Tactic:
refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)

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
⊢ SetRel.comp ((fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) ((fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) ⊆ (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
⊢ U ∈ map (fun p ↦ p.1⁻¹ * p.2) ((comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)).lift' fun s ↦ SetRel.comp s s)

Tactic:
refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)

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
⊢ SetRel.comp ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' V) ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' V) ⊆ (fun p ↦ p.1⁻¹ * p.2) ⁻¹' U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
⊢ IsClosed[inst✝³] ↑H

Tactic:
apply isClosed_of_spaced_out this

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
⊢ (↑H).Pairwise fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap ((fun p ↦ p.2 * p.1⁻¹) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) =
    comap (fun p ↦ p.1⁻¹ * p.2) (comap (⇑opHomeomorph) (𝓝 1))

Tactic:
comap_comap

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap ((fun p ↦ p.2 * p.1⁻¹) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) = comap (⇑opHomeomorph ∘ fun p ↦ p.1⁻¹ * p.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap ((fun p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) =
    comap (fun p ↦ p.2 * p.1⁻¹) (comap (⇑opHomeomorph) (𝓝 1))

Tactic:
comap_comap

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap ((fun p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) = comap (⇑opHomeomorph ∘ fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)
⊢ comap ((fun p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2)) (comap (⇑(Homeomorph.inv G)) (𝓝 1)) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
comap_comap

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)
⊢ comap (⇑(Homeomorph.inv G) ∘ (fun p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2)) (𝓝 1) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 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 ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

Tactic:
by
  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:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous fun x ↦ (↑x)⁻¹

Tactic:
continuous_iff_continuousAt

Goal state after:
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ ∀ (x : { r // 0 < r }), ContinuousAt (fun x ↦ (↑x)⁻¹) x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hf : Tendsto f l (𝓝 ⊤)
hg : f ≤ᶠ[l] g
⊢ Tendsto g l (𝓝 ⊤)

Tactic:
simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢
  intro x hx
  filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A
⊢ c a = 0

Tactic:
obtain ⟨c, rfl⟩ := h c

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A'
⊢ ((dual f) c) a = 0
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift ((ConcreteCategory.hom (c'.ι.app j)) x) = χ ((Quot.ι F j) x)

Tactic:
dsimp [c']

Goal state after:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift (AddEquiv.ulift.symm (χ ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
⊢ (f '' s).PairwiseDisjoint fun x ↦ Ioo x (z (invFunOn f s x))

Tactic:
rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
⊢ (Disjoint on fun x ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)