awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
x x_1 : F
⊢ { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x + x_1), cont := ⋯ } =
    HAdd.hAdd (α := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B))
      { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x, cont := ⋯ :
        ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
      { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
        ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
have h : ∀ (x_2 : WeakBilin B),
  Eq.{u_2 + 1} (α := 𝕜)
    (({ toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x + x_1), cont := sorry } : (a : WeakBilin B) → 𝕜) x_2 : 𝕜)
    ((HAdd.hAdd (α := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B))
            { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x, cont := sorry :
              ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
            { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := sorry :
              ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 } :
          (a : WeakBilin B) → 𝕜)
        x_2 :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
x : 𝕜
x_1 : F
⊢ { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x • x_1), cont := ⋯ } =
    HSMul.hSMul (α := 𝕜) (β := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
        ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
have h : ∀ (x_2 : WeakBilin B),
  Eq.{u_2 + 1} (α := 𝕜)
    (({ toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x • x_1), cont := sorry } : (a : WeakBilin B) → 𝕜) x_2 : 𝕜)
    ((HSMul.hSMul (α := 𝕜) (β := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
            { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := sorry :
              ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 } :
          (a : WeakBilin B) → 𝕜)
        x_2 :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpace B, instTopologicalSpace B] fun (a : WeakBilin B) ↦ -a
have refine : ∀ (y : F),
  Continuous[instTopologicalSpace B, inst] fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y
Tactic: refine continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
y : F
⊢ Continuous[instTopologicalSpace B, inst] fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y
have refine : Eq (α := (a : WeakBilin B) → 𝕜) (fun (x : WeakBilin B) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y))
  fun (a : WeakBilin B) ↦
  ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (a : WeakBilin B) ↦ -a)
    a y
Tactic: refine cast (congr_arg _ ?_) (eval_continuous B (-y))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
y : F
⊢ Eq (α := (a : WeakBilin B) → 𝕜)
    (fun (x : WeakBilin B) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y)) fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y
have h : ∀ (x : WeakBilin B),
  Eq.{u_2 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y) : 𝕜)
    (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
          fun (a : WeakBilin B) ↦ -a)
        x y :
      𝕜)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakDual (goal)
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
⊢ Continuous[inst_6, _] (AddHom.toFun (LinearMap.toAddHom (↑(toWeakSpace 𝕜 E) : E →ₗ[𝕜] WeakSpace 𝕜 E)))
have h : ∀ (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: apply WeakBilin.continuous_of_continuous_eval
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TransferInstance (goal)
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))
have simp : Continuous (LinearEquiv.invFun (linearEquiv R e))
Tactic: simp +instances only [Equiv.topologicalSpace, ← @coinduced_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TransferInstance (hypothesis)
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 : α × α) ↦ p.1 * p.2
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TransferInstance (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
inst_3 : TopologicalSpace α
inst_4 : Group α
e : α ≃ₜ* β
⊢ Continuous (Y := α) fun (a : α) ↦ a⁻¹
have 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 : α) → β)))
Tactic: have : Continuous (e.symm ∘ (fun q ↦ q⁻¹) ∘ e) := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TransferInstance (hypothesis)
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 (Y := α) fun (p : R × α) ↦ p.1 • p.2
have this : Continuous f
Tactic: have : Continuous f := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (hypothesis)
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))
⊢ ContinuousSMul 𝕜 H
have this : IsTopologicalAddGroup H
Tactic: have : IsTopologicalAddGroup H :=
    let ofFun' : (α → E) →+ (α →ᵤ E) := AddMonoidHom.id _
    IsInducing.topologicalAddGroup (ofFun'.comp (φ : H →+ (α → E))) hφ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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)}
have 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)}
Tactic: simp only [hφ.nhds_eq_comap, Function.comp_apply, map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (hypothesis)
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
⊢ ContinuousSMul 𝕜 H
have 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)}
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 _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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)}
⊢ ContinuousSMul 𝕜 H
have 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)}
Tactic: apply ContinuousSMul.of_basis_zero hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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)}
⊢ ContinuousSMul 𝕜 H
have 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)}
Tactic: apply ContinuousSMul.of_basis_zero hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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)}
⊢ ContinuousSMul 𝕜 H
have 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₀)
Tactic: apply ContinuousSMul.of_basis_zero hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (hypothesis)
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)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (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) U ((φ : (a : H) → α → E) u x : E)}
have this₁ : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
Tactic: have : Tendsto (fun x : 𝕜 × E ↦ x.1 • x.2) (𝓝 0) (𝓝 0) :=
      continuous_smul.tendsto' _ _ (zero_smul _ _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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_1 : 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)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
⊢ ∃ (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) U ((φ : (a : H) → α → E) u x : E)}
have hsmul : ∀ (V : Set 𝕜) (W : Set E) (hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U)
  (hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1) (hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2),
  ∃ (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) U ((φ : (a : H) → α → E) u x : E)}
Tactic: rcases ((Filter.basis_sets _).prod_nhds (Filter.basis_sets _)).tendsto_left_iff.1 this U hU
      with ⟨⟨V, W⟩, ⟨hV, hW⟩, hVW⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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_1 : 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)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
⊢ ∃ (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) U ((φ : (a : H) → α → E) u x : E)}
have hsmul : ∀ (a : 𝕜) (ha : a ∈ V) (u : H)
  (hu : Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) W ((φ : (a : H) → α → E) u x : E)} u)
  (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) (a • u) x : E)
Tactic: refine ⟨V, hV, W, hW, Set.smul_subset_iff.2 fun a ha u hu x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
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_1 : 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)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
a : 𝕜
ha : a ∈ V
u : H
hu : Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) W ((φ : (a : H) → α → E) u x : E)} u
x : α
⊢ Membership.mem (α := E) U ((φ : (a : H) → α → E) (a • u) x : E)
have hsmul : HSMul.hSMul (β := α → E) a ((φ : (a : H) → α → E) u : α → E) x ∈ U
Tactic: rw [map_smul]