mathlib-initiative/mathlib-tactics huggingface dataset:
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 γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ 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))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map (fun x ↦ Prod.fst ∘ x) fun x ↦ Prod.fst ∘ x) (𝓤 (α → β)) ⊓
      comap (Prod.map (fun x ↦ Prod.snd ∘ x) fun x ↦ Prod.snd ∘ x) (𝓤 (α → γ))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ ^ n = ⊥

Tactic:
by
  rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]

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)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) (uniformSpace α (δ i) 𝔖) =
    UniformSpace.comap (fun x ↦ Function.eval i ∘ x) (uniformSpace α (δ i) 𝔖)

Tactic:
rfl

Goal state after:
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✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b

Tactic:
inv_pure,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ pure a⁻¹ = pure b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 = c
⊢ (fun x ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
subst c

Goal state after:
case inl
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hab : a ≤ b
hc : 0 ≤ 0
⊢ (fun x ↦ x * 0) '' Icc a b = Icc (a * 0) (b * 0)
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 γ
⊢ map (fun b_1 ↦ a • b • b_1) f = map ((fun b ↦ a • b) ∘ fun b_1 ↦ b • b_1) f

Tactic:
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(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
a✝ : α
⊢ ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) ((fun f ↦ ⇑f) x✝)) a✝ = x✝ a✝

Tactic:
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(α, β)
inst✝ : DiscreteTopology α
x✝¹ : α → β
x✝ : α
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) x✝¹) x✝ = x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
· right; rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]

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

Goal state before:
pp: case e'_5
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
x✝ : X
⊢ f x✝ = (Setoid.quotientKerEquivOfSurjective ⇑f ⋯) (Quotient.mk' x✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
y : ι
hy : y ∈ s'
⊢ F y = F' y

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ ∀ (i : ι) (x : α), F' i x ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
i : ι
hi : i ∈ s'
⊢ (fun i x ↦ g (F i x)) i = (fun i x ↦ g (F' i x)) i

Tactic:
grind

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

Tactic:
Function.comp_def

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 ↦ (fun x1 x2 ↦ x1 * x2) (x₀ * x.1, x.2 * y₀).1 (x₀ * x.1, x.2 * y₀).2) (𝓝 1 ×ˢ 𝓝 1) =
    map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)
Module: Mathlib.Topology.Maps.Proper.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 : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf : IsProperMap (g ∘ f)
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
isProperMap_iff_ultrafilter

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf :
  Continuous[inst✝³, inst✝¹] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsProperMap f
hg : IsProperMap g
⊢ IsProperMap (Prod.map f g)

Tactic:
isProperMap_iff_ultrafilter

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g) ∧
    ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄, Tendsto (Prod.map f g) (↑𝒰) (𝓝 y) → ∃ x, Prod.map f g x = y ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: ι : 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 : ι), IsProperMap (f i)
⊢ IsProperMap fun x i ↦ f i (x i)

Tactic:
isProperMap_iff_ultrafilter

Goal state after:
ι : 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)) ∧
    ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
      Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i ↦ f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
use V, V1

Goal state after:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulLeft a).symm x✝ = (Homeomorph.mulLeft a⁻¹) x✝

Tactic:
rfl

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulRight a).symm x✝ = (Homeomorph.mulRight a⁻¹) x✝

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsClosed[inst✝²] (Quotient.mk' ⁻¹' {↑1}) ↔ IsClosed[inst✝²] (mk ⁻¹' {↑1})

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsOpen[inst✝²] (Quotient.mk' ⁻¹' {↑1}) ↔ IsOpen[inst✝²] (mk ⁻¹' {↑1})

Tactic:
rfl

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 t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s / t)

Tactic:
rw [← iUnion_div_right_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

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.2 * x.1⁻¹) ∘ Prod.swap) (𝓝 1) = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)

Tactic:
Function.comp_def

Goal state after:
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)
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.1⁻¹ * x.2) ∘ Prod.swap) (𝓝 1) = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
Function.comp_def

Goal state after:
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)
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.2 / x.1) ∘ Prod.swap) (𝓝 1) = comap (fun x ↦ x.1 / x.2) (𝓝 1)

Tactic:
Function.comp_def

Goal state after:
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)
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
by
  simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff]

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
⊢ ∃ V ∈ 𝓝 1, V * K ⊆ U

Tactic:
by
  rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU)
      (image_mono hKU) with
    ⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : op '' K * V ⊆ op '' U⟩
  refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩
  rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff,
    preimage_image_eq _ op_injective] at hV'

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
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun x ↦ g * x) ⁻¹' V

Tactic:
obtain ⟨t, ht⟩ : ∃ t : Finset G, K ⊆ ⋃ x ∈ t, interior ((x * ·) ⁻¹' V) := by
    refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
    obtain ⟨g₀, hg₀⟩ := hV
    refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
    refine preimage_interior_subset_interior_preimage (by fun_prop) ?_
    rwa [mem_preimage, inv_mul_cancel_right]
  exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩

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
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)

Tactic:
rfl

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
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)

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ sInf (upperBounds (range fun a ↦ f (g a))) = sInf (upperBounds (range (f ∘ g)))

pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range fun a ↦ f (g a))

Tactic:
Function.comp_def

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ sInf (upperBounds (range fun a ↦ f (g a))) = sInf (upperBounds (range fun x ↦ f (g x)))

α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range fun a ↦ f (g a))
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
inst✝ : Nonempty ι
g : ι → α
⊢ sSup (range (f ∘ g)) = sSup (range fun i ↦ f (g i))

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ sSup (range (f ∘ g)) = sSup (range fun i ↦ f (g i))

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)

Tactic:
rfl

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
this : U' ×ˢ V' ∈ 𝓝 x₀ ×ˢ 𝓝 y₀
⊢ (∃ t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀, t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1) ⁻¹' W'

Tactic:
grind

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 𝕜
⊢ (𝓝[>] 0)⁻¹ = atTop

Tactic:
by rw [← inv_atTop₀, inv_inv]

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun x ↦ f x⁻¹) atBot l
⊢ f = (fun x ↦ f x⁻¹) ∘ fun x ↦ x⁻¹

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [@IsLeftUniformGroup.uniformity_eq (G := G) us _ _]

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)

Tactic:
rfl

Goal state after: