awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
simp :
  ∀ (s : Set (E →SL_c[σ] F)),
    IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}] s →
      IsOpen[topologicalSpace]
        ((⇑(LinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SL_c[σ] F) :
            (a : E →SL[σ] F) → E →SL_c[σ] F) ⁻¹'
          s)
⊢ Continuous[topologicalSpace, UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}]
    (AddHom.toFun
      (LinearMap.toAddHom
        ((↑(LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL[σ] F) →ₗ[𝕜₂] E →SL_c[σ] F) :
          (E →SL[σ] F) →ₗ[𝕜₂] E →SL_c[σ] F)))

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, continuous_def]

Premises used: AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, continuous_def, LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}] s
apply :
  LE.le (α := TopologicalSpace (E →SL_c[σ] F)) topologicalSpace
    (UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S})
⊢ IsOpen[topologicalSpace]
    ((⇑(LinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SL_c[σ] F) :
        (a : E →SL[σ] F) → E →SL_c[σ] F) ⁻¹'
      s)

Tactic:
apply hs.mono

Premises used: IsOpen.mono
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}] s
h : Subset.{u_3} (α := Set (Set E)) {S : Set E | IsCompact S} {S : Set E | IsVonNBounded 𝕜₁ S}
⊢ LE.le (α := TopologicalSpace (E →SL_c[σ] F)) topologicalSpace
    (UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S})

Tactic:
apply UniformConvergenceCLM.topologicalSpace_mono

Premises used: UniformConvergenceCLM.topologicalSpace_mono
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}] s
x : Set E
hx : Membership.mem (γ := Set (Set E)) {S : Set E | IsCompact S} x
⊢ Membership.mem (γ := Set (Set E)) {S : Set E | IsVonNBounded 𝕜₁ S} x

Tactic:
hx.isVonNBounded 𝕜₁

Premises used: Bornology.IsVonNBounded, Set.Mem, setOf, IsCompact.isVonNBounded
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}] s
x : Set E
hx : Membership.mem (γ := Set (Set E)) {S : Set E | IsCompact S} x
⊢ Membership.mem (γ := Set (Set E)) {S : Set E | IsVonNBounded 𝕜₁ S} x

Tactic:
exact hx.isVonNBounded 𝕜₁

Premises used: IsCompact.isVonNBounded
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
apply :
  ContinuousAt (X := E →SL_c[σ] F) (Y := E →SL[σ] F)
    (⇑(LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
      (a : E →SL_c[σ] F) → E →SL[σ] F)
    0
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}, topologicalSpace]
    (LinearEquiv.invFun (LinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SL_c[σ] F))

Tactic:
apply continuous_of_continuousAt_zero (LinearEquiv.toCompactConvergenceCLM σ E F).symm

Premises used: LinearEquiv.symm, continuous_of_continuousAt_zero, _private.0.LinearEquiv.toCompactConvergenceCLM
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
rw :
  ∀ (ib : Prod.{u_3, u_4} (Set E) (Set F)),
    IsVonNBounded 𝕜₁ ib.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ib.2 →
      ∃ (ia : Prod.{u_3, u_4} (Set E) (Set F)),
        (IsCompact ia.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ia.2) ∧
          ∀ (x : E →SL_c[σ] F),
            Membership.mem (γ := Set (E →SL_c[σ] F))
                {f : E →SL_c[σ] F | ∀ x ∈ ia.1, Membership.mem (α := F) ia.2 ((f : (a : E) → F) x : F)} x →
              Membership.mem (α := E →SL[σ] F) (γ := Set (E →SL[σ] F))
                {f : E →SL[σ] F | ∀ x ∈ ib.1, Membership.mem (α := F) ib.2 ((f : (a : E) → F) x : F)}
                (((LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
                      (a : E →SL_c[σ] F) → E →SL[σ] F)
                    x :
                  E →SL[σ] F)
⊢ ContinuousAt (X := E →SL_c[σ] F) (Y := E →SL[σ] F)
    (⇑(LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
      (a : E →SL_c[σ] F) → E →SL[σ] F)
    0

Tactic:
rw [ContinuousAt, _root_.map_zero, CompactConvergenceCLM.hasBasis_nhds_zero.tendsto_iff
      ContinuousLinearMap.hasBasis_nhds_zero]

Premises used: ContinuousLinearMap.hasBasis_nhds_zero, Filter.HasBasis.tendsto_iff, ContinuousAt, map_zero, CompactConvergenceCLM.hasBasis_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
a : Set E
b : Set F
ha : IsVonNBounded 𝕜₁ (a, b).1
hb : Membership.mem (γ := Filter F) (𝓝 0) (a, b).2
h :
  (IsCompact (closure[inst_4] a, b).1 ∧ Membership.mem (γ := Filter F) (𝓝 0) (closure[inst_4] a, b).2) ∧
    ∀ (x : E →SL_c[σ] F),
      Membership.mem (γ := Set (E →SL_c[σ] F))
          {f : E →SL_c[σ] F |
            ∀ x ∈ (closure[inst_4] a, b).1, Membership.mem (α := F) (closure[inst_4] a, b).2 ((f : (a : E) → F) x : F)}
          x →
        Membership.mem (α := E →SL[σ] F) (γ := Set (E →SL[σ] F))
          {f : E →SL[σ] F | ∀ x ∈ (a, b).1, Membership.mem (α := F) (a, b).2 ((f : (a : E) → F) x : F)}
          (((LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
                (a : E →SL_c[σ] F) → E →SL[σ] F)
              x :
            E →SL[σ] F)
⊢ ∃ (ia : Prod.{u_3, u_4} (Set E) (Set F)),
    (IsCompact ia.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ia.2) ∧
      ∀ (x : E →SL_c[σ] F),
        Membership.mem (γ := Set (E →SL_c[σ] F))
            {f : E →SL_c[σ] F | ∀ x ∈ ia.1, Membership.mem (α := F) ia.2 ((f : (a : E) → F) x : F)} x →
          Membership.mem (α := E →SL[σ] F) (γ := Set (E →SL[σ] F))
            {f : E →SL[σ] F | ∀ x ∈ (a, b).1, Membership.mem (α := F) (a, b).2 ((f : (a : E) → F) x : F)}
            (((LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
                  (a : E →SL_c[σ] F) → E →SL[σ] F)
                x :
              E →SL[σ] F)

Tactic:
use ⟨closure a, b⟩
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
a : Set E
b : Set F
ha : IsVonNBounded 𝕜₁ (a, b).1
hb : Membership.mem (γ := Filter F) (𝓝 0) (a, b).2
⊢ (IsCompact (closure[inst_4] a, b).1 ∧ Membership.mem (γ := Filter F) (𝓝 0) (closure[inst_4] a, b).2) ∧
    ∀ (x : E →SL_c[σ] F),
      Membership.mem (γ := Set (E →SL_c[σ] F))
          {f : E →SL_c[σ] F |
            ∀ x ∈ (closure[inst_4] a, b).1, Membership.mem (α := F) (closure[inst_4] a, b).2 ((f : (a : E) → F) x : F)}
          x →
        Membership.mem (α := E →SL[σ] F) (γ := Set (E →SL[σ] F))
          {f : E →SL[σ] F | ∀ x ∈ (a, b).1, Membership.mem (α := F) (a, b).2 ((f : (a : E) → F) x : F)}
          (((LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
                (a : E →SL_c[σ] F) → E →SL[σ] F)
              x :
            E →SL[σ] F)

Tactic:
⟨⟨MontelSpace.isCompact_of_isClosed_of_isVonNBounded 𝕜₁ isClosed_closure
      ha.closure, hb⟩, fun _ hf _ hx ↦ hf _ (subset_closure hx)⟩

Premises used: MontelSpace.isCompact_of_isClosed_of_isVonNBounded, subset_closure, And.intro, Bornology.IsVonNBounded.closure, isClosed_closure
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
a : Set E
b : Set F
ha : IsVonNBounded 𝕜₁ (a, b).1
hb : Membership.mem (γ := Filter F) (𝓝 0) (a, b).2
⊢ (IsCompact (closure[inst_4] a, b).1 ∧ Membership.mem (γ := Filter F) (𝓝 0) (closure[inst_4] a, b).2) ∧
    ∀ (x : E →SL_c[σ] F),
      Membership.mem (γ := Set (E →SL_c[σ] F))
          {f : E →SL_c[σ] F |
            ∀ x ∈ (closure[inst_4] a, b).1, Membership.mem (α := F) (closure[inst_4] a, b).2 ((f : (a : E) → F) x : F)}
          x →
        Membership.mem (α := E →SL[σ] F) (γ := Set (E →SL[σ] F))
          {f : E →SL[σ] F | ∀ x ∈ (a, b).1, Membership.mem (α := F) (a, b).2 ((f : (a : E) → F) x : F)}
          (((LinearEquiv.symm (LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL_c[σ] F) ≃ₗ[𝕜₂] E →SL[σ] F) :
                (a : E →SL_c[σ] F) → E →SL[σ] F)
              x :
            E →SL[σ] F)

Tactic:
exact ⟨⟨MontelSpace.isCompact_of_isClosed_of_isVonNBounded 𝕜₁ isClosed_closure
      ha.closure, hb⟩, fun _ hf _ hx ↦ hf _ (subset_closure hx)⟩
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
f : E →SL[σ] F
x : E
⊢ Eq.{u_4 + 1} (α := F)
    (((((ContinuousLinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃L[𝕜₂] E →SL_c[σ] F) :
                (a : E →SL[σ] F) → E →SL_c[σ] F)
              f :
            E →SL_c[σ] F) :
          (a : E) → F)
        x :
      F)
    ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.Montel
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 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
f : E →SL_c[σ] F
x : E
⊢ Eq.{u_4 + 1} (α := F)
    (((((ContinuousLinearEquiv.symm (ContinuousLinearEquiv.toCompactConvergenceCLM σ E F) :
                  (E →SL_c[σ] F) ≃L[𝕜₂] E →SL[σ] F) :
                (a : E →SL_c[σ] F) → E →SL[σ] F)
              f :
            E →SL[σ] F) :
          (a : E) → F)
        x :
      F)
    ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜₁ E
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜₂ F
x : E
⊢ norm.{u_8} (E := F) ((0 : (a : E) → F) x : F) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜₁ E
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜₂ F
x : E
A B : E →SLₚₜ[σ] F
⊢ norm.{u_8} (E := F) ((A + B : (a : E) → F) x : F) ≤
    norm.{u_8} (E := F) ((A : (a : E) → F) x : F) + norm.{u_8} (E := F) ((B : (a : E) → F) x : F)

Tactic:
simpa only using norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜₁ E
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜₂ F
x : E
A : E →SLₚₜ[σ] F
⊢ norm.{u_8} (E := F) ((-A : (a : E) → F) x : F) = norm.{u_8} (E := F) ((A : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜₁ E
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜₂ F
x : E
r : 𝕜₂
A : E →SLₚₜ[σ] F
⊢ norm.{u_8} (E := F) ((r • A : (a : E) → F) x : F) = ‖r‖ * norm.{u_8} (E := F) ((A : (a : E) → F) x : F)

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜₂ F
⊢ Topology.IsInducing (X := E →SLₚₜ[σ] F) (Y := E → F) (⇑(inducingFn σ E F) : (a : E →SLₚₜ[σ] F) → E → F)

Tactic:
(PointwiseConvergenceCLM.isEmbedding_coeFn σ E F).isInducing

Premises used: PointwiseConvergenceCLM.isEmbedding_coeFn, Topology.IsEmbedding.isInducing, UniformConvergenceCLM
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜₂ F
⊢ WithSeminorms (E := E →SLₚₜ[σ] F) (PointwiseConvergenceCLM.seminormFamily σ E F)

Tactic:
let e : E ≃ (Σ _ : E, Fin 1) := .symm <| .sigmaUnique _ _
  (isInducing_inducingFn σ E F).withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜₂ F)
    |>.congr_equiv e

Premises used: PointwiseConvergenceCLM.isInducing_inducingFn, SeminormFamily.comp, PointwiseConvergenceCLM.seminorm, WithSeminorms.congr_equiv, Topology.IsInducing.withSeminorms, withSeminorms_pi, norm_withSeminorms, Seminorm.comp, Equiv.symm, OfNat.ofNat, Fin, Equiv.sigmaUnique
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
𝕜₁ : Type u_3
𝕜₂ : Type u_4
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜₂ F
f : Filter α
u : α → E →SLₚₜ[σ] F
y₀ : E →SLₚₜ[σ] F
⊢ Tendsto u f (𝓝 y₀) ↔
    ∀ (x : E) (ε : ℝ),
      0 < ε → ∀ᶠ (k : α) in f, ‖HSub.hSub (α := F) (β := F) ((u k : (a : E) → F) x : F) ((y₀ : (a : E) → F) x : F)‖ < ε

Tactic:
PointwiseConvergenceCLM.withSeminorms.tendsto_nhds _ _

Premises used: WithSeminorms.tendsto_nhds, PointwiseConvergenceCLM.withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
𝕜₁ : Type u_3
𝕜₂ : Type u_4
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜₂ F
inst_7 : SemilatticeSup α
inst_8 : Nonempty α
u : α → E →SLₚₜ[σ] F
y₀ : E →SLₚₜ[σ] F
⊢ Tendsto u atTop (𝓝 y₀) ↔
    ∀ (x : E) (ε : ℝ),
      0 < ε →
        ∃ (k₀ : α),
          ∀ (k : α), k₀ ≤ k → ‖HSub.hSub (α := F) (β := F) ((u k : (a : E) → F) x : F) ((y₀ : (a : E) → F) x : F)‖ < ε

Tactic:
PointwiseConvergenceCLM.withSeminorms.tendsto_nhds_atTop _ _

Premises used: WithSeminorms.tendsto_nhds_atTop, PointwiseConvergenceCLM.withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜₁ E
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜₂ F
inst_8 : AddCommGroup D
inst_9 : TopologicalSpace D
inst_10 : Module 𝕜₃ D
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace 𝕜₂ G
A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G
hbound :
  ∀ (f : D),
    ∃ (s : Finset E) (C : ℝ≥0),
      ∀ (B : E →SL[σ] F),
        ∃ (g : E) (_ : g ∈ s),
          norm.{u_9} (E := G) ((((A : (a : E →SL[σ] F) → D →SL[τ] G) B : D →SL[τ] G) : (a : D) → G) f : G) ≤
            C • norm.{u_8} (E := F) ((B : (a : E) → F) g : F)
apply :
  Seminorm.IsBounded (PointwiseConvergenceCLM.seminormFamily σ E F) (PointwiseConvergenceCLM.seminormFamily τ D G) A
⊢ Continuous (X := E →SLₚₜ[σ] F) (Y := D →SLₚₜ[τ] G)
    (AddHom.toFun
      (LinearMap.toAddHom
        ((↑(toUniformConvergenceCLM τ G {s : Set D | Finite.{u_6 + 1} (↑s : Type u_6)}) :
            (D →SL[τ] G) →ₗ[𝕜₂] UniformConvergenceCLM τ G {s : Set D | Finite (↑s : Type u_6)}) ∘ₗ
          A ∘ₗ
            (↑(LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)})) :
              UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)} →ₗ[𝕜₂] E →SL[σ] F))))

Tactic:
apply PointwiseConvergenceCLM.withSeminorms.continuous_of_isBounded
      PointwiseConvergenceCLM.withSeminorms A

Premises used: WithSeminorms.continuous_of_isBounded, PointwiseConvergenceCLM.withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence
Goal:
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜₁ E
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜₂ F
inst_8 : AddCommGroup D
inst_9 : TopologicalSpace D
inst_10 : Module 𝕜₃ D
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace 𝕜₂ G
A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G
hbound :
  ∀ (f : D),
    ∃ (s : Finset E) (C : ℝ≥0),
      ∀ (B : E →SL[σ] F),
        ∃ (g : E) (_ : g ∈ s),
          norm.{u_9} (E := G) ((((A : (a : E →SL[σ] F) → D →SL[τ] G) B : D →SL[τ] G) : (a : D) → G) f : G) ≤
            C • norm.{u_8} (E := F) ((B : (a : E) → F) g : F)
f : D
obtain :
  ∀ (s : Finset E) (C : ℝ≥0)
    (h :
      ∀ (B : E →SL[σ] F),
        ∃ (g : E) (_ : g ∈ s),
          norm.{u_9} (E := G) ((((A : (a : E →SL[σ] F) → D →SL[τ] G) B : D →SL[τ] G) : (a : D) → G) f : G) ≤
            C • norm.{u_8} (E := F) ((B : (a : E) → F) g : F)),
    ∃ (s : Finset E) (C : ℝ≥0),
      Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
        HSMul.hSMul (β := Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (s.sup (PointwiseConvergenceCLM.seminormFamily σ E F))
⊢ ∃ (s : Finset E) (C : ℝ≥0),
    Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
      HSMul.hSMul (β := Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (s.sup (PointwiseConvergenceCLM.seminormFamily σ E F))

Tactic:
obtain ⟨s, C, h⟩ := hbound f