awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
x y : H
⊢ Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) (x + y) =
    HAdd.hAdd (α := (↑s : Type u_2) → E) (β := (↑s : Type u_2) → E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) x : (↑s : Type u_2) → E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) y : (↑s : Type u_2) → E)

Tactic:
exact congr_arg s.restrict (map_add φ x y)

Premises used: map_add, congr_arg, Set.restrict
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
c : 𝕜
x : H
⊢ Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) (c • x) =
    HSMul.hSMul (α := 𝕜) (β := (↑s : Type u_2) → E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) x : (↑s : Type u_2) → E)

Tactic:
congr_arg s.restrict (map_smul φ c x)

Premises used: congr_arg, Set.restrict, map_smul
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
c : 𝕜
x : H
⊢ Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) (c • x) =
    HSMul.hSMul (α := 𝕜) (β := (↑s : Type u_2) → E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) x : (↑s : Type u_2) → E)

Tactic:
exact congr_arg s.restrict (map_smul φ c x)

Premises used: congr_arg, Set.restrict, map_smul
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
φ' : H →ₗ[𝕜] (↑s : Type u_2) → E :=
  { toFun := Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E), map_add' := ⋯,
    map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜 H

Tactic:
UniformFun.continuousSMul_induced_of_range_bounded 𝕜 s E H φ' ⟨rfl⟩ fun u ↦ ?_

Premises used: Set.Elem, UniformFun.continuousSMul_induced_of_range_bounded, Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
φ' : H →ₗ[𝕜] (↑s : Type u_2) → E :=
  { toFun := Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E), map_add' := ⋯,
    map_smul' := ⋯ }
refine :
  ∀ (u : H),
    Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E)
      (Set.range.{u_3, u_2 + 1} (ι := (↑s : Type u_2)) ((φ' : (a : H) → (↑s : Type u_2) → E) u))
⊢ ContinuousSMul 𝕜 H

Tactic:
refine UniformFun.continuousSMul_induced_of_range_bounded 𝕜 s E H φ' ⟨rfl⟩ fun u ↦ ?_

Premises used: Set.Elem, UniformFun.continuousSMul_induced_of_range_bounded, Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
φ' : H →ₗ[𝕜] (↑s : Type u_2) → E :=
  { toFun := Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E), map_add' := ⋯,
    map_smul' := ⋯ }
u : H
⊢ Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E)
    (Set.range.{u_3, u_2 + 1} (ι := (↑s : Type u_2)) ((φ' : (a : H) → (↑s : Type u_2) → E) u))

Tactic:
simpa only [Set.image_eq_range] using h u s hs

Premises used: Set.image_eq_range
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
H : Submodule 𝕜 (α →ᵤ[𝔖] E)
h : ∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)
⊢ ContinuousSMul 𝕜 ↥H

Tactic:
UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜 α E H
    (LinearMap.id.domRestrict H : H →ₗ[𝕜] α → E) IsInducing.subtypeVal fun ⟨u, hu⟩ => h u hu

Premises used: LinearMap.id, UniformOnFun.continuousSMul_induced_of_image_bounded, Membership.mem, Subtype, LinearMap.domRestrict, _private.0.UniformOnFun.continuousSMul_submodule_of_image_bounded.match_1, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Monoid.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : TopologicalSpace A
inst_1 : AddMonoidWithOne A
inst_2 : Monoid M
inst_3 : TopologicalSpace M
inst_4 : T2Space M
hdr : DenseRange.{u_1, 0} (X := A) Nat.cast
κ₁ κ₂ : AddChar A M
hκ₁ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₁ : (a : A) → M)
hκ₂ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₂ : (a : A) → M)
h : Eq.{u_2 + 1} (α := M) ((κ₁ : (a : A) → M) 1 : M) ((κ₂ : (a : A) → M) 1 : M)
⊢ κ₁ = κ₂

Tactic:
DFunLike.coe_injective <| hdr.equalizer hκ₁ hκ₂ (funext fun n ↦ ?_)

Premises used: DenseRange.equalizer, funext, DFunLike.coe_injective
-- Module: Mathlib.Topology.Algebra.Monoid.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : TopologicalSpace A
inst_1 : AddMonoidWithOne A
inst_2 : Monoid M
inst_3 : TopologicalSpace M
inst_4 : T2Space M
hdr : DenseRange.{u_1, 0} (X := A) Nat.cast
κ₁ κ₂ : AddChar A M
hκ₁ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₁ : (a : A) → M)
hκ₂ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₂ : (a : A) → M)
h : Eq.{u_2 + 1} (α := M) ((κ₁ : (a : A) → M) 1 : M) ((κ₂ : (a : A) → M) 1 : M)
refine :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := M)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := A) ((fun (f : AddChar A M) ↦ ((⇑f : (a : A) → M) : (a : A) → M)) κ₁)
        Nat.cast n)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := A) ((fun (f : AddChar A M) ↦ ((⇑f : (a : A) → M) : (a : A) → M)) κ₂)
        Nat.cast n)
⊢ κ₁ = κ₂

Tactic:
refine DFunLike.coe_injective <| hdr.equalizer hκ₁ hκ₂ (funext fun n ↦ ?_)

Premises used: DenseRange.equalizer, funext, DFunLike.coe_injective
-- Module: Mathlib.Topology.Algebra.Monoid.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : TopologicalSpace A
inst_1 : AddMonoidWithOne A
inst_2 : Monoid M
inst_3 : TopologicalSpace M
inst_4 : T2Space M
hdr : DenseRange.{u_1, 0} (X := A) Nat.cast
κ₁ κ₂ : AddChar A M
hκ₁ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₁ : (a : A) → M)
hκ₂ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₂ : (a : A) → M)
h : Eq.{u_2 + 1} (α := M) ((κ₁ : (a : A) → M) 1 : M) ((κ₂ : (a : A) → M) 1 : M)
n : ℕ
⊢ Eq.{u_2 + 1} (α := M)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := A) ((fun (f : AddChar A M) ↦ ((⇑f : (a : A) → M) : (a : A) → M)) κ₁)
      Nat.cast n)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := A) ((fun (f : AddChar A M) ↦ ((⇑f : (a : A) → M) : (a : A) → M)) κ₂)
      Nat.cast n)

Tactic:
simp only [Function.comp_apply, ← nsmul_one, h, AddChar.map_nsmul_eq_pow]

Premises used: AddChar.map_nsmul_eq_pow, Function.comp_apply, nsmul_one
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : M × M) ↦ p.1 * p.2

Tactic:
ContinuousMul.continuous_mul

Premises used: ContinuousMul.continuous_mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
α : Type u_2
f g : α → M
x : Filter α
a b : M
hf : Tendsto f x (𝓝 a)
hg : Tendsto g x (𝓝 b)
⊢ Tendsto (fun (x : α) ↦ f x * g x) x (𝓝 (a * b))

Tactic:
(continuous_mul.tendsto _).comp (hf.prodMk_nhds hg)

Premises used: continuous_mul, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
α : Type u_2
E : Type u_3
inst : CommGroup E
inst_1 : TopologicalSpace E
inst_2 : ContinuousMul E
f g : α → E
m : E
x : Filter α
hf : Tendsto f x (𝓝 m)
hfg : Tendsto (g / f) x (𝓝 1)
⊢ Tendsto g x (𝓝 m)

Tactic:
simpa using Tendsto.mul hf hfg

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f g : X → M
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
⊢ Continuous[inst_3, inst] (f * g)

Tactic:
continuous_mul.comp₂ hf hg

Premises used: Continuous.comp₂, continuous_mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f g : X → M
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (f * g) s x

Tactic:
Filter.Tendsto.mul hf hg

Premises used: ContinuousWithinAt, Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f g : X → M
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (f * g) x

Tactic:
Filter.Tendsto.mul hf hg

Premises used: ContinuousAt, Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f g : X → M
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (f * g) s

Tactic:
fun x hx ↦
  (hf x hx).mul (hg x hx)

Premises used: ContinuousOn, ContinuousWithinAt.mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
m : M
⊢ Continuous[inst, inst] fun (x : M) ↦ m * x

Tactic:
SeparatelyContinuousMul.continuous_const_mul

Premises used: SeparatelyContinuousMul.continuous_const_mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
m : M
⊢ Continuous[inst, inst] fun (x : M) ↦ x * m

Tactic:
SeparatelyContinuousMul.continuous_mul_const

Premises used: SeparatelyContinuousMul.continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
α : Type u_2
f : α → M
x : Filter α
a b : M
hf : Tendsto f x (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ b * f x) x (𝓝 (b * a))

Tactic:
continuous_const_mul b |>.tendsto _ |>.comp hf

Premises used: continuous_const_mul, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
α : Type u_2
f : α → M
x : Filter α
a b : M
hf : Tendsto f x (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ f x * b) x (𝓝 (a * b))

Tactic:
continuous_mul_const b |>.tendsto _ |>.comp hf

Premises used: Continuous.tendsto, Filter.Tendsto.comp, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
hf : Continuous[inst_3, inst] f
b : M
⊢ Continuous[inst_3, inst] fun (x : X) ↦ f x * b

Tactic:
continuous_mul_const b |>.comp hf

Premises used: Continuous.comp, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
hf : Continuous[inst_3, inst] f
b : M
⊢ Continuous[inst_3, inst] fun (x : X) ↦ b * f x

Tactic:
continuous_const_mul b |>.comp hf

Premises used: Continuous.comp, continuous_const_mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
s : Set X
x : X
hf : ContinuousWithinAt f s x
b : M
⊢ ContinuousWithinAt.{u_2, u_1} (Y := M) (fun (x : X) ↦ f x * b) s x

Tactic:
Filter.Tendsto.mul_const b hf

Premises used: ContinuousWithinAt, Filter.Tendsto.mul_const
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
s : Set X
x : X
hf : ContinuousWithinAt f s x
b : M
⊢ ContinuousWithinAt.{u_2, u_1} (Y := M) (fun (x : X) ↦ b * f x) s x

Tactic:
Filter.Tendsto.const_mul b hf

Premises used: ContinuousWithinAt, Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
x : X
hf : ContinuousAt f x
b : M
⊢ ContinuousAt.{u_2, u_1} (Y := M) (fun (x : X) ↦ f x * b) x

Tactic:
Filter.Tendsto.mul_const b hf

Premises used: ContinuousAt, Filter.Tendsto.mul_const
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
x : X
hf : ContinuousAt f x
b : M
⊢ ContinuousAt.{u_2, u_1} (Y := M) (fun (x : X) ↦ b * f x) x

Tactic:
Filter.Tendsto.const_mul b hf

Premises used: ContinuousAt, Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
s : Set X
hf : ContinuousOn f s
b : M
⊢ ContinuousOn.{u_2, u_1} (Y := M) (fun (x : X) ↦ f x * b) s

Tactic:
fun x hx ↦ (hf x hx).mul_const b

Premises used: ContinuousWithinAt.mul_const, ContinuousOn
-- Module: Mathlib.Topology.Algebra.Monoid.Defs
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : SeparatelyContinuousMul M
X : Type u_2
inst_3 : TopologicalSpace X
f : X → M
s : Set X
hf : ContinuousOn f s
b : M
⊢ ContinuousOn.{u_2, u_1} (Y := M) (fun (x : X) ↦ b * f x) s

Tactic:
fun x hx ↦ (hf x hx).const_mul b

Premises used: ContinuousWithinAt.const_mul, ContinuousOn
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
have : ∀ (this : Fintype X), Continuous (X := X → M) (map f)
⊢ Continuous (X := X → M) (map f)

Tactic:
have := Fintype.ofFinite X
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
⊢ Continuous (X := X → M) (map f)

Tactic:
continuous_pi (fun y ↦ ?_)

Premises used: continuous_pi
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
refine : ∀ (y : Y), Continuous (Y := M) fun (a : X → M) ↦ map f a y
⊢ Continuous (X := X → M) (map f)

Tactic:
refine continuous_pi (fun y ↦ ?_)

Premises used: continuous_pi
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
y : Y
simp : Continuous (Y := M) fun (a : X → M) ↦ ∑ x : X with f x = y, a x
⊢ Continuous (Y := M) fun (a : X → M) ↦ map f a y

Tactic:
simp only [FunOnFinite.map_apply_apply]

Premises used: FunOnFinite.map_apply_apply
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
y : Y
⊢ Continuous (Y := M) fun (a : X → M) ↦ ∑ x : X with f x = y, a x

Tactic:
continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)

Premises used: continuous_finsetSum, continuous_apply
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
y : Y
⊢ Continuous (Y := M) fun (a : X → M) ↦ ∑ x : X with f x = y, a x

Tactic:
exact continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)

Premises used: continuous_finsetSum, continuous_apply
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
have have₁ have₂ : ∀ (this : Fintype X), Continuous (X := X → M) (map f)
have₃ : ∀ (this : Fintype X) (y : Y), Continuous (Y := M) fun (a : X → M) ↦ map f a y
have₄ : ∀ (this : Fintype X) (y : Y), Continuous (Y := M) fun (a : X → M) ↦ ∑ x : X with f x = y, a x
⊢ Continuous (X := X → M) (map f)

Tactic:
classical
  have := Fintype.ofFinite X
  refine continuous_pi (fun y ↦ ?_)
  simp only [FunOnFinite.map_apply_apply]
  exact continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)

Premises used: continuous_pi, continuous_finsetSum, continuous_apply, FunOnFinite.map_apply_apply
-- Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
X : Type u_3
Y : Type u_4
inst_5 : Finite X
inst_6 : Finite Y
f : X → Y
⊢ Continuous (X := X → M) (Y := Y → M) (⇑(linearMap R M f) : (a : X → M) → Y → M)

Tactic:
FunOnFinite.continuous_map _ _

Premises used: FunOnFinite.continuous_map, FunOnFinite.map
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : One M
⊢ Continuous[inst, inst_1] 1

Tactic:
@continuous_const _ _ _ _ 1

Premises used: continuous_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 α
inst_2 : Mul α
inst_3 : ContinuousMul α
⊢ ContinuousMul.{u_2} αᵐᵒᵖ

Tactic:
⟨continuous_op.comp (continuous_unop.snd'.mul continuous_unop.fst')⟩

Premises used: Continuous.fst', Continuous.snd', Continuous.comp, MulOpposite.continuous_unop, ContinuousMul.mk, Continuous.mul, MulOpposite.continuous_op
-- 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
a : ULift.{u, u_3} M
⊢ Continuous[ULift.topologicalSpace, inst_1] fun (x : ULift.{u, u_3} M) ↦ a.down * x.down

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 : SeparatelyContinuousMul M
a : ULift.{u, u_3} M
⊢ Continuous[ULift.topologicalSpace, inst_1] fun (x : ULift.{u, u_3} M) ↦ x.down * a.down

Tactic:
fun_prop