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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this✝ : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst✝²] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
this : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b

Tactic:
filter_upwards [inter_mem V₁_in V₂_in] using this

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
⊢ IsPreconnected (⋂ Z, ↑Z)

Tactic:
isPreconnected_iff_subset_of_fully_disjoint_closed hs

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
⊢ ∀ (u v : Set X), IsClosed[inst✝²] u → IsClosed[inst✝²] v → ⋂ s, ↑s ⊆ u ∪ v → Disjoint u v → ⋂ s, ↑s ⊆ u ∨ ⋂ s, ↑s ⊆ v
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s

Tactic:
by
  rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsMeagre ∅

Tactic:
by
  rw [IsMeagre, compl_empty]
  exact Filter.univ_mem

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h✝ : connectedComponent a ∩ ⋂ s, ↑s = ∅
h : ∃ u, connectedComponent a ∩ ⋂ i ∈ u, ↑i = ∅
⊢ ∃ U V, IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
obtain ⟨fin_a, ha⟩ := h

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
fin_a : Finset { s // IsClopen s ∧ b ∈ s }
ha : connectedComponent a ∩ ⋂ i ∈ fin_a, ↑i = ∅
⊢ ∃ U V, IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
f : Filter α
⊢ (∀ (i' : ι), p i' → ∃ i ∈ f, id i ×ˢ id i ⊆ s i') ↔ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

Tactic:
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun s ↦ g (ball x s)

Tactic:
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
  simp_rw [ball, Function.comp_def]

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rw [Filter.disjoint_iff]

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y ↦ (f x, f y) ∉ V₀
⊢ (range f).Pairwise fun x y ↦ (x, y) ∉ V₀

Tactic:
by
    rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h
    exact hf (ne_of_apply_ne f h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOn F p s
hss' : s' ⊆ s
⊢ UniformCauchySeqOn F p s'

Tactic:
uniformCauchySeqOn_iff_uniformCauchySeqOnFilter

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
γ : Type u_5
hf : UniformCauchySeqOn F p s
g : γ → α
⊢ UniformCauchySeqOn (fun n ↦ F n ∘ g) p (g ⁻¹' s)

Tactic:
uniformCauchySeqOn_iff_uniformCauchySeqOnFilter

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
γ : Type u_5
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter (fun n ↦ F n ∘ g) p (𝓟 (g ⁻¹' s))
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f

Tactic:
by
  rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_ultrafilter]

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

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

Tactic:
rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
⊢ ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q ↦ (f q.2, F q.1 q.2)) ∘ x) atTop (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
this : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, ball x U
⊢ SeparableSpace α

Tactic:
rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
this : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, ball x U
t : Set α
htc : t.Countable
ht : univ ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ SeparableSpace α
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
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
← equicontinuousWithinAt_univ,

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]

Goal state after:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_3.inl
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₁
⊢ (toFun (f, g).1 (φ₁ y), toFun (f, g).2 (φ₁ y)) ∈ U

Tactic:
exact hfg.1 y

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 α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousAt F x₀
⊢ ContinuousWithinAt f univ x₀

Tactic:
← equicontinuousWithinAt_univ,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ (a • b) • f = a • b • f

Tactic:
by simp only [← Filter.map_smul, map_map, smul_assoc]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : TopologicalSpace δ
f g : C(α, β)
X₁ : Type u_5
X₂ : Type u_6
Y₁ : Type u_7
Y₂ : Type u_8
inst✝³ : TopologicalSpace X₁
inst✝² : TopologicalSpace X₂
inst✝¹ : TopologicalSpace Y₁
inst✝ : TopologicalSpace Y₂
e : X₁ ≃ₜ X₂
e' : Y₁ ≃ₜ Y₂
x✝ : C(X₁, Y₁)
⊢ (fun g ↦ { toFun := ⇑e'.symm, continuous_toFun := ⋯ }.comp (g.comp { toFun := ⇑e, continuous_toFun := ⋯ }))
      ((fun f ↦ { toFun := ⇑e', continuous_toFun := ⋯ }.comp (f.comp { toFun := ⇑e.symm, continuous_toFun := ⋯ })) x✝) =
    x✝

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : TopologicalSpace δ
f g : C(α, β)
X₁ : Type u_5
X₂ : Type u_6
Y₁ : Type u_7
Y₂ : Type u_8
inst✝³ : TopologicalSpace X₁
inst✝² : TopologicalSpace X₂
inst✝¹ : TopologicalSpace Y₁
inst✝ : TopologicalSpace Y₂
e : X₁ ≃ₜ X₂
e' : Y₁ ≃ₜ Y₂
x✝ : C(X₂, Y₂)
⊢ (fun f ↦ { toFun := ⇑e', continuous_toFun := ⋯ }.comp (f.comp { toFun := ⇑e.symm, continuous_toFun := ⋯ }))
      ((fun g ↦ { toFun := ⇑e'.symm, continuous_toFun := ⋯ }.comp (g.comp { toFun := ⇑e, continuous_toFun := ⋯ })) x✝) =
    x✝

Tactic:
by aesop

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (map Prod.fst l ×ˢ 𝓝 0) (𝓝 0)

Tactic:
apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Disjoint (map Prod.fst l) (cocompact M)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
x✝ : α
⊢ f x✝ = b⁻¹ * (b * f x✝)

Tactic:
rw [inv_mul_cancel_left]

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

Goal state before:
pp: case e'_5
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
⊢ c = b⁻¹ * (b * c)

Tactic:
rw [inv_mul_cancel_left]

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
this : ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
⊢ IsOpen[inst✝⁵] (⇑φ ⁻¹' ⇑φ '' U)

Tactic:
by
        exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ map (fun x ↦ x / c) (𝓝[>] a) = 𝓝[>] (a / c)

Tactic:
convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ Ioi (a / c) = ⇑(Homeomorph.divRight c) '' Ioi a
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ map (fun x ↦ x / c) (𝓝[<] a) = 𝓝[<] (a / c)

Tactic:
convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ Iio (a / c) = ⇑(Homeomorph.divRight c) '' Iio a
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ map (fun x ↦ x / c) (𝓝[≠] a) = 𝓝[≠] (a / c)

Tactic:
convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ {a / c}ᶜ = ⇑(Homeomorph.divRight c) '' {a}ᶜ
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) = map (fun x_1 ↦ x * x_1) (𝓝 1) * 𝓝 y

Tactic:
← map_mul_right_nhds_one y,

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ G ≃ᵤ G

Tactic:
have B : @UniformContinuous G G (IsTopologicalGroup.leftUniformSpace G)
      (IsTopologicalGroup.rightUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff_le_comap.2
    rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]
    simp

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
B : UniformContinuous ⇑(Equiv.inv G)
⊢ G ≃ᵤ G
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ closure (↑K)⁻¹

Tactic:
← Set.image_inv_eq_inv

Goal state after:
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ closure ((fun x ↦ x⁻¹) '' ↑K)
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : g y + g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ g x + g x = 0

pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S

pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S

Tactic:
← two_mul,

Goal state after:
case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : 2 * g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ 2 * g x = 0

α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S

α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ (range fun x ↦ a ^ x) = univ

Tactic:
← H

Goal state after:
case inr.inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ (range fun x ↦ a⁻¹ ^ x) = univ
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : ∀ (i : ℕ), True → ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → (x m, x n) ∈ {x | x.2 / x.1 ∈ mk '' u i}
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
simp only [mem_ofPred_eq, forall_true_left, mem_image] at hx

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ x = ↑e'.symm (↑e x)

Tactic:
heq hx,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ x = ↑e'.symm (↑e' x)
Module: Mathlib.Algebra.Category.Grp.EnoughInjectives

Goal state before:
pp: A_ : AddCommGrpCat
⊢ (fun i ↦ { down := i 0 }) = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EnoughInjectives

Goal state before:
pp: A_ : AddCommGrpCat
⊢ ∀ (x y : ↑A_),
    { toFun := fun a i ↦ { down := i a }, map_zero' := ⋯ }.toFun (x + y) =
      { toFun := fun a i ↦ { down := i a }, map_zero' := ⋯ }.toFun x +
        { toFun := fun a i ↦ { down := i a }, map_zero' := ⋯ }.toFun y

Tactic:
by aesop

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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] B
⊢ ∀ (x y : CharacterModule B),
    AddMonoidHom.comp (x + y) f.toAddMonoidHom =
      AddMonoidHom.comp x f.toAddMonoidHom + AddMonoidHom.comp y f.toAddMonoidHom

Tactic:
by aesop

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] (⋃ z, Ioo (a + z • p) (a + p + z • p))

Tactic:
exact isOpen_iUnion fun i => isOpen_Ioo

Goal state after: