awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Mul M
inst_3 : SeparatelyContinuousMul M
⊢ ContinuousConstSMul M M

Tactic:
⟨fun _ ↦ continuous_const_mul⟩

Premises used: SeparatelyContinuousMul.continuous_const_mul, ContinuousConstSMul.mk
-- 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 : Mul M
inst_3 : SeparatelyContinuousMul M
⊢ ContinuousConstSMul Mᵐᵒᵖ M

Tactic:
⟨fun _ ↦ continuous_mul_const⟩

Premises used: ContinuousConstSMul.mk, SeparatelyContinuousMul.continuous_mul_const
-- 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 : Mul M
inst_3 : ContinuousMul M
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : ULift.{u, u_3} M × ULift.{u, u_3} M) ↦
    ULift.down.{u, u_3} p.1 * ULift.down.{u, u_3} p.2

Tactic:
fun_prop
-- 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 : Mul M
inst_3 : ContinuousMul M
⊢ ContinuousSMul M M

Tactic:
⟨continuous_mul⟩

Premises used: ContinuousMul.continuous_mul, ContinuousSMul.mk
-- 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 : Mul M
inst_3 : ContinuousMul M
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    ((fun (p : M × M) ↦ p.1 * p.2) ∘ Prod.swap ∘ Prod.map MulOpposite.unop id)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ ContinuousMul α

Tactic:
⟨continuous_induced_rng.2 ?_⟩

Premises used: Iff.mpr, ContinuousMul.mk, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
refine :
  Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : α × α) ↦ p.1 * p.2)
⊢ ContinuousMul α

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
simp :
  Continuous[instTopologicalSpaceProd, tβ] fun (x : α × α) ↦
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x.1 : β) ((f : (a : α) → β) x.2 : β)
⊢ Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : α × α) ↦ p.1 * p.2)

Tactic:
simp only [Function.comp_def, map_mul]

Premises used: map_mul, Function.comp_def
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ Continuous[instTopologicalSpaceProd, tβ] fun (x : α × α) ↦
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x.1 : β) ((f : (a : α) → β) x.2 : β)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b : M
⊢ Tendsto (fun (p : M × M) ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
continuous_iff_continuousAt.mp ContinuousMul.continuous_mul (a, b)

Premises used: ContinuousAt, Prod.mk, ContinuousMul.continuous_mul, Iff.mp, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b : M
rw : map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)

Tactic:
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]

Premises used: Filter.map₂_mul, Filter.map_uncurry_prod, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)

Tactic:
continuous_mul.tendsto _

Premises used: Set.Mem, continuous_mul, Continuous.tendsto, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)

Tactic:
exact continuous_mul.tendsto _

Premises used: continuous_mul, Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a : M
⊢ 𝓝 1 * 𝓝 a = 𝓝 a

Tactic:
((le_nhds_mul _ _).trans_eq <| congr_arg _ (one_mul a)).antisymm <|
    le_mul_of_one_le_left' <| pure_le_nhds 1

Premises used: LE.le.trans_eq, pure_le_nhds, LE.le.antisymm, le_mul_of_one_le_left', congr_arg, OfNat.ofNat, one_mul, le_nhds_mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a : M
⊢ 𝓝 a * 𝓝 1 = 𝓝 a

Tactic:
((le_nhds_mul _ _).trans_eq <| congr_arg _ (mul_one a)).antisymm <|
    le_mul_of_one_le_right' <| pure_le_nhds 1

Premises used: LE.le.trans_eq, pure_le_nhds, LE.le.antisymm, congr_arg, le_mul_of_one_le_right', mul_one, OfNat.ofNat, le_nhds_mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_5
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : One X
b : X
⊢ 1 ≤ 𝓝 b ↔ 1 = b

Tactic:
pure_le_nhds_iff

Premises used: Set.Mem, pure_le_nhds_iff
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x : α
h_1 : f x ∈ Ioi c
rw : c < f x → b * c < b * f x
⊢ b * f x ∈ Ioi (b * c)

Tactic:
rw [Set.mem_Ioi] at *

Premises used: Set.mem_Ioi
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x : α
h_1 : c < f x
ha : 0 < b
⊢ b * c < b * f x

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x : α
h_1 : f x ∈ Iio c
rw : f x < c → b * f x < b * c
⊢ b * f x ∈ Iio (b * c)

Tactic:
rw [Set.mem_Iio] at *

Premises used: Set.mem_Iio
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x : α
h_1 : f x < c
ha : 0 < b
⊢ b * f x < b * c

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x : α
h_1 : f x ∈ Ioi c
rw : c < f x → c * b < f x * b
⊢ f x * b ∈ Ioi (c * b)

Tactic:
rw [Set.mem_Ioi] at *

Premises used: Set.mem_Ioi
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x : α
h_1 : c < f x
ha : 0 < b
⊢ c * b < f x * b

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x : α
h_1 : f x ∈ Iio c
rw : f x < c → f x * b < c * b
⊢ f x * b ∈ Iio (c * b)

Tactic:
rw [Set.mem_Iio] at *

Premises used: Set.mem_Iio
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x : α
h_1 : f x < c
ha : 0 < b
⊢ f x * b < c * b

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b c d : M
hab : a ⤳ b
hcd : c ⤳ d
⊢ (a * c) ⤳ (b * d)

Tactic:
hab.smul hcd

Premises used: Specializes.smul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b c d : M
hab : Inseparable a b
hcd : Inseparable c d
⊢ Inseparable (a * c) (b * d)

Tactic:
hab.smul hcd

Premises used: Inseparable.smul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a b : M
h : a ⤳ b
n : ℕ
⊢ (a ^ Nat.zero) ⤳ (b ^ Nat.zero)

Tactic:
simp only [pow_zero, specializes_rfl]

Premises used: pow_zero, specializes_rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a b : M
h : a ⤳ b
n x : ℕ
ihn : (a ^ x) ⤳ (b ^ x)
⊢ (a ^ x.succ) ⤳ (b ^ x.succ)

Tactic:
simpa only [pow_succ] using ihn.mul h

Premises used: pow_succ, Specializes.mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_6
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a b : M
h : Inseparable a b
n : ℕ
⊢ Inseparable (a ^ n) (b ^ n)

Tactic:
(h.specializes.pow n).antisymm (h.specializes'.pow n)

Premises used: Inseparable.specializes', Specializes.antisymm, Inseparable.specializes, Specializes.pow
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Monoid N
inst_6 : ContinuousMul N
inst_7 : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst_8 : l.NeBot
h₁ : Tendsto (fun (x : ι) ↦ (↑(f x) : N)) l (𝓝 r₁)
h₂ : Tendsto (fun (x : ι) ↦ (↑(f x)⁻¹ : N)) l (𝓝 r₂)
symm : 1 = r₁ * r₂
⊢ r₁ * r₂ = 1

Tactic:
symm
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Monoid N
inst_6 : ContinuousMul N
inst_7 : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst_8 : l.NeBot
h₁ : Tendsto (fun (x : ι) ↦ (↑(f x) : N)) l (𝓝 r₁)
h₂ : Tendsto (fun (x : ι) ↦ (↑(f x)⁻¹ : N)) l (𝓝 r₂)
⊢ 1 = r₁ * r₂

Tactic:
simpa using h₁.mul h₂

Premises used: Filter.Tendsto.mul
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Monoid N
inst_6 : ContinuousMul N
inst_7 : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst_8 : l.NeBot
h₁ : Tendsto (fun (x : ι) ↦ (↑(f x) : N)) l (𝓝 r₁)
h₂ : Tendsto (fun (x : ι) ↦ (↑(f x)⁻¹ : N)) l (𝓝 r₂)
symm : 1 = r₂ * r₁
⊢ r₂ * r₁ = 1

Tactic:
symm
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Monoid N
inst_6 : ContinuousMul N
inst_7 : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst_8 : l.NeBot
h₁ : Tendsto (fun (x : ι) ↦ (↑(f x) : N)) l (𝓝 r₁)
h₂ : Tendsto (fun (x : ι) ↦ (↑(f x)⁻¹ : N)) l (𝓝 r₂)
⊢ 1 = r₂ * r₁

Tactic:
simpa using h₂.mul h₁

Premises used: Filter.Tendsto.mul
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : ContinuousMul N
hf : Continuous[instTopologicalSpaceProd, inst_1] fun (x : (M × N) × M × N) ↦ x.1.1 * x.2.1
hg : Continuous[instTopologicalSpaceProd, inst_4] fun (x : (M × N) × M × N) ↦ x.1.2 * x.2.2
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : (M × N) × M × N) ↦ p.1 * p.2

Tactic:
apply Continuous.prodMk

Premises used: Continuous.prodMk
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : ContinuousMul N
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : (M × N) × M × N) ↦ x.1.1 * x.2.1

Tactic:
fun_prop
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : ContinuousMul N
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (x : (M × N) × M × N) ↦ x.1.2 * x.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
hf : Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x.1 * x_1.1
hg : Continuous[instTopologicalSpaceProd, inst_7] fun (x_1 : M × N) ↦ x.2 * x_1.2
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (x_1 : M × N) ↦ x * x_1

Tactic:
apply Continuous.prodMk

Premises used: Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x.1 * x_1.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (x_1 : M × N) ↦ x.2 * x_1.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
hf : Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x_1.1 * x.1
hg : Continuous[instTopologicalSpaceProd, inst_7] fun (x_1 : M × N) ↦ x_1.2 * x.2
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (x_1 : M × N) ↦ x_1 * x

Tactic:
apply Continuous.prodMk

Premises used: Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x_1.1 * x.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (x_1 : M × N) ↦ x_1.2 * x.2

Tactic:
fun_prop
-- 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 : Mul M
inst_3 : ContinuousMul M
⊢ ContinuousMul (ι → M)

Tactic:
Pi.continuousMul

Premises used: Pi.continuousMul
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : DiscreteTopology N
⊢ ContinuousMul N

Tactic:
⟨continuous_of_discreteTopology⟩

Premises used: ContinuousMul.mk, continuous_of_discreteTopology
-- 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 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : IndiscreteTopology N
⊢ ContinuousMul N

Tactic:
⟨continuous_of_indiscreteTopology⟩

Premises used: continuous_of_indiscreteTopology, ContinuousMul.mk
-- 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)
rw : ∀ (x : M × M), ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) x
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × M) ↦ p.1 * p.2

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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
h :
  ∀ (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) p
⊢ 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))

Tactic:
ext p
-- 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
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) p

Tactic:
simp [uncurry, mul_assoc]

Premises used: mul_assoc, 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
⊢ 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))

Tactic:
have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) =
        ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) := by
      ext p
      simp [uncurry, mul_assoc]
-- 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))
h : ∀ (x : M), ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) x = x₀ * y₀ * x
⊢ Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x

Tactic:
ext x
-- 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))
x : M
⊢ ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) x = x₀ * y₀ * x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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))
⊢ Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x

Tactic:
have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x := by
      ext x
      simp [mul_assoc]