awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
G : Type u_10
H : Type u_11
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e₁ : E ≃L[𝕜] F
e₂ : H ≃L[𝕜] G
φ : F →L_c[𝕜] G
e : E
⊢ Eq.{u_11 + 1} (α := H)
    ((((ContinuousLinearEquiv.symm (e₁.compactConvergenceCLMCongr e₂) : (a : F →L_c[𝕜] G) → E →L_c[𝕜] H) φ :
            E →L_c[𝕜] H) :
          (a : E) → H)
        e :
      H)
    ((e₂.symm : (a : G) → H) ((φ : (a : F) → G) ((e₁ : (a : E) → F) e : F) : G) : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
⊢ IsTopologicalAddGroup (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.instIsTopologicalAddGroup σ F _

Premises used: UniformConvergenceCLM.instIsTopologicalAddGroup, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : RingHomSurjective σ
inst_12 : RingHomIsometric σ
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜₂ F
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.continuousSMul σ F { S | IsVonNBounded 𝕜₁ S } fun _ hs => hs

Premises used: Bornology.IsVonNBounded, setOf, UniformConvergenceCLM.continuousSMul, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
⊢ IsUniformAddGroup (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.instIsUniformAddGroup σ F _

Premises used: UniformConvergenceCLM.instIsUniformAddGroup, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜₁ E
⊢ ContinuousEvalConst (E →SL[σ] F) E F

Tactic:
UniformConvergenceCLM.continuousEvalConst σ F _ Bornology.sUnion_isVonNBounded_eq_univ

Premises used: UniformConvergenceCLM.continuousEvalConst, Bornology.sUnion_isVonNBounded_eq_univ, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜₁ E
inst_14 : T2Space F
⊢ T2Space (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.t2Space σ F _ Bornology.sUnion_isVonNBounded_eq_univ

Premises used: UniformConvergenceCLM.t2Space, Bornology.sUnion_isVonNBounded_eq_univ, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_7
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
⊢ HasBasis (α := E →SL[σ] F) (𝓝 0) (fun (Si : Prod.{u_4, u_7} (Set E) ι) ↦ IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2)
    fun (Si : Prod.{u_4, u_7} (Set E) ι) ↦
    {f : E →SL[σ] F | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}

Tactic:
UniformConvergenceCLM.hasBasis_nhds_zero_of_basis σ F { S | IsVonNBounded 𝕜₁ S }
    ⟨∅, isVonNBounded_empty 𝕜₁ E⟩
    (directedOn_of_sup_mem fun _ _ => IsVonNBounded.union) h

Premises used: Bornology.isVonNBounded_empty, Bornology.IsVonNBounded, Set.Mem, setOf, directedOn_of_sup_mem, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, Exists.intro, EmptyCollection.emptyCollection, UniformConvergenceCLM, Bornology.IsVonNBounded.union
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
⊢ HasBasis (α := E →SL[σ] F) (𝓝 0)
    (fun (SV : Prod.{u_4, u_5} (Set E) (Set F)) ↦ IsVonNBounded 𝕜₁ SV.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) SV.2)
    fun (SV : Prod.{u_4, u_5} (Set E) (Set F)) ↦
    {f : E →SL[σ] F | ∀ x ∈ SV.1, Membership.mem (α := F) SV.2 ((f : (a : E) → F) x : F)}

Tactic:
ContinuousLinearMap.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets

Premises used: Set.Mem, setOf, nhds, Filter.basis_sets, ContinuousLinearMap.hasBasis_nhds_zero_of_basis, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
⊢ IsUniformEmbedding (β := E →ᵤ[{s : Set E | IsVonNBounded 𝕜₁ s}] F) fun (f : E →SL[σ] F) ↦
    (UniformOnFun.ofFun {s : Set E | IsVonNBounded 𝕜₁ s} : (a : E → F) → E →ᵤ[{s : Set E | IsVonNBounded 𝕜₁ s}] F)
      (⇑f : (a : E) → F)

Tactic:
UniformConvergenceCLM.isUniformEmbedding_coeFn ..

Premises used: UniformConvergenceCLM.isUniformEmbedding_coeFn, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
M : Type u_7
inst_11 : Monoid M
inst_12 : DistribMulAction M F
inst_13 : SMulCommClass 𝕜₂ M F
inst_14 : UniformSpace F
inst_15 : IsUniformAddGroup F
inst_16 : UniformContinuousConstSMul M F
⊢ UniformContinuousConstSMul M (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.instUniformContinuousConstSMul σ F _ _

Premises used: UniformConvergenceCLM.instUniformContinuousConstSMul, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
M : Type u_7
inst_11 : Monoid M
inst_12 : DistribMulAction M F
inst_13 : SMulCommClass 𝕜₂ M F
inst_14 : TopologicalSpace F
inst_15 : IsTopologicalAddGroup F
inst_16 : ContinuousConstSMul M F
⊢ ContinuousConstSMul M (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.instContinuousConstSMul σ F _ _

Premises used: UniformConvergenceCLM.instContinuousConstSMul, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_7
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
⊢ Eq (α := Filter (E →SL[σ] F)) (𝓝 0)
    (⨅ (s : Set E),
      ⨅ (_ : IsVonNBounded 𝕜₁ s), ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : E →SL[σ] F | MapsTo (⇑f : (a : E) → F) s (b i)})

Tactic:
UniformConvergenceCLM.nhds_zero_eq_of_basis _ _ _ h

Premises used: Bornology.IsVonNBounded, Set.Mem, setOf, UniformConvergenceCLM, UniformConvergenceCLM.nhds_zero_eq_of_basis
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
⊢ Eq (α := Filter (E →SL[σ] F)) (𝓝 0)
    (⨅ (s : Set E),
      ⨅ (_ : IsVonNBounded 𝕜₁ s),
        ⨅ (U : Set F),
          ⨅ (_ : Membership.mem (γ := Filter F) (𝓝 0) U), 𝓟 {f : E →SL[σ] F | MapsTo (⇑f : (a : E) → F) s U})

Tactic:
UniformConvergenceCLM.nhds_zero_eq ..

Premises used: Bornology.IsVonNBounded, Set.Mem, setOf, UniformConvergenceCLM.nhds_zero_eq, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
s : Set E
hs : IsVonNBounded 𝕜₁ s
U : Set F
hu : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ ∀ᶠ (f : E →SL[σ] F) in 𝓝 0, MapsTo (⇑f : (a : E) → F) s U

Tactic:
UniformConvergenceCLM.eventually_nhds_zero_mapsTo _ hs hu

Premises used: UniformConvergenceCLM.eventually_nhds_zero_mapsTo, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
R : Type u_7
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
S : Set (E →SL[σ] F)
hS : IsVonNBounded R S
s : Set E
hs : IsVonNBounded 𝕜₁ s
⊢ IsVonNBounded.{u_7, u_5} R (E := F) (image2 (fun (f : E →SL[σ] F) (x : E) ↦ (f : (a : E) → F) x) S s)

Tactic:
UniformConvergenceCLM.isVonNBounded_image2_apply hS hs

Premises used: UniformConvergenceCLM.isVonNBounded_image2_apply, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
R : Type u_7
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
S : Set (E →SL[σ] F)
⊢ IsVonNBounded R S ↔
    ∀ (s : Set E),
      IsVonNBounded 𝕜₁ s →
        IsVonNBounded.{u_7, u_5} R (E := F) (image2 (fun (f : E →SL[σ] F) (x : E) ↦ (f : (a : E) → F) x) S s)

Tactic:
UniformConvergenceCLM.isVonNBounded_iff

Premises used: Bornology.IsVonNBounded, Set.Mem, setOf, UniformConvergenceCLM, UniformConvergenceCLM.isVonNBounded_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
inst_11 : ContinuousSMul 𝕜₁ E
h : IsCoherentWith.{u_4} (X := E) {s : Set E | IsVonNBounded 𝕜₁ s}
⊢ CompleteSpace (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.completeSpace _ _ h sUnion_isVonNBounded_eq_univ

Premises used: UniformConvergenceCLM.completeSpace, Bornology.sUnion_isVonNBounded_eq_univ, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : IsTopologicalAddGroup E
inst_12 : ContinuousSMul 𝕜₁ E
inst_13 : SequentialSpace E
inst_14 : UniformSpace F
inst_15 : IsUniformAddGroup F
inst_16 : ContinuousSMul 𝕜₂ F
inst_17 : CompleteSpace F
⊢ CompleteSpace (E →SL[σ] F)

Tactic:
completeSpace <| .of_seq fun _ _ h ↦ (h.isVonNBounded_range 𝕜₁).insert _

Premises used: ContinuousLinearMap.completeSpace, Filter.Tendsto.isVonNBounded_range, Bornology.IsVonNBounded.insert, Topology.IsCoherentWith.of_seq
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : UniformSpace G
inst_14 : IsUniformAddGroup G
f : F →SL[τ] G
hf : IsUniformInducing.{u_5, u_6} (α := F) (β := G) (⇑f : (a : F) → G)
⊢ IsUniformInducing (α := E →SL[σ] F) f.comp

Tactic:
UniformConvergenceCLM.isUniformInducing_postcomp _ f hf _

Premises used: UniformConvergenceCLM, UniformConvergenceCLM.isUniformInducing_postcomp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : UniformSpace G
inst_14 : IsUniformAddGroup G
f : F →SL[τ] G
hf : IsUniformEmbedding.{u_5, u_6} (α := F) (β := G) (⇑f : (a : F) → G)
⊢ IsUniformEmbedding (α := E →SL[σ] F) f.comp

Tactic:
UniformConvergenceCLM.isUniformEmbedding_postcomp _ f hf _

Premises used: UniformConvergenceCLM.isUniformEmbedding_postcomp, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup F
inst_14 : IsTopologicalAddGroup G
f : F →SL[τ] G
hf : IsInducing.{u_5, u_6} (X := F) (Y := G) (⇑f : (a : F) → G)
⊢ IsInducing (X := E →SL[σ] F) f.comp

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  letI : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
  haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
  (isUniformInducing_postcomp f <| AddMonoidHom.isUniformInducing_of_isInducing hf).isInducing

Premises used: AddMonoidHom.isUniformInducing_of_isInducing, IsUniformInducing.isInducing, ContinuousLinearMap.isUniformInducing_postcomp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup F
inst_14 : IsTopologicalAddGroup G
f : F →SL[τ] G
hf : IsEmbedding.{u_5, u_6} (X := F) (Y := G) (⇑f : (a : F) → G)
⊢ IsEmbedding (X := E →SL[σ] F) f.comp

Tactic:
.mk (isInducing_postcomp f hf.isInducing) fun _ _ ↦ f.cancel_left hf.injective

Premises used: Topology.IsEmbedding.isInducing, ContinuousLinearMap.isInducing_postcomp, Topology.IsEmbedding.injective, ContinuousLinearMap.cancel_left, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
𝔖 : Set (Set E)
h : 𝔖 ⊆ {S : Set E | IsVonNBounded 𝕜₁ S}
⊢ Continuous[topologicalSpace, UniformConvergenceCLM.instTopologicalSpace σ F 𝔖]
    (⇑(toUniformConvergenceCLM σ F 𝔖) : (a : E →SL[σ] F) → UniformConvergenceCLM σ F 𝔖)

Tactic:
continuous_id_of_le <| UniformConvergenceCLM.topologicalSpace_mono _ _ h

Premises used: UniformConvergenceCLM.topologicalSpace_mono, continuous_id_of_le, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₂
inst_1 : NormedField 𝕜₃
E : Type u_4
F : Type u_5
G : Type u_6
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
inst_5 : AddCommGroup G
inst_6 : Module 𝕜₃ G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
𝕜₁ : Type u_7
inst_10 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_11 : Module 𝕜₁ E
τ : 𝕜₃ →+* 𝕜₂
inst_12 : RingHomSurjective τ
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜₃ G
inst_15 : IsTopologicalAddGroup F
inst_16 : ContinuousConstSMul 𝕜₂ F
B : G →ₛₗ[τ] E →SL[σ] F
hB :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : G × E) ↦
    (((B : (a : G) → E →SL[σ] F) p.1 : E →SL[σ] F) : (a : E) → F) p.2
⊢ Continuous[inst_9, topologicalSpace] (⇑B : (a : G) → E →SL[σ] F)

Tactic:
UniformConvergenceCLM.continuous_of_continuous_uncurry (fun _ ↦ id) B hB

Premises used: UniformConvergenceCLM.continuous_of_continuous_uncurry, Bornology.IsVonNBounded, setOf, id, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
rw :
  (HAdd.hAdd (α := F →SL[σ₂₃] G) (β := F →SL[σ₂₃] G) ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G)
          ((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) :
        (a : F) → G)
      y =
    HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
rw₁ rw₂ :
  HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
    HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (x + x') : F →SL[σ₂₃] G) : (a : F) → G) y =
    HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)

Tactic:
rw [f.map_add, add_apply]

Premises used: ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
y : F
rw : Eq.{u_7 + 1} (α := G) ((0 : (a : F) → G) y : G) (0 : G)
rw₁ rw₂ : Eq.{u_7 + 1} (α := G) 0 0
⊢ Eq.{u_7 + 1} (α := G) (((f : (a : E) → F →SL[σ₂₃] G) 0 : (a : F) → G) y : G) (0 : G)

Tactic:
rw [f.map_zero, zero_apply]

Premises used: ContinuousLinearMap.map_zero, ContinuousLinearMap.zero_apply