awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
h₁ :
  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:
use s, C
-- 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
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)
h₁ :
  Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
    s.sup (HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F))
⊢ Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
    HSMul.hSMul (β := Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (s.sup (PointwiseConvergenceCLM.seminormFamily σ E F))

Tactic:
rw [← Seminorm.finset_sup_smul]

Premises used: Seminorm.finset_sup_smul
-- 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
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)
B : E →SLₚₜ[σ] F
h₁ :
  ∀ (g : E) (h₁ : g ∈ s)
    (h₂ :
      norm.{u_9} (E := G)
          ((((A : (a : E →SL[σ] F) → D →SL[τ] G)
                    ((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                        (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                      B) :
                  D →SL[τ] G) :
                (a : D) → G)
              f :
            G) ≤
        C •
          norm.{u_8} (E := F)
            ((((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                        (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                      B :
                    E →SL[σ] F) :
                  (a : E) → F)
                g :
              F)),
    LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
      ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
        (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B)
      ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
        (s.sup (HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F))) B)
⊢ LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
      (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
      (s.sup (HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F))) B)

Tactic:
obtain ⟨g, h₁, h₂⟩ := h ((toUniformConvergenceCLM _ _ _).symm B)

Premises used: LinearEquiv.symm, ContinuousLinearMap.toUniformConvergenceCLM, DFunLike.coe
-- 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
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)
B : E →SLₚₜ[σ] F
g : E
h₁ : g ∈ s
h₂ :
  norm.{u_9} (E := G)
      ((((A : (a : E →SL[σ] F) → D →SL[τ] G)
                ((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B) :
              D →SL[τ] G) :
            (a : D) → G)
          f :
        G) ≤
    C •
      norm.{u_8} (E := F)
        ((((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B :
                E →SL[σ] F) :
              (a : E) → F)
            g :
          F)
⊢ LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
      (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
      (s.sup (HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F))) B)

Tactic:
le_trans ?_ (Seminorm.le_finset_sup_apply h₁)

Premises used: Seminorm.le_finset_sup_apply, le_trans
-- 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
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)
B : E →SLₚₜ[σ] F
g : E
h₁ : g ∈ s
h₂ :
  norm.{u_9} (E := G)
      ((((A : (a : E →SL[σ] F) → D →SL[τ] G)
                ((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B) :
              D →SL[τ] G) :
            (a : D) → G)
          f :
        G) ≤
    C •
      norm.{u_8} (E := F)
        ((((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B :
                E →SL[σ] F) :
              (a : E) → F)
            g :
          F)
h₃ :
  LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
        (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B :
      ℝ)
    ((HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F) g :
          (a : E →SLₚₜ[σ] F) → ℝ)
        B :
      ℝ)
⊢ LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
      (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
      (s.sup (HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F))) B)

Tactic:
refine le_trans ?_ (Seminorm.le_finset_sup_apply h₁)

Premises used: Seminorm.le_finset_sup_apply, le_trans
-- 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
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)
B : E →SLₚₜ[σ] F
g : E
h₁ : g ∈ s
h₂ :
  norm.{u_9} (E := G)
      ((((A : (a : E →SL[σ] F) → D →SL[τ] G)
                ((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B) :
              D →SL[τ] G) :
            (a : D) → G)
          f :
        G) ≤
    C •
      norm.{u_8} (E := F)
        ((((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B :
                E →SL[σ] F) :
              (a : E) → F)
            g :
          F)
⊢ LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
        (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B :
      ℝ)
    ((HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F) g :
          (a : E →SLₚₜ[σ] F) → ℝ)
        B :
      ℝ)

Tactic:
h₂
-- 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
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)
B : E →SLₚₜ[σ] F
g : E
h₁ : g ∈ s
h₂ :
  norm.{u_9} (E := G)
      ((((A : (a : E →SL[σ] F) → D →SL[τ] G)
                ((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B) :
              D →SL[τ] G) :
            (a : D) → G)
          f :
        G) ≤
    C •
      norm.{u_8} (E := F)
        ((((LinearEquiv.symm (toUniformConvergenceCLM σ F {s : Set E | Finite.{u_7 + 1} (↑s : Type u_7)}) :
                    (a : UniformConvergenceCLM σ F {s : Set E | Finite (↑s : Type u_7)}) → E →SL[σ] F)
                  B :
                E →SL[σ] F) :
              (a : E) → F)
            g :
          F)
⊢ LE.le (α := (fun (a : E →SLₚₜ[σ] F) ↦ ℝ) B)
    ((fun (f : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) ↦ ((⇑f : (a : E →SLₚₜ[σ] F) → ℝ) : (a : E →SLₚₜ[σ] F) → ℝ))
        (Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A) B :
      ℝ)
    ((HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F) g :
          (a : E →SLₚₜ[σ] F) → ℝ)
        B :
      ℝ)

Tactic:
exact h₂
-- 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 : AddCommGroup F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : Module 𝕜₂ F
inst_10 : Semiring R
inst_11 : PartialOrder R
inst_12 : Module R F
inst_13 : ContinuousConstSMul R F
inst_14 : LocallyConvexSpace R F
inst_15 : SMulCommClass 𝕜₂ R F
⊢ LocallyConvexSpace R (E →SLₚₜ[σ] F)

Tactic:
UniformConvergenceCLM.locallyConvexSpace R {(s : Set E) | Set.Finite s} ⟨∅, Set.finite_empty⟩
    (directedOn_of_sup_mem fun _ _ => Set.Finite.union)

Premises used: Set.Finite.union, Set.finite_empty, setOf, Set.Finite, directedOn_of_sup_mem, _private.0.PointwiseConvergenceCLM.instLocallyConvexSpace.match_1, Exists.intro, EmptyCollection.emptyCollection, UniformConvergenceCLM.locallyConvexSpace
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
y : F
⊢ y ∈ B.polar s ↔ ∀ x ∈ s, norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LinearMap.polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
y : F
hy : y ∈ B.polar s
⊢ ∀ x ∈ s, norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
hy

Premises used: Set.Mem, setOf, LinearMap.polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar s =
    ⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1)

Tactic:
aesop
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
rw :
  IsClosed[WeakBilin.instTopologicalSpace B.flip]
    (⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1))
⊢ IsClosed[WeakBilin.instTopologicalSpace B.flip] (B.polar s)

Tactic:
rw [polar_eq_biInter_preimage]

Premises used: LinearMap.polar_eq_biInter_preimage
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed[WeakBilin.instTopologicalSpace B.flip]
    (⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1))

Tactic:
isClosed_biInter
    fun _ _ ↦ Metric.isClosed_closedBall.preimage (WeakBilin.eval_continuous B.flip _)

Premises used: isClosed_biInter, Metric.isClosed_closedBall, WeakBilin, LinearMap.flip, WeakBilin.eval_continuous, IsClosed.preimage
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed[WeakBilin.instTopologicalSpace B.flip]
    (⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1))

Tactic:
exact isClosed_biInter
    fun _ _ ↦ Metric.isClosed_closedBall.preimage (WeakBilin.eval_continuous B.flip _)

Premises used: isClosed_biInter, Metric.isClosed_closedBall, LinearMap.flip, WeakBilin.eval_continuous, IsClosed.preimage
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
h : x ∈ s
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) 0 : 𝕜) ≤ 1

Tactic:
simp only [map_zero, norm_zero, zero_le_one]

Premises used: norm_zero, map_zero, zero_le_one
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
h : 0 ∈ B.polar s
⊢ (B.polar s).Nonempty

Tactic:
use 0
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ 0 ∈ B.polar s

Tactic:
zero_mem_polar B s

Premises used: LinearMap.zero_mem_polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ 0 ∈ B.polar s

Tactic:
exact zero_mem_polar B s

Premises used: LinearMap.zero_mem_polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
h :
  ∀ (x : F),
    x ∈ B.polar s ↔
      Membership.mem (γ := Set F)
        (⋂ x ∈ s, {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1}) x
⊢ B.polar s =
    ⋂ x ∈ s, {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1}

Tactic:
ext
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
⊢ x ∈ B.polar s ↔
    Membership.mem (γ := Set F)
      (⋂ x ∈ s, {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1}) x

Tactic:
simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.mem_iInter, LinearMap.polar_mem_iff
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ GaloisConnection (β := (Set F)ᵒᵈ) ((⇑OrderDual.toDual : (a : Set F) → (Set F)ᵒᵈ) ∘ B.polar)
    (B.flip.polar ∘ (⇑OrderDual.ofDual : (a : (Set F)ᵒᵈ) → Set F))

Tactic:
fun _ _ =>
  ⟨fun h _ hx _ hy => h hy _ hx, fun h _ hx _ hy => h hy _ hx⟩

Premises used: Iff.intro, GaloisConnection
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
ι : Sort u_4
s : ι → Set E
⊢ B.polar (⋃ (i : ι), s i) = ⋂ (i : ι), B.polar (s i)

Tactic:
B.polar_gc.l_iSup

Premises used: iInf, Set.Mem, Set.iInter, setOf, LinearMap.polar, LinearMap.polar_gc, GaloisConnection.l_iSup, OrderDual, Set.iUnion
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s t : Set E
⊢ B.polar (s ∪ t) = B.polar s ∩ B.polar t

Tactic:
B.polar_gc.l_sup

Premises used: Set.Mem, setOf, LinearMap.polar, LinearMap.polar_gc, OrderDual, GaloisConnection.l_sup