awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
s_1 : Set α
x : α
s : Subgroup G
g : G
hg : g ∈ closure[inst] (↑s : Set G)
⊢ g⁻¹ ∈ closure[inst] (↑s : Set G)

Tactic:
simpa only [← Set.mem_inv, inv_closure, inv_coe_set] using hg

Premises used: inv_coe_set, inv_closure, Set.mem_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Subgroup G
⊢ (↑s.topologicalClosure : Set G) = closure[inst] (↑s : Set G)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Subgroup G
⊢ s ≤ s.topologicalClosure

Tactic:
_root_.subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Subgroup G
⊢ IsClosed[inst] (↑s.topologicalClosure : Set G)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Subgroup G
h : s ≤ t
ht : IsClosed[inst] (↑t : Set G)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Subgroup G
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
_root_.closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst, inst_4] (⇑f : (a : G) → H)
hf' : DenseRange.{x, w} (X := H) (α := G) (⇑f : (a : G) → H)
s : Subgroup G
hs : s.topologicalClosure = ⊤
rw :
  ∀ (hs : (↑s.topologicalClosure : Set G) = (↑⊤ : Set G)),
    (↑(Subgroup.map f s).topologicalClosure : Set H) = (↑⊤ : Set H)
⊢ (Subgroup.map f s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst, inst_4] (⇑f : (a : G) → H)
hf' : DenseRange.{x, w} (X := H) (α := G) (⇑f : (a : G) → H)
s : Subgroup G
hs : (↑s.topologicalClosure : Set G) = (↑⊤ : Set G)
simp : ∀ (hs : Dense (↑s : Set G)), Dense (↑(Subgroup.map f s) : Set H)
⊢ (↑(Subgroup.map f s).topologicalClosure : Set H) = (↑⊤ : Set H)

Tactic:
simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢

Premises used: dense_iff_closure_eq, Subgroup.coe_top, Subgroup.topologicalClosure_coe
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst, inst_4] (⇑f : (a : G) → H)
hf' : DenseRange.{x, w} (X := H) (α := G) (⇑f : (a : G) → H)
s : Subgroup G
hs : Dense (↑s : Set G)
⊢ Dense (↑(Subgroup.map f s) : Set H)

Tactic:
hf'.dense_image hf hs

Premises used: setOf, Set.image, DenseRange.dense_image
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst, inst_4] (⇑f : (a : G) → H)
hf' : DenseRange.{x, w} (X := H) (α := G) (⇑f : (a : G) → H)
s : Subgroup G
hs : Dense (↑s : Set G)
⊢ Dense (↑(Subgroup.map f s) : Set H)

Tactic:
exact hf'.dense_image hf hs

Premises used: DenseRange.dense_image
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
apply : MapsTo (fun (h : G) ↦ g * h * g⁻¹) (↑N : Set G) (↑N : Set G)
⊢ g * n * g⁻¹ ∈ N.topologicalClosure

Tactic:
apply map_mem_closure (IsTopologicalGroup.continuous_conj g) hn

Premises used: map_mem_closure, IsTopologicalGroup.continuous_conj
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ MapsTo (fun (h : G) ↦ g * h * g⁻¹) (↑N : Set G) (↑N : Set G)

Tactic:
fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g

Premises used: Set.Mem, inferInstance, Set.MapsTo, Subgroup.Normal.conj_mem
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ MapsTo (fun (h : G) ↦ g * h * g⁻¹) (↑N : Set G) (↑N : Set G)

Tactic:
exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g

Premises used: inferInstance, Subgroup.Normal.conj_mem
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
rw : g * h ∈ connectedComponent g
⊢ Membership.mem (γ := Set G) (connectedComponent 1) (g * h)

Tactic:
rw [connectedComponent_eq hg]

Premises used: connectedComponent_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
a : Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent h) g
⊢ g ∈ connectedComponent (g * h)

Tactic:
apply Continuous.image_connectedComponent_subset (continuous_const_mul g)

Premises used: Continuous.image_connectedComponent_subset, continuous_const_mul
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
a : Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent 1) g
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent h) g

Tactic:
rw [← connectedComponent_eq hh]

Premises used: connectedComponent_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ (fun (x : G) ↦ g * x) 1 = g

Tactic:
simp only [mul_one]

Premises used: mul_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent 1) g

Tactic:
exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ g ∈ connectedComponent (g * h)

Tactic:
have hmul : g ∈ connectedComponent (g * h) := by
    apply Continuous.image_connectedComponent_subset (continuous_const_mul g)
    rw [← connectedComponent_eq hh]
    exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
hmul : g ∈ connectedComponent (g * h)
⊢ g * h ∈ connectedComponent g

Tactic:
simpa [← connectedComponent_eq hmul] using mem_connectedComponent

Premises used: mem_connectedComponent, connectedComponent_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : DivisionMonoid G
inst_2 : ContinuousInv G
g : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
rw : Membership.mem (γ := Set G) (connectedComponent 1⁻¹) g⁻¹
⊢ Membership.mem (γ := Set G) (connectedComponent 1) g⁻¹

Tactic:
rw [← inv_one]

Premises used: inv_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : DivisionMonoid G
inst_2 : ContinuousInv G
g : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
⊢ Membership.mem (γ := Set G) (connectedComponent 1⁻¹) g⁻¹

Tactic:
Continuous.image_connectedComponent_subset continuous_inv _
      ((Set.mem_image _ _ _).mp ⟨g, hg, rfl⟩)

Premises used: Continuous.image_connectedComponent_subset, Set.mem_image, And.intro, Exists.intro, Iff.mp, ContinuousInv.continuous_inv, rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : DivisionMonoid G
inst_2 : ContinuousInv G
g : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
⊢ Membership.mem (γ := Set G) (connectedComponent 1⁻¹) g⁻¹

Tactic:
exact
    Continuous.image_connectedComponent_subset continuous_inv _
      ((Set.mem_image _ _ _).mp ⟨g, hg, rfl⟩)

Premises used: Continuous.image_connectedComponent_subset, Set.mem_image, And.intro, Exists.intro, Iff.mp, ContinuousInv.continuous_inv, rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ (↑(topologicalClosure ⊥) : Set G) = closure[inst] {1}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
⊢ s ∈ 𝓝 (HMul.hMul (α := G × G → G) (β := G × G → G) Prod.fst (fun (x : G × G) ↦ x.2⁻¹) (1, 1))

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
⊢ Membership.mem (γ := Filter (G × G)) (𝓝 (1, 1)) ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ⁻¹' s)

Tactic:
have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) :=
    continuousAt_fst.mul continuousAt_snd.inv (by simpa)
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
this : Membership.mem (γ := Filter (G × G)) (𝓝 (1, 1)) ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ⁻¹' s)
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Tactic:
simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using
    this

Premises used: Filter.mem_prod_self_iff, Set.prod_subset_iff, div_eq_mul_inv, nhds_prod_eq, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
⊢ 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
⊢ 𝓝 (x⁻¹⁻¹ * 1) = 𝓝 x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ map (fun (x_1 : G) ↦ x * x_1) (𝓝 y) = 𝓝 (x * y)

Tactic:
(Homeomorph.mulLeft x).map_nhds_eq y

Premises used: Homeomorph.map_nhds_eq, Homeomorph.mulLeft
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
⊢ map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) = 𝓝 x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ map (fun (x_1 : G) ↦ x_1 * x) (𝓝 y) = 𝓝 (y * x)

Tactic:
(Homeomorph.mulRight x).map_nhds_eq y

Premises used: Homeomorph.mulRight, Homeomorph.map_nhds_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
⊢ map (fun (x_1 : G) ↦ x_1 * x) (𝓝 1) = 𝓝 x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
rw :
  HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
    {y : G | y / x ∈ s i}
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ {y : G | y / x ∈ s i}

Tactic:
rw [← nhds_translation_mul_inv]

Premises used: nhds_translation_mul_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
simp_rw :
  HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
    {y : G | y * x⁻¹ ∈ s i}
⊢ HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
    {y : G | y / x ∈ s i}

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
    {y : G | y * x⁻¹ ∈ s i}

Tactic:
hb.comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
    {y : G | y * x⁻¹ ∈ s i}

Tactic:
exact hb.comap _

Premises used: Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
s : Set G
rw :
  (∀ (i : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) i → ∃ y ∈ s, Membership.mem (γ := Set G) {y : G | y / x ∈ id i} y) ↔
    ∀ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U → ∃ y ∈ s, y / x ∈ U
⊢ x ∈ closure[inst] s ↔ ∀ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U → ∃ y ∈ s, y / x ∈ U

Tactic:
rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]

Premises used: Filter.HasBasis.nhds_of_one, nhds, Filter.basis_sets, OfNat.ofNat, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
M : Type u_1
hom : Type u_2
inst_3 : MulOneClass M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
f : hom
hf : Tendsto.{w, u_1} (α := G) (β := M) (⇑f : (a : G) → M) (𝓝 1) (𝓝 1)
x : G
⊢ ContinuousAt.{w, u_1} (Y := M) (⇑f : (a : G) → M) x

Tactic:
simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
      map_mul, mul_one] using hf.const_mul (f x)

Premises used: ContinuousAt, Filter.tendsto_map'_iff, Filter.Tendsto.const_mul, map_mul, Function.comp_def, mul_one, DFunLike.coe, map_mul_left_nhds_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
M : Type u_1
hom : Type u_2
inst_3 : MulOneClass M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
f : hom
hf : ContinuousAt.{w, u_1} (X := G) (Y := M) (⇑f : (a : G) → M) 1
⊢ Tendsto.{w, u_1} (α := G) (β := M) (⇑f : (a : G) → M) (𝓝 1) (𝓝 1)

Tactic:
simpa using hf.tendsto

Premises used: ContinuousAt.tendsto
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst_3 : CommMonoid M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : IsTopologicalGroup H
f : G →* H →* M
hf : ContinuousAt (Y := M) (fun (x : G × H) ↦ (((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2) (1, 1)
hl : ∀ (x : G), ContinuousAt.{u_1, u_2} (X := H) (Y := M) (⇑((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1
hr : ∀ (y : H), ContinuousAt.{w, u_2} (Y := M) (fun (x : G) ↦ (((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) 1
x_1 : G × H
x : G
y : H
simp :
  ∀
    (hf :
      Tendsto (β := M) (fun (x : G × H) ↦ ((((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2 : M))
        (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
        (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) 1) : Filter M)),
    Tendsto (β := M)
      (fun (x_2 : G × H) ↦
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
            ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) y : M) *
          HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) x_2.2 : M)
            ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) x_2.2 : M))
      (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
      (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) : Filter M)
⊢ ContinuousAt (Y := M) (fun (x : G × H) ↦ (((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2) (x, y)

Tactic:
simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
    prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *

Premises used: ContinuousAt, Filter.tendsto_map'_iff, map_mul, Function.comp_def, nhds_prod_eq, Filter.prod_map_map_eq, map_mul_left_nhds_one, MonoidHom.mul_apply
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst_3 : CommMonoid M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : IsTopologicalGroup H
f : G →* H →* M
hl :
  ∀ (x : G),
    Tendsto.{u_1, u_2} (α := H) (β := M) ((⇑((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) : (a : H) → M) (𝓝 1)
      (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1) : Filter M)
hr :
  ∀ (y : H),
    Tendsto.{w, u_2} (β := M) (fun (x : G) ↦ ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)) (𝓝 1)
      (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) y) : Filter M)
x_1 : G × H
x : G
y : H
hf :
  Tendsto (β := M) (fun (x : G × H) ↦ ((((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) 1) : Filter M)
⊢ Tendsto (β := M)
    (fun (x_2 : G × H) ↦
      HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) y : M) *
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) x_2.2 : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) x_2.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) : Filter M)

Tactic:
((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.mono_right, Filter.Tendsto.comp, le_of_eq, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst_3 : CommMonoid M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : IsTopologicalGroup H
f : G →* H →* M
hl :
  ∀ (x : G),
    Tendsto.{u_1, u_2} (α := H) (β := M) ((⇑((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) : (a : H) → M) (𝓝 1)
      (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1) : Filter M)
hr :
  ∀ (y : H),
    Tendsto.{w, u_2} (β := M) (fun (x : G) ↦ ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)) (𝓝 1)
      (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) y) : Filter M)
x_1 : G × H
x : G
y : H
hf :
  Tendsto (β := M) (fun (x : G × H) ↦ ((((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) 1) : Filter M)
refine :
  𝓝
      (HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
          (((f : (a : G) → H →* M) 1 : (a : H) → M) y : M) *
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1 : M)
          (((f : (a : G) → H →* M) 1 : (a : H) → M) 1 : M)) =
    𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y)
⊢ Tendsto (β := M)
    (fun (x_2 : G × H) ↦
      HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) y : M) *
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) x_2.2 : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) x_2.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) : Filter M)

Tactic:
refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.mono_right, Filter.Tendsto.comp, le_of_eq, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst_3 : CommMonoid M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : IsTopologicalGroup H
f : G →* H →* M
hl :
  ∀ (x : G),
    Tendsto.{u_1, u_2} (α := H) (β := M) ((⇑((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) : (a : H) → M) (𝓝 1)
      (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1) : Filter M)
hr :
  ∀ (y : H),
    Tendsto.{w, u_2} (β := M) (fun (x : G) ↦ ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)) (𝓝 1)
      (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) y) : Filter M)
x_1 : G × H
x : G
y : H
hf :
  Tendsto (β := M) (fun (x : G × H) ↦ ((((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) 1) : Filter M)
⊢ 𝓝
      (HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
          (((f : (a : G) → H →* M) 1 : (a : H) → M) y : M) *
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1 : M)
          (((f : (a : G) → H →* M) 1 : (a : H) → M) 1 : M)) =
    𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y)

Tactic:
simp only [map_one, mul_one, MonoidHom.one_apply]

Premises used: map_one, MonoidHom.one_apply, mul_one