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

Goal state before:
pp: case hf
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun x ↦ x.1 * x✝.1

pp: case hg
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun x ↦ x.2 * x✝.2

Tactic:
<;>

Goal state after:
case hf
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun x ↦ x.1 * x✝.1

case hg
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun x ↦ x.2 * x✝.2
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: case false
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

pp: case true
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
<;>

Goal state after:
case false
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

case true
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) →
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x) →
    ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) →
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x) →
    ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
set l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β)) with l_def

Goal state after:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) → IsProperMap f

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) → IsProperMap f
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case false
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

pp: case true
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
<;>

Goal state after:
case false
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

case true
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul 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 ↦ f x * b) l (𝓝 (c * b))
x✝ : α
⊢ f x✝ = f x✝ * b * b⁻¹

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 ↦ f x * b) l (𝓝 (c * b))
⊢ c = c * b * b⁻¹

Tactic:
<;>

Goal state after:
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 ↦ f x * b) l (𝓝 (c * b))
x✝ : α
⊢ f x✝ = f x✝ * b * b⁻¹

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 ↦ f x * b) l (𝓝 (c * b))
⊢ c = c * b * b⁻¹
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ s * {a} ∈ 𝓝 a

Tactic:
simpa only [one_mul] using mul_singleton_mem_nhds a h

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

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

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

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)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case false
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

pp: case true
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
<;>

Goal state after:
case false
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

case true
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
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 ↑𝒢
⊢ LeftInverse ⇑((MulDistribMulAction.toMonoidEnd H G) h) fun x ↦ h⁻¹ • x

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 ↑𝒢
⊢ RightInverse ⇑((MulDistribMulAction.toMonoidEnd H G) h) fun x ↦ h⁻¹ • x

Tactic:
<;>

Goal state after:
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 ↑𝒢
⊢ LeftInverse ⇑((MulDistribMulAction.toMonoidEnd H G) h) fun x ↦ h⁻¹ • x

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 ↑𝒢
⊢ RightInverse ⇑((MulDistribMulAction.toMonoidEnd H G) h) fun x ↦ h⁻¹ • x
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
⊢ ∃ U ∈ 𝓝 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
refine ⟨U, hU, hUinv, fun g hgS ↦ ?_⟩

Goal state after:
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
⊢ ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1
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

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

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

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

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

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

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
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

pp: case e'_5
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹

Tactic:
<;>

Goal state after:
case e'_3
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

case e'_5
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

pp: case e'_5
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹

Tactic:
<;>

Goal state after:
case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

case e'_5
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹
Module: Mathlib.Topology.Algebra.Group.Basic

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

pp: case e'_5
G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
⊢ c = (b / c)⁻¹ * b

Tactic:
<;>

Goal state after:
case e'_3
G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
k : α
⊢ f k = (b / f k)⁻¹ * b

case e'_5
G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
⊢ c = (b / c)⁻¹ * b
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ ContinuousAt (⇑f) 1

Tactic:
ContinuousAt,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 (f 1))
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1 * unop p.2

pp: case refine_2
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ unop p.2 * p.1

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1 * unop p.2

case refine_2
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ unop p.2 * p.1
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case false
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

pp: case true
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
<;>

Goal state after:
case false
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

case true
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G
Module: Mathlib.Topology.Algebra.GroupWithZero

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

Tactic:
div_zero

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
ContinuousAt,

Goal state after:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto Inv.inv (𝓝 x) (𝓝 x⁻¹)
Module: Mathlib.Topology.Order.LocalExtr

Goal state before:
pp: case inl
α : 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
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case inr
α : 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
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
<;>

Goal state after:
case inl
α : 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
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

case inr
α : 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
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Topology.Order.LocalExtr

Goal state before:
pp: case inl
α : 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
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f b ≤ f x) x}

pp: case inr
α : 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
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f b ≤ f x) x}

Tactic:
<;>

Goal state after:
case inl
α : 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
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f b ≤ f x) x}

case inr
α : 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
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f b ≤ f x) x}