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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ HasBasis (α := UniformConvergenceCLM σ F 𝔖)
    (comap (β := E →ᵤ[𝔖] F)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (𝓝
        (comp (α := UniformConvergenceCLM σ F 𝔖) (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F)
          (DFunLike.coe (β := fun (a : E) ↦ F)) 0)))
    (fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}

Tactic:
exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap DFunLike.coe

Premises used: Filter.HasBasis.comap, UniformOnFun.hasBasis_nhds_zero_of_basis, DFunLike.coe
-- 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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
⊢ HasBasis (α := UniformConvergenceCLM σ F 𝔖) (𝓝 0)
    (fun (SV : Prod.{u_3, u_4} (Set E) (Set F)) ↦ SV.1 ∈ 𝔖 ∧ Membership.mem (γ := Filter F) (𝓝 0) SV.2)
    fun (SV : Prod.{u_3, u_4} (Set E) (Set F)) ↦
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ SV.1, Membership.mem (α := F) SV.2 ((f : (a : E) → F) x : F)}

Tactic:
hasBasis_nhds_zero_of_basis σ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets

Premises used: Set.Mem, setOf, nhds, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, Filter.basis_sets, OfNat.ofNat
-- 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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
rw :
  Eq (α := Filter (UniformConvergenceCLM σ F 𝔖))
    (comap (β := E →ᵤ[𝔖] F)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (⨅ s ∈ 𝔖,
        ⨅ (i : ι),
          ⨅ (_ : p i),
            𝓟
              {g : E →ᵤ[𝔖] F |
                ∀ x ∈ s,
                  Membership.mem.{u_4, u_4} (α := F × F) (γ := Set (F × F)) {x : F × F | x.2 - x.1 ∈ b i}
                    (((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F)
                          (comp (α := UniformConvergenceCLM σ F 𝔖) (β := E → F)
                            (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) 0)
                          x,
                        (UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) g x) :
                      F × F)}))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s (b i)})
⊢ Eq (α := Filter (UniformConvergenceCLM σ F 𝔖)) (𝓝 0)
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s (b i)})

Tactic:
rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap,
    UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero]

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsInducing.nhds_eq_comap, UniformOnFun.nhds_eq_of_basis, Topology.IsEmbedding.isInducing, Filter.HasBasis.uniformity_of_nhds_zero
-- 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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Eq (α := Filter (UniformConvergenceCLM σ F 𝔖))
    (comap (β := E →ᵤ[𝔖] F)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (⨅ s ∈ 𝔖,
        ⨅ (i : ι),
          ⨅ (_ : p i),
            𝓟
              {g : E →ᵤ[𝔖] F |
                ∀ x ∈ s,
                  Membership.mem.{u_4, u_4} (α := F × F) (γ := Set (F × F)) {x : F × F | x.2 - x.1 ∈ b i}
                    (((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F)
                          (comp (α := UniformConvergenceCLM σ F 𝔖) (β := E → F)
                            (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) 0)
                          x,
                        (UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) g x) :
                      F × F)}))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s (b i)})

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- 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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
⊢ Eq (α := Filter (UniformConvergenceCLM σ F 𝔖)) (𝓝 0)
    (⨅ s ∈ 𝔖,
      ⨅ (t : Set F),
        ⨅ (_ : Membership.mem (γ := Filter F) (𝓝 0) t),
          𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s t})

Tactic:
nhds_zero_eq_of_basis _ _ _ (𝓝 0).basis_sets

Premises used: nhds, Filter.basis_sets, OfNat.ofNat, UniformConvergenceCLM.nhds_zero_eq_of_basis
-- 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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : Membership.mem (γ := Filter F) (𝓝 0) U
rw :
  ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in
    ⨅ s ∈ 𝔖,
      ⨅ (t : Set F),
        ⨅ (_ : Membership.mem (γ := Filter F) (𝓝 0) t),
          𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s t},
    MapsTo (⇑f : (a : E) → F) s U
⊢ ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in 𝓝 0, MapsTo (⇑f : (a : E) → F) s U

Tactic:
rw [nhds_zero_eq]

Premises used: UniformConvergenceCLM.nhds_zero_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
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in
    ⨅ s ∈ 𝔖,
      ⨅ (t : Set F),
        ⨅ (_ : Membership.mem (γ := Filter F) (𝓝 0) t),
          𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s t},
    MapsTo (⇑f : (a : E) → F) s U

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem
-- 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
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
h :
  ∀ (c : R)
    (hc :
      S ⊆
        HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
          {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}),
    image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U
⊢ Absorbs R U (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)

Tactic:
filter_upwards [hS (eventually_nhds_zero_mapsTo σ hs hU)] with c hc

Premises used: UniformConvergenceCLM.eventually_nhds_zero_mapsTo
-- 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
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc :
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}
h : ∀ x ∈ S, ∀ y ∈ s, Membership.mem (α := F) (c • U) ((x : (a : E) → F) y : F)
⊢ image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U

Tactic:
rw [image2_subset_iff]

Premises used: Set.image2_subset_iff
-- 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
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc :
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ S
x : E
hx : x ∈ s
h :
  ∀ (g : UniformConvergenceCLM σ F 𝔖)
    (hg :
      Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
        {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U} g)
    (hf : (fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g ∈ S),
    Membership.mem (α := F) (c • U) (((fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g : (a : E) → F) x : F)
⊢ Membership.mem (α := F) (c • U) ((f : (a : E) → F) x : F)

Tactic:
rcases hc hf with ⟨g, hg, rfl⟩

Premises used: rfl
-- 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
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc :
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}
x : E
hx : x ∈ s
g : UniformConvergenceCLM σ F 𝔖
hg :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U} g
hf : (fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g ∈ S
⊢ Membership.mem (α := F) (c • U) (((fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g : (a : E) → F) x : F)

Tactic:
smul_mem_smul_set (hg hx)

Premises used: Set.Mem, Set.smul_mem_smul_set
-- 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
R : Type u_6
inst_7 : SeminormedRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : DistribMulAction R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc :
  S ⊆
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U}
x : E
hx : x ∈ s
g : UniformConvergenceCLM σ F 𝔖
hg :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {x : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑x : (a : E) → F) s U} g
hf : (fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g ∈ S
⊢ Membership.mem (α := F) (c • U) (((fun (x : UniformConvergenceCLM σ F 𝔖) ↦ c • x) g : (a : E) → F) x : F)

Tactic:
exact smul_mem_smul_set (hg hx)

Premises used: Set.smul_mem_smul_set
-- 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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
⊢ IsVonNBounded R S ↔
    ∀ s ∈ 𝔖,
      IsVonNBounded.{u_6, u_4} R (E := F)
        (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)

Tactic:
⟨fun hS s hs ↦ isVonNBounded_image2_apply hS hs, fun h ↦ ?_⟩

Premises used: UniformConvergenceCLM.isVonNBounded_image2_apply, Iff.intro
-- 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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
refine :
  ∀
    (h :
      ∀ s ∈ 𝔖,
        IsVonNBounded.{u_6, u_4} R (E := F)
          (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)),
    IsVonNBounded R S
⊢ IsVonNBounded R S ↔
    ∀ s ∈ 𝔖,
      IsVonNBounded.{u_6, u_4} R (E := F)
        (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)

Tactic:
refine ⟨fun hS s hs ↦ isVonNBounded_image2_apply hS hs, fun h ↦ ?_⟩
-- 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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
simp_rw :
  ∀ (i : Set E) (i_1 : i ∈ 𝔖) (i_2 : Set F) (i_3 : Membership.mem (γ := Filter F) (𝓝 0) i_2),
    {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) i i_2} ∈ absorbing R S
⊢ IsVonNBounded R S

Tactic:
simp_rw [isVonNBounded_iff_absorbing_le, nhds_zero_eq, le_iInf_iff, le_principal_iff]

Premises used: Filter.le_principal_iff, Bornology.isVonNBounded_iff_absorbing_le, le_iInf_iff, UniformConvergenceCLM.nhds_zero_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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
rw :
  ∀ᶠ (a : R) in cobounded R,
    S ⊆
      HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) a
        {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}
⊢ {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U} ∈ absorbing R S

Tactic:
rw [Filter.mem_absorbing, Absorbs]

Premises used: Filter.mem_absorbing, Absorbs
-- 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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
h₁ :
  ∀ (c : R) (hc : image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U)
    (hc₀ : c ≠ 0) ⦃f : UniformConvergenceCLM σ F 𝔖⦄ (hf : f ∈ S),
    f ∈
      HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
        {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}
⊢ ∀ᶠ (a : R) in cobounded R,
    S ⊆
      HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) a
        {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}

Tactic:
filter_upwards [h s hs hU, eventually_ne_cobounded 0] with c hc hc₀ f hf

Premises used: Bornology.eventually_ne_cobounded, OfNat.ofNat
-- 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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc : image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U
hc₀ : c ≠ 0
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ S
h₁ :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U} (c⁻¹ • f)
⊢ f ∈
    HSMul.hSMul (β := Set (UniformConvergenceCLM σ F 𝔖)) c
      {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s U}

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc₀]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀
-- 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
R : Type u_6
inst_7 : NormedDivisionRing R
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : Module R F
inst_11 : ContinuousConstSMul R F
inst_12 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h :
  ∀ s ∈ 𝔖,
    IsVonNBounded.{u_6, u_4} R (E := F)
      (image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : R
hc : image2 (fun (f : UniformConvergenceCLM σ F 𝔖) (x : E) ↦ (f : (a : E) → F) x) S s ⊆ c • U
hc₀ : c ≠ 0
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ S
x : E
hx : x ∈ s
⊢ Membership.mem (α := F) U ((c⁻¹ • f : (a : E) → F) x : F)

Tactic:
simpa only [mem_smul_set_iff_inv_smul_mem₀ hc₀] using hc (mem_image2_of_mem hf hx)

Premises used: Set.mem_image2_of_mem, Set.mem_smul_set_iff_inv_smul_mem₀
-- 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
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
M : Type u_6
inst_7 : Monoid M
inst_8 : DistribMulAction M F
inst_9 : SMulCommClass 𝕜₂ M F
inst_10 : UniformSpace F
inst_11 : IsUniformAddGroup F
inst_12 : UniformContinuousConstSMul M F
𝔖 : Set (Set E)
x : M
x_1 : UniformConvergenceCLM σ F 𝔖
⊢ comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))
      (x • x_1) =
    HSMul.hSMul (β := E →ᵤ[𝔖] F) x
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) x_1)

Tactic:
rfl