awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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
⊢ LE.le (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖₁)) (instTopologicalSpace σ F 𝔖₁)
    (instTopologicalSpace σ F 𝔖₂)
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 𝔖₁)) (instTopologicalSpace σ F 𝔖₁)
    (instTopologicalSpace σ F 𝔖₂)
have simp_rw : LE.le (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖₁)) UniformSpace.toTopologicalSpace
  UniformSpace.toTopologicalSpace
Tactic: simp_rw [← uniformity_toTopologicalSpace_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
⊢ Continuous[inst_14, instTopologicalSpace σ F 𝔖] (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖)
have hf : Tendsto (α := G) (β := UniformConvergenceCLM σ F 𝔖) (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖) (𝓝 0) (𝓝 0)
Tactic: apply continuous_of_tendsto_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
⊢ Tendsto (α := G) (β := UniformConvergenceCLM σ F 𝔖) (⇑B : (a : G) → UniformConvergenceCLM σ F 𝔖) (𝓝 0) (𝓝 0)
have 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)
Tactic: suffices ∀ s ∈ 𝔖, ∀ U ∈ 𝓝 0, ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ s, B g e ∈ U by
    simpa [UniformConvergenceCLM.nhds_zero_eq, MapsTo]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
have 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)
Tactic: rcases mem_nhds_prod_iff.mp <| hB.tendsto' (0 : G × E) 0 (by simp) hU
    with ⟨V, hV, W, hW, hVW⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
have 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)
Tactic: rcases (h𝔖 S hS) hW |>.eventually_nhdsNE_zero.and eventually_mem_nhdsWithin |>.exists with
    ⟨c, hc, c_ne : c ≠ 0⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
have 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)
Tactic: rcases RingHom.surjective τ (σ c) with ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
have rwa : Ne.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) (0 : 𝕜₂)
Tactic: rwa [← map_ne_zero τ, hd, map_ne_zero σ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 : 𝕜₂)
⊢ d ≠ 0
have rwa₁ : Ne.{u_2 + 1} (α := 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂) (0 : 𝕜₂)
Tactic: rwa [← map_ne_zero τ, hd, map_ne_zero σ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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 : 𝕜₂)
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
have d_ne : d ≠ 0
Tactic: have d_ne : d ≠ 0 := by rwa [← map_ne_zero τ, hd, map_ne_zero σ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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
⊢ ∀ᶠ (g : G) in 𝓝 0,
    ∀ e ∈ S,
      Membership.mem (α := F) U
        ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) g : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
have h : ∀ a ∈ d • V,
  ∀ e ∈ S,
    Membership.mem (α := F) U
      ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) a : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) e : F)
Tactic: filter_upwards [(set_smul_mem_nhds_zero_iff d_ne).mpr hV]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 𝔖) ((fun (x : G) ↦ d • x) a) : (a : E) → F) x : F)
have h : Membership.mem (α := F) U
  ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) a : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) (c • x) : F)
Tactic: rw [map_smulₛₗ, hd, UniformConvergenceCLM.smul_apply, ← map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup G
inst_21 : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun (x : Set E) ↦ (⇑L : (a : E) → F) '' x) 𝔖 𝔗
this : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L
have this₁ : IsUniformAddGroup G
Tactic: haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup G
inst_21 : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun (x : Set E) ↦ (⇑L : (a : E) → F) '' x) 𝔖 𝔗
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this : IsUniformAddGroup G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L
have rw : Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformOnFun.topologicalSpace E G 𝔖]
  (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
    (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
      (DFunLike.coe (β := fun (a : E) ↦ G)))
    fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L)
Tactic: rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f
have this₁ : IsUniformAddGroup G
Tactic: haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this_2 : IsUniformAddGroup G
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup