mathlib-initiative/mathlib-tactics huggingface dataset:
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
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

Tactic:
constructor

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

Tactic:
constructor

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

case right
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
⊢ ∀ ⦃𝒰 : 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 : ι),
    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

Tactic:
constructor

Goal state after:
case left
ι : 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)

case right
ι : 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
⊢ ∀ ⦃𝒰 : 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.Maps.Proper.Basic

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

Tactic:
constructor

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: X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y : X
⊢ ContinuousMap.mulRight (x * y) = (ContinuousMap.mulRight y).comp (ContinuousMap.mulRight x)

Tactic:
ext

Goal state after:
X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y a✝ : X
⊢ (ContinuousMap.mulRight (x * y)) a✝ = ((ContinuousMap.mulRight y).comp (ContinuousMap.mulRight x)) a✝
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
ext

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulLeft a).symm x✝ = (Homeomorph.mulLeft a⁻¹) x✝
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y : X
⊢ ContinuousMap.mulLeft (x * y) = (ContinuousMap.mulLeft x).comp (ContinuousMap.mulLeft y)

Tactic:
ext

Goal state after:
X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y a✝ : X
⊢ (ContinuousMap.mulLeft (x * y)) a✝ = ((ContinuousMap.mulLeft x).comp (ContinuousMap.mulLeft y)) a✝
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
ext

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulRight a).symm x✝ = (Homeomorph.mulRight a⁻¹) x✝
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ ((Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})) ↔
    CompactSpace X

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ ((Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})) →
    CompactSpace X

case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ CompactSpace X →
    (Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})
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
⊢ DiscreteTopology (G ⧸ N) ↔ IsOpen[inst✝²] (mk ⁻¹' {↑1})

Tactic:
MulAction.IsPretransitive.discreteTopology_iff G (mk 1),

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsOpen[instTopologicalSpace N] {↑1} ↔ IsOpen[inst✝²] (mk ⁻¹' {↑1})
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
ht : IsClosed[inst✝²] t
hs : IsCompact s
⊢ IsClosed[inst✝²] (t * s)

Tactic:
rw [← image_op_smul]
  exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)

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
h : tᶜ * closure[inst✝²] {1} = tᶜ
⊢ t * closure[inst✝²] {1} = t

Tactic:
by simpa using compl_mul_closure_one_eq h

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

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

Tactic:
ext

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: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ id = (fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2

Tactic:
ext

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.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
⊢ conj ∘ ⇑φ = dr

Tactic:
ext

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
x✝ : β × β
⊢ (conj ∘ ⇑φ) x✝ = dr x✝
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 : G
⊢ (⇑f ∘ fun x_1 ↦ x_1 * x⁻¹) = (fun x_1 ↦ x_1 * (f x)⁻¹) ∘ ⇑f

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
⊢ snd ∘ ⇑φ = dl

Tactic:
ext

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
x✝ : β × β
⊢ (snd ∘ ⇑φ) x✝ = dl x✝
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
x : A
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U ↔ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U

Tactic:
constructor

Goal state after:
case mp
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
x : A
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U → x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U

case mpr
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
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' ⇑φ '' U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
⊢ φ = g * ψ * g⁻¹

Tactic:
ext

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
x✝ : (β × β) × β × β
⊢ φ x✝ = (g * ψ * g⁻¹) x✝
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)
hconj : ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀✝ x₀ : G
⊢ ((fun x ↦ x₀ * x * x₀⁻¹) ∘ fun x ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) = id

Tactic:
ext

Goal state after:
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)
hconj : ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀✝ x₀ x✝ : G
⊢ ((fun x ↦ x₀ * x * x₀⁻¹) ∘ fun x ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) x✝ = id x✝
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i ↦ {x | x.2 / x.1 ∈ U i}

Tactic:
by
  rw [uniformity_eq_comap_nhds_one]
  exact h.comap _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
⊢ ((fun x ↦ x.2 / x.1) ∘ fun x ↦ (f x.1, f x.2)) = fun x ↦ f (x.2 / x.1)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
x✝ : α × α
⊢ ((fun x ↦ x.2 / x.1) ∘ fun x ↦ (f x.1, f x.2)) x✝ = f (x✝.2 / x✝.1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ IsUniformGroup G

Tactic:
constructor

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformContinuous fun p ↦ p.1 / p.2
Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]
    rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]

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

Goal state before:
pp: α : 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
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U : Set (β × β)
V : Set (δ × δ)
V_in : ∃ t ∈ comap (⇑f) (𝓝 y₀), t ×ˢ t ⊆ V
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U → y ∈ V → (fun p ↦ (φ p.1) p.2) ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈ W
U₁ : Set β
U₁_in : U₁ ∈ comap (⇑e) (𝓝 x₀)
HU₁ : U₁ ×ˢ U₁ ⊆ U
⊢ ∃ U₁ ∈ comap (⇑e) (𝓝 x₀),
    ∃ V₁ ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W

Tactic:
rcases V_in with ⟨V₁, V₁_in, HV₁⟩

Goal state after:
α : 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
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U : Set (β × β)
V : Set (δ × δ)
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U → y ∈ V → (fun p ↦ (φ p.1) p.2) ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈ W
U₁ : Set β
U₁_in : U₁ ∈ comap (⇑e) (𝓝 x₀)
HU₁ : U₁ ×ˢ U₁ ⊆ U
V₁ : Set δ
V₁_in : V₁ ∈ comap (⇑f) (𝓝 y₀)
HV₁ : V₁ ×ˢ V₁ ⊆ V
⊢ ∃ U₁ ∈ comap (⇑e) (𝓝 x₀),
    ∃ V₁ ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : 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₀ : γ
⊢ Cauchy (map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))))

Tactic:
constructor

Goal state after:
case left
α : 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₀ : γ
⊢ (map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀)))).NeBot

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₀ : γ
⊢ map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ≤
    𝓤 G
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, ¬(x' x < a x ∧ a x < y' x)
⊢ ∃ x, (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True

Tactic:
rcases ha' with ⟨w, hw⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
⊢ ∃ x, (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True