mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Div α
a b : α
⊢ pure a / pure b = pure (a / b)

Tactic:
simp

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 : α
⊢ (fun x ↦ x * a) '' Iic b = Iic (b * a)

Tactic:
simp

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 : α
⊢ (fun x ↦ x * a) '' Iio b = Iio (b * a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Ici a = Iic a⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Iic a = Ici a⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Ioi a = Iio a⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Iio a = Ioi a⁻¹

Tactic:
simp

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 : α
⊢ Inv.inv '' Icc a b = Icc b⁻¹ a⁻¹

Tactic:
simp

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 : α
⊢ Inv.inv '' Ico a b = Ioc b⁻¹ a⁻¹

Tactic:
simp

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 : α
⊢ Inv.inv '' Ioc a b = Ico b⁻¹ a⁻¹

Tactic:
simp

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 : α
⊢ Inv.inv '' Ioo a b = Ioo b⁻¹ a⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x + a) '' [[b, c]] = [[b + a, c + a]]

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ Neg.neg '' [[a, b]] = [[-a, -b]]

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
b : β
⊢ pure a • pure b = pure (a • b)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : VSub α β
a b : β
⊢ pure a -ᵥ pure b = pure (a -ᵥ b)

Tactic:
simp

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ x + b) '' Ico (a * c) (a * d) = Ico (a * c + b) (a * d + b)

Tactic:
image_add_const_Ico

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ Ico (a * c + b) (a * d + b) = Ico (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
⊢ a ∈ Ici a

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a : α
x✝ : 1 ≠ 0
⊢ Ici a ^ 1 = Ici (a ^ 1)

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
x✝ : { g // FactorsThrough ⇑g ⇑f }
⊢ (fun g ↦ ⟨g.comp f, ⋯⟩) ((fun g ↦ hf.lift ↑g ⋯) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ s ∈ 𝓝 1

Tactic:
simp

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

Goal state before:
pp: case inl.inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure[inst✝²] (0 • ∅) = 0 • closure[inst✝²] ∅

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝⁸ : Monoid M
inst✝⁷ : TopologicalSpace α
inst✝⁶ : MulAction M α
inst✝⁵ : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst✝⁴ : SMul S M
inst✝³ : SMul S α
inst✝² : IsScalarTower S M α
inst✝¹ : SMul S β
f : α →ₑ[id] β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
c : S
hc : IsUnit (c • 1)
x✝ : α
⊢ ((fun x ↦ c • x) ∘ ⇑f) x✝ = (⇑f ∘ fun x ↦ (c • 1) • x) x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_6
N : Type u_7
F : Type u_8
inst✝⁶ : Mul M
inst✝⁵ : Mul N
inst✝⁴ : FunLike F M N
inst✝³ : MulHomClass F M N
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace N
inst✝ : SeparatelyContinuousMul N
f : F
hf : IsInducing ⇑f
m : M
⊢ ∀ {c x : Mᵐᵒᵖ},
    ((⇑opHomeomorph ∘ ⇑f) ∘ ⇑opHomeomorph.symm) (c • x) =
      op (f (unop c)) • ((⇑opHomeomorph ∘ ⇑f) ∘ ⇑opHomeomorph.symm) x

Tactic:
simp

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
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ univ ∈ 𝓝 0 ∧ ∅ * univ ⊆ U

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ IsOpen[inst✝²] {x | m ∈ s}

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
c a : G
⊢ {c * a}ᶜ = ⇑(Homeomorph.mulLeft c) '' {a}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
⊢ Tendsto f (cocompact X) cofinite

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
c a : G
⊢ {a * c}ᶜ = ⇑(Homeomorph.mulRight c) '' {a}ᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
x✝ : ↑s × β
⊢ (fun gx ↦ (gx.1, (↑gx.1)⁻¹ • gx.2)) ((fun gx ↦ (gx.1, ↑gx.1 • gx.2)) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
x✝ : ↑s × β
⊢ (fun gx ↦ (gx.1, ↑gx.1 • gx.2)) ((fun gx ↦ (gx.1, (↑gx.1)⁻¹ • gx.2)) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
⊢ s ⊆ s * {1}

Tactic:
simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst✝²] (K * {1}) = closure[inst✝²] K

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
a : G
⊢ {a⁻¹}ᶜ = ⇑(Homeomorph.inv G) '' {a}ᶜ

Tactic:
simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ closure[inst✝²] (F * {1}) = F

Tactic:
simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : x * g ∈ t
⊢ (fun x1 x2 ↦ x1 * x2) (x * g) g⁻¹ = x

Tactic:
simp

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
x y : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) x = ((MulDistribMulAction.toMonoidEnd H G) h) y → x = y

Tactic:
simp

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

Goal state before:
pp: case l_inv
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
x : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) ((fun x ↦ h⁻¹ • x) x) = x

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case r_inv
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
x : G
⊢ (fun x ↦ h⁻¹ • x) (((MulDistribMulAction.toMonoidEnd H G) h) x) = x

Tactic:
simp

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

Goal state before:
pp: Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ comap (fun x ↦ x.swap.1⁻¹ * x.swap.2) (𝓝 1) = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ Ioi (a * c) = ⇑(Homeomorph.mulRight c) '' Ioi a

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ Iio (a * c) = ⇑(Homeomorph.mulRight c) '' Iio a

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Iio a⁻¹ = ⇑(Homeomorph.inv H) '' Ioi a

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Ioi a⁻¹ = ⇑(Homeomorph.inv H) '' Iio a

Tactic:
simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))

Tactic:
simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))

Tactic:
simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))

Tactic:
simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))

Tactic:
simp

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
⊢ ↑⊥.topologicalClosure = closure[inst✝²] {1}

Tactic:
simp

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
x : G
⊢ 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x

Tactic:
simp

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
x : G
⊢ 𝓝 (x⁻¹⁻¹ * 1) = 𝓝 x

Tactic:
simp

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
x : G
⊢ map (fun x_1 ↦ x * x_1) (𝓝 1) = 𝓝 x

Tactic:
simp

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
x : G
⊢ map (fun x_1 ↦ x_1 * x) (𝓝 1) = 𝓝 x

Tactic:
simp

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

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
x✝ : α × α
⊢ (id x✝).1 = (((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) x✝).1

Tactic:
simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete ↑S
V : Set G
hV : V ∈ 𝓝 1 ∧ V ∩ ↑S = {1}
U : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U⁻¹
hgx : (fun x ↦ g * x) x ∈ U
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x ↦ g * x) x) x⁻¹ = g

Tactic:
simp

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

Goal state before:
pp: case snd
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
x✝ : α × α
⊢ (id x✝).2 = (((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) x✝).2

Tactic:
simp

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

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
x✝ : α × α
⊢ (id x✝).1 = (((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) x✝).1

Tactic:
simp

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

Goal state before:
pp: case snd
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
x✝ : α × α
⊢ (id x✝).2 = (((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) x✝).2

Tactic:
simp

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

Goal state before:
pp: case e_m
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hf : 𝓝 1 = comap (⇑f) (𝓝 1)
x x✝ : G
⊢ (⇑f ∘ fun x_1 ↦ x_1 * x⁻¹) x✝ = ((fun x_1 ↦ x_1 * (f x)⁻¹) ∘ ⇑f) x✝

Tactic:
simp

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x ↦ x * x₀⁻¹) ∘ fun x ↦ x * x₀) (𝓝 1) = 𝓝 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ b ≤ k * b / k

Tactic:
rw [mul_div_assoc, mul_div_cancel₀]

Goal state after:
case hb
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ k ≠ 0
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: 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

Tactic:
simp

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

Goal state before:
pp: 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

Tactic:
simp

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

Goal state before:
pp: 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 (c / a) = ⇑(Homeomorph.divLeft c) '' Ioi a

Tactic:
simp

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

Goal state before:
pp: 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 (c / a) = ⇑(Homeomorph.divLeft c) '' Iio a

Tactic:
simp

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

Goal state before:
pp: 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
⊢ univ ∈ 𝓝 1 ∧ ∅ * univ ⊆ U

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ 1 = 1 * 1⁻¹

Tactic:
simp

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

Goal state before:
pp: G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ IsTopologicalGroup.rightUniformSpace G = u

Tactic:
ext : 1
  rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_mul_inv_nhds_one]

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
x y : G
⊢ 𝓝 (x * y) = map (fun x_1 ↦ x * x_1) (map (fun x ↦ x * y) (𝓝 1 * 𝓝 1))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x : G₀
⊢ (∃ x_1, x_1 ≠ 0 ∧ x_1 = x) ↔ x ∈ {g | g = 0 → False}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x✝ : { g // g ≠ 0 }
⊢ (fun g ↦ ⟨(↑g)⁻¹, ⋯⟩) ((fun g ↦ ⟨(↑g)⁻¹, ⋯⟩) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 ((Homeomorph.mulRight₀ a ha).symm.symm 1) = 𝓝 a

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ 𝓝 1 = 𝓝 ((Homeomorph.inv G).symm 1)

Tactic:
simp

Goal state after:
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)
⊢ IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) ∘ ⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
t : β × β
⊢ ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) t = (⇑e ∘ fun t ↦ t.2 / t.1) t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
⊢ b ∈ Iic b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
⊢ b ∈ Iic b

Tactic:
simp

Goal state after: