awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ LE.le (α := UniformSpace (UniformConvergenceCLM σ F 𝔖₁))
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₁) : (a : E → F) → E →ᵤ[𝔖₁] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖₁))
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₂) : (a : E → F) → E →ᵤ[𝔖₂] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖₂))

Tactic:
exact UniformSpace.comap_mono (UniformOnFun.mono (le_refl _) h)

Premises used: le_refl, UniformOnFun.mono, UniformSpace.comap_mono
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
simp_rw :
  LE.le (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖₁)) UniformSpace.toTopologicalSpace
    UniformSpace.toTopologicalSpace
⊢ LE.le (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖₁)) (instTopologicalSpace σ F 𝔖₁)
    (instTopologicalSpace σ F 𝔖₂)

Tactic:
simp_rw [← uniformity_toTopologicalSpace_eq]

Premises used: UniformConvergenceCLM.uniformity_toTopologicalSpace_eq
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ LE.le (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖₁)) UniformSpace.toTopologicalSpace
    UniformSpace.toTopologicalSpace

Tactic:
UniformSpace.toTopologicalSpace_mono (uniformSpace_mono σ F h)

Premises used: UniformConvergenceCLM.uniformSpace_mono, UniformSpace.toTopologicalSpace_mono
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ LE.le (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖₁)) UniformSpace.toTopologicalSpace
    UniformSpace.toTopologicalSpace

Tactic:
exact UniformSpace.toTopologicalSpace_mono (uniformSpace_mono σ F h)

Premises used: UniformConvergenceCLM.uniformSpace_mono, UniformSpace.toTopologicalSpace_mono
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
hf : Tendsto (α := G) (β := UniformConvergenceCLM σ F 𝔖) (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖) (𝓝 0) (𝓝 0)
⊢ Continuous[inst_14, instTopologicalSpace σ F 𝔖] (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖)

Tactic:
apply continuous_of_tendsto_nhds_zero

Premises used: continuous_of_tendsto_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
this :
  ∀ s ∈ 𝔖,
    ∀ (U : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) U →
        ∀ᶠ (g : G) in 𝓝 0,
          ∀ e ∈ s,
            Membership.mem (α := F) U
              ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
⊢ Tendsto (α := G) (β := UniformConvergenceCLM σ F 𝔖) (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖) (𝓝 0) (𝓝 0)

Tactic:
simpa [UniformConvergenceCLM.nhds_zero_eq, MapsTo]

Premises used: Set.MapsTo, UniformConvergenceCLM.nhds_zero_eq
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
hf :
  ∀ s ∈ 𝔖,
    ∀ (U : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) U →
        ∀ᶠ (g : G) in 𝓝 0,
          ∀ e ∈ s,
            Membership.mem (α := F) U
              ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
⊢ Tendsto (α := G) (β := UniformConvergenceCLM σ F 𝔖) (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖) (𝓝 0) (𝓝 0)

Tactic:
suffices ∀ s ∈ 𝔖, ∀ U ∈ 𝓝 0, ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ s, B g e ∈ U by
    simpa [UniformConvergenceCLM.nhds_zero_eq, MapsTo]
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ Eq.{u_4 + 1} (α := F) (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) 0.1 : (a : E) → F) 0.2 : F) (0 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
hf :
  ∀ (V : Set G) (hV : Membership.mem (γ := Filter G) (𝓝 0) V) (W : Set E) (hW : Membership.mem (γ := Filter E) (𝓝 0) W)
    (hVW :
      V ×ˢ W ⊆
        (fun (p : G × E) ↦
            (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
          U),
    ∀ᶠ (g : G) in 𝓝 0,
      ∀ e ∈ S,
        Membership.mem (α := F) U
          ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)

Tactic:
rcases mem_nhds_prod_iff.mp <| hB.tendsto' (0 : G × E) 0 (by simp) hU
    with ⟨V, hV, W, hW, hVW⟩

Premises used: mem_nhds_prod_iff, Iff.mp, Continuous.tendsto', OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
hf :
  ∀ (c : 𝕜₁) (hc : MapsTo (fun (x : E) ↦ c • x) S W) (c_ne : c ≠ 0),
    ∀ᶠ (g : G) in 𝓝 0,
      ∀ e ∈ S,
        Membership.mem (α := F) U
          ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)

Tactic:
rcases (h𝔖 S hS) hW |>.eventually_nhdsNE_zero.and eventually_mem_nhdsWithin |>.exists with
    ⟨c, hc, c_ne : c ≠ 0⟩

Premises used: eventually_mem_nhdsWithin, Absorbs.eventually_nhdsNE_zero, Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
hf :
  ∀ (d : 𝕜₃) (hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)),
    ∀ᶠ (g : G) in 𝓝 0,
      ∀ e ∈ S,
        Membership.mem (α := F) U
          ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)

Tactic:
rcases RingHom.surjective τ (σ c) with ⟨d, hd⟩

Premises used: RingHom.surjective, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
rwa : Ne.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) (0 : 𝕜₂)
rwa₁ : Ne.{u_2 + 1} (α := 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) (0 : 𝕜₂)
rwa₂ rwa₃ rwa₄ rwa₅ : c ≠ 0
⊢ d ≠ 0

Tactic:
rwa [← map_ne_zero τ, hd, map_ne_zero σ]

Premises used: map_ne_zero
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
⊢ d ≠ 0

Tactic:
have d_ne : d ≠ 0 := by rwa [← map_ne_zero τ, hd, map_ne_zero σ]
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
d_ne : d ≠ 0
h :
  ∀ a ∈ d • V,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) a : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)

Tactic:
filter_upwards [(set_smul_mem_nhds_zero_iff d_ne).mpr hV]

Premises used: Iff.mpr, set_smul_mem_nhds_zero_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
h :
  Membership.mem (α := F) U
    ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) a : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) (c • x) : F)
⊢ Membership.mem (α := F) U
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) ((fun (x : G) ↦ d • x) a) : (a : E) → F) x : F)

Tactic:
rw [map_smulₛₗ, hd, UniformConvergenceCLM.smul_apply, ← map_smulₛₗ]

Premises used: UniformConvergenceCLM.smul_apply, MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ Membership.mem (α := F) U
    ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) a : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) (c • x) : F)

Tactic:
@hVW ⟨_, _⟩ ⟨ha, hc hx⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro