awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
⊢ ∀ (y : E →L[𝕜] 𝕜),
    Continuous[inst_6, inst_1] fun (a : E) ↦
      (((LinearMap.flip (topDualPairing 𝕜 E) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
              (AddHom.toFun (LinearMap.toAddHom (↑(toWeakSpace 𝕜 E) : E →ₗ[𝕜] WeakSpace 𝕜 E)) a) :
            (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) :
          (a : E →L[𝕜] 𝕜) → 𝕜)
        y

Tactic:
ContinuousLinearMap.continuous

Premises used: ContinuousLinearMap.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
⊢ ∀ (y : E →L[𝕜] 𝕜),
    Continuous[inst_6, inst_1] fun (a : E) ↦
      (((LinearMap.flip (topDualPairing 𝕜 E) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
              (AddHom.toFun (LinearMap.toAddHom (↑(toWeakSpace 𝕜 E) : E →ₗ[𝕜] WeakSpace 𝕜 E)) a) :
            (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) :
          (a : E →L[𝕜] 𝕜) → 𝕜)
        y

Tactic:
exact ContinuousLinearMap.continuous

Premises used: ContinuousLinearMap.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x : E
⊢ Eq (α := WeakSpace 𝕜 E) ((toWeakSpaceCLM 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
    ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
⊢ Function.Bijective (α := E) (β := WeakSpace 𝕜 E) (⇑(toWeakSpaceCLM 𝕜 E) : (a : E) → WeakSpace 𝕜 E)

Tactic:
(toWeakSpace 𝕜 E).bijective

Premises used: LinearEquiv.bijective, toWeakSpace
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
⊢ IsOpenMap (X := WeakSpace 𝕜 E) (Y := E) (⇑(LinearEquiv.symm (toWeakSpace 𝕜 E)) : (a : WeakSpace 𝕜 E) → E)

Tactic:
IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont
    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv

Premises used: LinearEquiv.right_inv, LinearEquiv.left_inv, toWeakSpaceCLM, IsOpenMap.of_inverse, toWeakSpace, ContinuousLinearMap.cont
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
V : Set E
hV : IsOpen (X := WeakSpace 𝕜 E) ((⇑(toWeakSpaceCLM 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' V)
⊢ IsOpen[inst_6] V

Tactic:
simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV

Premises used: Set.image_image, isOpenMap_toWeakSpace_symm
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
l : Filter α
f : α → WeakDual 𝕜 E
x : WeakDual 𝕜 E
⊢ Tendsto f l (𝓝 x) ↔
    ∀ (y : E),
      Tendsto.{u_1, u_2} (β := 𝕜)
        (fun (i : α) ↦ ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) (f i) : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)) l
        (𝓝 ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y) : Filter 𝕜)

Tactic:
WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective

Premises used: WeakBilin.tendsto_iff_forall_eval_tendsto, WeakDual, ContinuousLinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommRing 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : IsTopologicalAddGroup 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : IsTopologicalAddGroup E
⊢ IsTopologicalAddGroup.{u_4} (WeakSpace 𝕜 E)

Tactic:
WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip

Premises used: instAddCommMonoidWeakBilin._aux_1, instAddCommMonoidWeakBilin._aux_4, topDualPairing, LinearMap.flip, WeakSpace.instAddCommGroup._aux_2, instAddCommMonoidWeakSpace._aux_2, WeakSpace, instAddCommMonoidWeakSpace._aux_1, WeakBilin.instIsTopologicalAddGroup, WeakSpace.instAddCommGroup._aux_1
-- Module: Mathlib.Topology.Algebra.Module.Star
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TrivialStar R
inst_3 : AddCommMonoid A
inst_4 : StarAddMonoid A
inst_5 : Module R A
inst_6 : StarModule R A
inst_7 : TopologicalSpace A
inst_8 : ContinuousStar A
r : R
a : A
⊢ (AddEquiv.toEquiv (AddEquiv.refl A)).toFun (r • a) =
    HSMul.hSMul (α := R) ((starRingEnd R : (a : R) → R) r : R) ((AddEquiv.toEquiv (AddEquiv.refl A)).toFun a)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Star
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
inst_8 : TopologicalSpace A
inst_9 : ContinuousAdd A
inst_10 : ContinuousStar A
inst_11 : ContinuousConstSMul R A
⊢ Continuous.{u_2, u_2} (X := A) (Y := ↥(selfAdjoint A)) (⇑(selfAdjointPart R) : (a : A) → ↥(selfAdjoint A))

Tactic:
((continuous_const_smul _).comp <| continuous_id.add continuous_star).subtype_mk _

Premises used: ContinuousConstSMul.continuous_const_smul, ContinuousStar.continuous_star, Continuous.comp, Continuous.subtype_mk, continuous_id, Continuous.add
-- Module: Mathlib.Topology.Algebra.Module.Star
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
inst_8 : TopologicalSpace A
inst_9 : ContinuousSub A
inst_10 : ContinuousStar A
inst_11 : ContinuousConstSMul R A
⊢ Continuous.{u_2, u_2} (X := A) (Y := ↥(skewAdjoint A)) (⇑(skewAdjointPart R) : (a : A) → ↥(skewAdjoint A))

Tactic:
((continuous_const_smul _).comp <| continuous_id.sub continuous_star).subtype_mk _

Premises used: ContinuousConstSMul.continuous_const_smul, ContinuousStar.continuous_star, Continuous.comp, Continuous.subtype_mk, continuous_id, Continuous.sub
-- Module: Mathlib.Topology.Algebra.Module.Star
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
inst_8 : TopologicalSpace A
inst_9 : IsTopologicalAddGroup A
inst_10 : ContinuousStar A
inst_11 : ContinuousConstSMul R A
⊢ Continuous (X := A) (Y := ↥(selfAdjoint A) × ↥(skewAdjoint A))
    (⇑(StarModule.decomposeProdAdjoint R A) : (a : A) → ↥(selfAdjoint A) × ↥(skewAdjoint A))

Tactic:
(continuous_selfAdjointPart R A).prodMk (continuous_skewAdjointPart R A)

Premises used: continuous_selfAdjointPart, Function.prod, continuous_skewAdjointPart, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Module.Star
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
inst_8 : TopologicalSpace A
inst_9 : ContinuousAdd A
⊢ Continuous (X := ↥(selfAdjoint A) × ↥(skewAdjoint A)) (Y := A)
    (⇑(LinearEquiv.symm (StarModule.decomposeProdAdjoint R A)) : (a : ↥(selfAdjoint A) × ↥(skewAdjoint A)) → A)

Tactic:
(continuous_subtype_val.comp continuous_fst).add (continuous_subtype_val.comp continuous_snd)

Premises used: continuous_subtype_val, Continuous.comp, continuous_snd, continuous_fst, Continuous.add
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
e_1 : α ≃ β
inst : TopologicalSpace β
inst_1 : AddCommMonoid β
inst_2 : Semiring R
inst_3 : Module R β
e : α ≃ β
this_1 : TopologicalSpace α := e.topologicalSpace
this_2 : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
simp : Continuous (LinearEquiv.invFun (linearEquiv R e))
⊢ Continuous (LinearEquiv.invFun (linearEquiv R e))

Tactic:
simp +instances only [Equiv.topologicalSpace, ← @coinduced_symm]

Premises used: Equiv.coinduced_symm, Equiv.topologicalSpace
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
e_1 : α ≃ β
inst : TopologicalSpace β
inst_1 : AddCommMonoid β
inst_2 : Semiring R
inst_3 : Module R β
e : α ≃ β
this_1 : TopologicalSpace α := e.topologicalSpace
this_2 : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
⊢ Continuous (LinearEquiv.invFun (linearEquiv R e))

Tactic:
continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
e_1 : α ≃ β
inst : TopologicalSpace β
inst_1 : AddCommMonoid β
inst_2 : Semiring R
inst_3 : Module R β
e : α ≃ β
this_1 : TopologicalSpace α := e.topologicalSpace
this_2 : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
⊢ Continuous (LinearEquiv.invFun (linearEquiv R e))

Tactic:
exact continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : AddCommMonoid β
inst_2 : Semiring R
inst_3 : Module R β
e : α ≃ β
⊢ Eq (α := α ≃ₗ[R] β) (↑(continuousLinearEquiv R e) : α ≃ₗ[R] β) (linearEquiv R e)

Tactic:
rfl

Premises used: Equiv.linearEquiv, rfl
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
f : (q : β × β) → β := fun (q : β × β) ↦ q.1 * q.2
⊢ Continuous (Y := α) fun (p : α × α) ↦ (e.symm : (a : β) → α) (f ((e : (a : α) → β) p.1, (e : (a : α) → β) p.2))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
f : (q : β × β) → β := fun (q : β × β) ↦ q.1 * q.2
⊢ Continuous (Y := α) fun (p : α × α) ↦ (e.symm : (a : β) → α) (f ((e : (a : α) → β) p.1, (e : (a : α) → β) p.2))

Tactic:
have : Continuous (fun p ↦ e.symm <| f (e p.1, e p.2) : (α × α → α)) := by fun_prop
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
f : (q : β × β) → β := fun (q : β × β) ↦ q.1 * q.2
this : Continuous (Y := α) fun (p : α × α) ↦ (e.symm : (a : β) → α) (f ((e : (a : α) → β) p.1, (e : (a : α) → β) p.2))
p : α × α
⊢ (e.symm : (a : β) → α) (f ((e : (a : α) → β) p.1, (e : (a : α) → β) p.2)) = p.1 * p.2

Tactic:
simp [f]
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
f : (q : β × β) → β := fun (q : β × β) ↦ q.1 * q.2
this : Continuous (Y := α) fun (p : α × α) ↦ (e.symm : (a : β) → α) (f ((e : (a : α) → β) p.1, (e : (a : α) → β) p.2))
⊢ Continuous (Y := α) fun (p : α × α) ↦ p.1 * p.2

Tactic:
exact this.congr <| fun p ↦ by simp [f]

Premises used: Continuous.congr
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
⊢ Continuous.{u_2, u_2} (X := α) (Y := α)
    (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑e.symm : (a : β) → α)
      ((fun (q : β) ↦ q⁻¹) ∘ (⇑e : (a : α) → β)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
⊢ Continuous.{u_2, u_2} (X := α) (Y := α)
    (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑e.symm : (a : β) → α)
      ((fun (q : β) ↦ q⁻¹) ∘ (⇑e : (a : α) → β)))

Tactic:
have : Continuous (e.symm ∘ (fun q ↦ q⁻¹) ∘ e) := by fun_prop
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
this :
  Continuous.{u_2, u_2} (X := α) (Y := α)
    (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑e.symm : (a : β) → α)
      ((fun (q : β) ↦ q⁻¹) ∘ (⇑e : (a : α) → β)))
p : α
⊢ Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑e.symm : (a : β) → α) ((fun (q : β) ↦ q⁻¹) ∘ (⇑e : (a : α) → β))
      p =
    p⁻¹

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
this :
  Continuous.{u_2, u_2} (X := α) (Y := α)
    (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑e.symm : (a : β) → α)
      ((fun (q : β) ↦ q⁻¹) ∘ (⇑e : (a : α) → β)))
⊢ Continuous (Y := α) fun (a : α) ↦ a⁻¹

Tactic:
exact this.congr (fun p ↦ by simp)

Premises used: Continuous.congr
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : TopologicalSpace β
inst_2 : AddCommGroup β
inst_3 : Module R β
inst_4 : TopologicalSpace R
inst_5 : ContinuousSMul R β
inst_6 : TopologicalSpace α
inst_7 : AddCommGroup α
inst_8 : Module R α
e : α ≃L[R] β
f : R × α → α := fun (p : R × α) ↦ (e.symm : (a : β) → α) (HSMul.hSMul (β := β) p.1 ((e : (a : α) → β) p.2 : β))
⊢ Continuous f

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : TopologicalSpace β
inst_2 : AddCommGroup β
inst_3 : Module R β
inst_4 : TopologicalSpace R
inst_5 : ContinuousSMul R β
inst_6 : TopologicalSpace α
inst_7 : AddCommGroup α
inst_8 : Module R α
e : α ≃L[R] β
f : R × α → α := fun (p : R × α) ↦ (e.symm : (a : β) → α) (HSMul.hSMul (β := β) p.1 ((e : (a : α) → β) p.2 : β))
⊢ Continuous f

Tactic:
have : Continuous f := by fun_prop
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : TopologicalSpace β
inst_2 : AddCommGroup β
inst_3 : Module R β
inst_4 : TopologicalSpace R
inst_5 : ContinuousSMul R β
inst_6 : TopologicalSpace α
inst_7 : AddCommGroup α
inst_8 : Module R α
e : α ≃L[R] β
f : R × α → α := fun (p : R × α) ↦ (e.symm : (a : β) → α) (HSMul.hSMul (β := β) p.1 ((e : (a : α) → β) p.2 : β))
this : Continuous f
p : R × α
⊢ f p = p.1 • p.2

Tactic:
simp [f]
-- Module: Mathlib.Topology.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
inst_1 : TopologicalSpace β
inst_2 : AddCommGroup β
inst_3 : Module R β
inst_4 : TopologicalSpace R
inst_5 : ContinuousSMul R β
inst_6 : TopologicalSpace α
inst_7 : AddCommGroup α
inst_8 : Module R α
e : α ≃L[R] β
f : R × α → α := fun (p : R × α) ↦ (e.symm : (a : β) → α) (HSMul.hSMul (β := β) p.1 ((e : (a : α) → β) p.2 : β))
this : Continuous f
⊢ Continuous (Y := α) fun (p : R × α) ↦ p.1 • p.2

Tactic:
exact this.congr (fun p ↦ by simp [f])

Premises used: Continuous.congr
-- 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 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
⊢ IsTopologicalAddGroup H

Tactic:
have : IsTopologicalAddGroup H :=
    let ofFun' : (α → E) →+ (α →ᵤ E) := AddMonoidHom.id _
    IsInducing.topologicalAddGroup (ofFun'.comp (φ : H →+ (α → E))) hφ
-- 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 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
simp :
  HasBasis.{u_4, u_3 + 1} (α := H)
    (comap (β := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
      (𝓝 ((ofFun : (a : α → E) → α →ᵤ E) 0)))
    (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
⊢ HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}

Tactic:
simp only [hφ.nhds_eq_comap, Function.comp_apply, map_zero]

Premises used: Topology.IsInducing.nhds_eq_comap, map_zero, Function.comp_apply
-- 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 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
⊢ HasBasis.{u_4, u_3 + 1} (α := H)
    (comap (β := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
      (𝓝 ((ofFun : (a : α → E) → α →ᵤ E) 0)))
    (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}

Tactic:
UniformFun.hasBasis_nhds_zero.comap _

Premises used: Set.Mem, setOf, UniformFun.hasBasis_nhds_zero, Filter.HasBasis.comap, Set.preimage, instZeroUniformFun._aux_1
-- 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 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
⊢ HasBasis.{u_4, u_3 + 1} (α := H)
    (comap (β := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
      (𝓝 ((ofFun : (a : α → E) → α →ᵤ E) 0)))
    (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}

Tactic:
exact UniformFun.hasBasis_nhds_zero.comap _

Premises used: UniformFun.hasBasis_nhds_zero, Filter.HasBasis.comap
-- 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 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
⊢ HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}

Tactic:
have hb : (𝓝 (0 : H)).HasBasis (· ∈ 𝓝 (0 : E)) fun V ↦ {u | ∀ x, φ u x ∈ V} := by
    simp only [hφ.nhds_eq_comap, Function.comp_apply, map_zero]
    exact UniformFun.hasBasis_nhds_zero.comap _
-- 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 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
hsmul :
  ∀ {i : Set E},
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (V : Set 𝕜),
        Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
          ∃ (j : Set E),
            Membership.mem (γ := Filter E) (𝓝 0) j ∧
              HSMul.hSMul (β := Set H) V
                  {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)} ⊆
                {u : H | ∀ (x : α), Membership.mem (α := E) i ((φ : (a : H) → α → E) u x : E)}
hsmul_left :
  ∀ (x₀ : 𝕜) {i : Set E},
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) j ∧
          Set.MapsTo (β := H) (fun (x : H) ↦ x₀ • x)
            {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)}
            {u : H | ∀ (x : α), Membership.mem (α := E) i ((φ : (a : H) → α → E) u x : E)}
hsmul_right :
  ∀ (m₀ : H) {i : Set E},
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∀ᶠ (x : 𝕜) in 𝓝 0,
        Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) i ((φ : (a : H) → α → E) u x : E)}
          (x • m₀)
⊢ ContinuousSMul 𝕜 H

Tactic:
apply ContinuousSMul.of_basis_zero hb

Premises used: ContinuousSMul.of_basis_zero