awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.1⁻¹ * x.2 ∈ U i}

Tactic:
h.comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.1⁻¹ * x.2 ∈ U i}

Tactic:
exact h.comap _

Premises used: Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
rw :
  HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.1 / x.2) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.1 / x.2 ∈ U i}
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ {x : α × α | x.1 / x.2 ∈ U i}

Tactic:
rw [uniformity_eq_comap_nhds_one_swapped]

Premises used: uniformity_eq_comap_nhds_one_swapped
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.1 / x.2) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.1 / x.2 ∈ U i}

Tactic:
h.comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.1 / x.2) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.1 / x.2 ∈ U i}

Tactic:
exact h.comap _

Premises used: Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
rw :
  HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.2⁻¹ * x.1) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.2⁻¹ * x.1 ∈ U i}
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ {x : α × α | x.2⁻¹ * x.1 ∈ U i}

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]

Premises used: uniformity_eq_comap_inv_mul_nhds_one_swapped
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.2⁻¹ * x.1) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.2⁻¹ * x.1 ∈ U i}

Tactic:
h.comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.2⁻¹ * x.1) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.2⁻¹ * x.1 ∈ U i}

Tactic:
exact h.comap _

Premises used: Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
h₁ :
  ∀ (x : α × α),
    Eq.{u_2 + 1} (α := β)
      (((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2)) x : β)
      ((f : (a : α) → β) (x.2 / x.1) : β)
⊢ Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
x : α × α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2)) x : β)
    ((f : (a : α) → β) (x.2 / x.1) : β)

Tactic:
simp only [Function.comp_apply, map_div]

Premises used: Function.comp_apply, map_div
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
⊢ Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)

Tactic:
have :
    ((fun x : β × β => x.2 / x.1) ∘ fun x : α × α => (f x.1, f x.2)) = fun x : α × α =>
      f (x.2 / x.1) := by ext; simp only [Function.comp_apply, map_div]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
this :
  Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)
rw :
  Tendsto.{u_1, u_2} (β := β) (fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1))
    (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β,
    tendsto_comap_iff, this]

Premises used: UniformContinuous, Filter.tendsto_comap_iff, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
this :
  Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1))
    (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)

Tactic:
Tendsto.comp h tendsto_comap

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
this :
  Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1))
    (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)

Tactic:
exact Tendsto.comp h tendsto_comap

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
hf : ContinuousAt.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β) 1
⊢ Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)

Tactic:
simpa using hf.tendsto

Premises used: ContinuousAt.tendsto
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
f : α →* β
hf : ContinuousAt.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β) 1
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
_root_.uniformContinuous_of_continuousAt_one f hf

Premises used: uniformContinuous_of_continuousAt_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)

Tactic:
⟨fun hf => ?_, fun hf => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
refine_1 :
  ∀ (hf : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)),
    IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
refine_2 :
  ∀ (hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)),
    UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)

Tactic:
refine ⟨fun hf => ?_, fun hf => ?_⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)

Tactic:
apply (isOpen_discrete ({1} : Set β)).preimage hf.continuous

Premises used: UniformContinuous.continuous, isOpen_discrete, Singleton.singleton, OfNat.ofNat, IsOpen.preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
refine_2 : ContinuousAt.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β) 1
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
apply uniformContinuous_of_continuousAt_one

Premises used: uniformContinuous_of_continuousAt_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
refine_2 : ∀ᶠ (x : α) in 𝓝 1, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) (1 : β)
⊢ ContinuousAt.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β) 1

Tactic:
rw [ContinuousAt, nhds_discrete β, map_one, tendsto_pure]

Premises used: ContinuousAt, Filter.tendsto_pure, map_one, nhds_discrete
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
⊢ ∀ᶠ (x : α) in 𝓝 1, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) (1 : β)

Tactic:
hf.mem_nhds (map_one f)

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, map_one, IsOpen.mem_nhds, Set.singleton
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
⊢ ∀ᶠ (x : α) in 𝓝 1, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) (1 : β)

Tactic:
exact hf.mem_nhds (map_one f)

Premises used: map_one, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Continuous[inst.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑f : (a : α) → β)
this :
  Tendsto.{u_1, u_2} (α := α) (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 1) (𝓝 ((f : (a : α) → β) 1) : Filter β)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)),
    Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
⊢ Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)

Tactic:
rwa [map_one] at this

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
Hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike Hom α β
inst_7 : MonoidHomClass Hom α β
f : Hom
h : IsInducing.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ comap (fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2)) (𝓤 β) = 𝓤 α

Tactic:
simp [uniformity_eq_comap_nhds_one, comap_comap, Function.comp_def, h.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, Function.comp_def, Filter.comap_comap, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Tendsto (β := G) (fun (p : G × G) ↦ (p.2 * p.1⁻¹)⁻¹) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) (𝓝 1⁻¹)
⊢ Tendsto.{u_1, u_1} (α := G × G) Prod.swap (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
    (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))

Tactic:
simpa [tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
rcases :
  ∀ (V : Set G) (V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V) (V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U),
    Membership.mem (γ := Filter G)
      (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
        (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
          SetRel.comp s s))
      U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U

Tactic:
rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩

Premises used: exists_nhds_one_split
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U

Tactic:
mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)

Premises used: Iff.mpr, Filter.mem_lift', Filter.preimage_mem_comap, Filter.mem_map, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
refine :
  Subset (α := Set (G × G))
    (SetRel.comp (β := G) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V))
    ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' U)
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U

Tactic:
refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)

Premises used: Iff.mpr, Filter.mem_lift', Filter.preimage_mem_comap, Filter.mem_map, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : Membership.mem (γ := SetRel G G) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) (x, z)
hz₂ : Membership.mem (γ := SetRel G G) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) (z, y)
⊢ Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' U) (x, y)

Tactic:
simpa using V_mul _ hz₂ _ hz₁
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : G
⊢ 𝓝 x = comap (Prod.mk x) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))

Tactic:
simp only [comap_comap, Function.comp_def, nhds_translation_mul_inv]

Premises used: nhds_translation_mul_inv, Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ 𝓤 G = comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
rfl

Premises used: uniformity, rfl, Filter.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Tendsto (β := G) (fun (p : G × G) ↦ (p.1⁻¹ * p.2)⁻¹) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) (𝓝 1⁻¹)
⊢ Tendsto.{u_1, u_1} (α := G × G) Prod.swap (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))
    (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))

Tactic:
simpa [tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
rcases :
  ∀ (V : Set G) (V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V) (V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U),
    Membership.mem (γ := Filter G)
      (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
        (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
          SetRel.comp s s))
      U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U

Tactic:
rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩

Premises used: exists_nhds_one_split
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U

Tactic:
mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)

Premises used: Iff.mpr, Filter.mem_lift', Filter.preimage_mem_comap, Filter.mem_map, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
refine :
  Subset (α := Set (G × G))
    (SetRel.comp (β := G) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' V) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' V))
    ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' U)
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U

Tactic:
refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)

Premises used: Iff.mpr, Filter.mem_lift', Filter.preimage_mem_comap, Filter.mem_map, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : Membership.mem (γ := SetRel G G) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' V) (x, z)
hz₂ : Membership.mem (γ := SetRel G G) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' V) (z, y)
⊢ Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' U) (x, y)

Tactic:
simpa using V_mul _ hz₁ _ hz₂
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : G
⊢ 𝓝 x = comap (Prod.mk x) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))

Tactic:
simp only [comap_comap, Function.comp_def, nhds_translation_inv_mul]

Premises used: Function.comp_def, Filter.comap_comap, nhds_translation_inv_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ 𝓤 G = comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)

Tactic:
rfl

Premises used: uniformity, rfl, Filter.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
uniformContinuous_div : UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2
⊢ IsUniformGroup G

Tactic:
constructor