awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
rw rw₁ :
  Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
⊢ Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (x₀, y₀)))
    (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
unfold :
  Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))

Tactic:
unfold uncurry

Premises used: Function.uncurry
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
rw :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (𝓝 y₀)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₁ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (β := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1))
        (map (fun (x : M) ↦ x * y₀) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₂ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (map (fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₃ :
  Eq (α := Filter M)
    (map ((fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) ∘ fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀))
      (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₄ rw₅ :
  Eq (α := Filter M)
    (map (fun (x : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) (x₀ * x.1, x.2 * y₀).1 (x₀ * x.1, x.2 * y₀).2)
      (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))

Tactic:
rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]

Premises used: Filter.map_map, Function.comp_def, Filter.prod_map_map_eq
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
rw :
  Eq (α := Filter M)
    (map (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
      (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
rw₁ rw₂ :
  Eq (α := Filter M)
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
⊢ Eq (α := Filter M)
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))

Tactic:
rw [key, ← Filter.map_map]

Premises used: Filter.map_map
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
⊢ LE.le (α := Filter M)
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1))

Tactic:
map_mono hmul

Premises used: Filter.map_mono
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₁ : map (fun (x : M) ↦ x₀ * x) (𝓝 y₀) = 𝓝 (x₀ * y₀)
rw₂ : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₃ : map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
rw₄ : map (fun (x : M) ↦ x₀ * y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
rw₅ rw₆ : 𝓝 (x₀ * y₀) = 𝓝 (x₀ * y₀)
⊢ map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)

Tactic:
rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]

Premises used: Filter.map_map
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
map :
  Eq (α := Filter M) (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (x₀, y₀)))
    (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
map₁ :
  Eq (α := Filter M) (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (Filter.map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
map₂ :
  Eq (α := Filter M)
    (Filter.map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (Filter.map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
map₃ : Filter.map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)

Tactic:
calc
      map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by
        rw [nhds_prod_eq]
      _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) := by
        unfold uncurry
        rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
      _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by
        rw [key, ← Filter.map_map]
      _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := map_mono hmul
      _ = 𝓝 (x₀ * y₀) := by
        rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]

Premises used: Filter.map_mono, HMul.hMul, SProd.sprod, Filter.map, Function.comp, nhds, Prod.mk, Prod.fst, Function.uncurry, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : CommMonoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
apply : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
⊢ ContinuousMul M

Tactic:
apply ContinuousMul.of_nhds_one hmul hleft

Premises used: ContinuousMul.of_nhds_one
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u
inst : CommMonoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
x₀ : M
simp_rw : 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
⊢ 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)

Tactic:
simp_rw [mul_comm, hleft x₀]

Premises used: mul_comm
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : One M₁
inst_3 : One M₂
⊢ IsClosed[Pi.topologicalSpace] {f : M₁ → M₂ | f 1 = 1}

Tactic:
isClosed_eq (continuous_apply 1) continuous_const

Premises used: continuous_const, isClosed_eq
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : Mul M₁
inst_3 : Mul M₂
inst_4 : ContinuousMul M₂
simp : IsClosed[Pi.topologicalSpace] (⋂ (i : M₁), ⋂ (i_1 : M₁), {x : M₁ → M₂ | x (i * i_1) = x i * x i_1})
⊢ IsClosed[Pi.topologicalSpace] {f : M₁ → M₂ | ∀ (x y : M₁), f (x * y) = f x * f y}

Tactic:
simp only [setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : Mul M₁
inst_3 : Mul M₂
inst_4 : ContinuousMul M₂
x y : M₁
⊢ Continuous[Pi.topologicalSpace, inst] fun (x_1 : M₁ → M₂) ↦ x_1 x * x_1 y

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : Mul M₁
inst_3 : Mul M₂
inst_4 : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : M₁), ⋂ (i_1 : M₁), {x : M₁ → M₂ | x (i * i_1) = x i * x i_1})

Tactic:
exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦
    isClosed_eq (continuous_apply _) (by fun_prop)

Premises used: isClosed_eq, continuous_apply, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : Mul M₁
inst_3 : Mul M₂
inst_4 : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] (range (ι := M₁ →ₙ* M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))

Tactic:
isClosed_of_closure_subset fun f hf => ⟨mulHomOfMemClosureRangeCoe f hf, rfl⟩

Premises used: Exists.intro, mulHomOfMemClosureRangeCoe, isClosed_of_closure_subset, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : MulOneClass M₁
inst_3 : MulOneClass M₂
inst_4 : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] (Set.range (ι := M₁ →* M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))

Tactic:
isClosed_of_closure_subset fun f hf => ⟨monoidHomOfMemClosureRangeCoe f hf, rfl⟩

Premises used: monoidHomOfMemClosureRangeCoe, Exists.intro, isClosed_of_closure_subset, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
N : Type u_7
F : Type u_8
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
inst_4 : TopologicalSpace M
inst_5 : TopologicalSpace N
inst_6 : ContinuousMul N
f : F
hf : IsInducing.{u_6, u_7} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ ContinuousMul M

Tactic:
⟨(hf.continuousSMul hf.continuous (map_mul f _ _)).1⟩

Premises used: ContinuousMul.mk, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
N : Type u_7
F : Type u_8
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
inst_4 : TopologicalSpace N
inst_5 : ContinuousMul N
f : F
⊢ ContinuousMul M

Tactic:
letI := induced f ‹_›
  IsInducing.continuousMul f ⟨rfl⟩

Premises used: Topology.IsInducing.continuousMul, Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : ContinuousMul M
S : Subsemigroup M
⊢ ContinuousMul.{u_3} ↥S

Tactic:
IsInducing.continuousMul ({ toFun := (↑), map_mul' := fun _ _ => rfl } : MulHom S M) ⟨rfl⟩

Premises used: Topology.IsInducing.continuousMul, MulHom.mk, Topology.IsInducing.mk, Subtype.val, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
S : Submonoid M
⊢ ContinuousMul.{u_3} ↥S

Tactic:
S.toSubsemigroup.continuousMul

Premises used: Set.Mem, Submonoid.toSubsemigroup, Subsemigroup.continuousMul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
N : Type u_7
F : Type u_8
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
inst_4 : TopologicalSpace M
inst_5 : TopologicalSpace N
inst_6 : SeparatelyContinuousMul N
f : F
hf : IsInducing.{u_6, u_7} (X := M) (Y := N) (⇑f : (a : M) → N)
m : M
⊢ ∀ {c x : Mᵐᵒᵖ},
    Function.comp (β := M) (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ) (⇑f : (a : M) → N))
        (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M) (c • x) =
      HSMul.hSMul (α := Nᵐᵒᵖ) (β := Nᵐᵒᵖ) ((fun (x : Mᵐᵒᵖ) ↦ (op ((f : (a : M) → N) (unop x)) : Nᵐᵒᵖ)) c)
        (Function.comp (β := M) (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ) (⇑f : (a : M) → N))
          (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M) x)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
N : Type u_7
F : Type u_8
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
inst_4 : TopologicalSpace N
inst_5 : SeparatelyContinuousMul N
f : F
⊢ SeparatelyContinuousMul M

Tactic:
letI := induced f ‹_›
  IsInducing.separatelyContinuousMul f ⟨rfl⟩

Premises used: Topology.IsInducing.separatelyContinuousMul, Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
S : Subsemigroup M
⊢ SeparatelyContinuousMul.{u_3} ↥S

Tactic:
IsInducing.separatelyContinuousMul
    ({ toFun := (↑), map_mul' := fun _ _ => rfl } : MulHom S M) ⟨rfl⟩

Premises used: Topology.IsInducing.separatelyContinuousMul, MulHom.mk, Topology.IsInducing.mk, Subtype.val, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : SeparatelyContinuousMul M
S : Submonoid M
⊢ SeparatelyContinuousMul.{u_3} ↥S

Tactic:
S.toSubsemigroup.separatelyContinuousMul

Premises used: Set.Mem, Submonoid.toSubsemigroup, Subsemigroup.separatelyContinuousMul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ K * V ⊆ U

Tactic:
hK.induction_on ?_ ?_ ?_ ?_

Premises used: IsCompact.induction_on
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
refine_1 : ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ ∅ * V ⊆ U
refine_2 :
  ∀ ⦃s t : Set M⦄,
    s ⊆ t →
      (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
        ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U
refine_3 :
  ∀ ⦃s t : Set M⦄,
    (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U) →
      (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
        ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ (s ∪ t) * V ⊆ U
refine_4 : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
⊢ Membership.mem (γ := Filter M) (𝓝 0) univ ∧ HMul.hMul (α := Set M) ∅ univ ⊆ U

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ ∅ * V ⊆ U

Tactic:
exact ⟨univ, by simp⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
s t : Set M
hst : s ⊆ t
V : Set M
hV : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : t * V ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U

Tactic:
⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩

Premises used: HasSubset.Subset.trans, Set.mul_subset_mul_right, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
s t : Set M
hst : s ⊆ t
V : Set M
hV : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : t * V ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U

Tactic:
exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
s t V : Set M
V_in : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : s * V ⊆ U
W : Set M
W_in : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : t * W ⊆ U
right : (s ∪ t) * (V ∩ W) ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ (s ∪ t) * V ⊆ U

Tactic:
use V ∩ W, inter_mem V_in W_in

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
s t V : Set M
V_in : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : s * V ⊆ U
W : Set M
W_in : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : t * W ⊆ U
right : s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
rw [union_mul]

Premises used: Set.union_mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
s t V : Set M
V_in : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : s * V ⊆ U
W : Set M
W_in : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Tactic:
union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset, Set.mul_subset_mul_left, Set.inter_subset_right
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
s t V : Set M
V_in : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : s * V ⊆ U
W : Set M
W_in : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Tactic:
exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset, Set.mul_subset_mul_left, Set.inter_subset_right
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 0)

Tactic:
simpa using hU
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
⊢ Membership.mem (γ := Filter M) (map (fun (p : M × M) ↦ p.1 * p.2) (𝓝 (x, 0))) U

Tactic:
have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)