awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Montel (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : 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
⊢ IsOpen[topologicalSpace]
    ((⇑(LinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SL_c[σ] F) :
        (a : E →SL[σ] F) → E →SL_c[σ] F) ⁻¹'
      s)
have apply : LE.le (α := TopologicalSpace (E →SL_c[σ] F)) topologicalSpace
  (UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S})
Tactic: apply hs.mono
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Montel (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : 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
⊢ LE.le (α := TopologicalSpace (E →SL_c[σ] F)) topologicalSpace
    (UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S})
have h : Subset.{u_3} (α := Set (Set E)) {S : Set E | IsCompact S} {S : Set E | IsVonNBounded 𝕜₁ S}
Tactic: apply UniformConvergenceCLM.topologicalSpace_mono
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Montel (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : 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
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}, topologicalSpace]
    (LinearEquiv.invFun (LinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SL_c[σ] F))
have 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
Tactic: apply continuous_of_continuousAt_zero (LinearEquiv.toCompactConvergenceCLM σ E F).symm
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Montel (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : 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
⊢ 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
have 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)
Tactic: rw [ContinuousAt, _root_.map_zero, CompactConvergenceCLM.hasBasis_nhds_zero.tendsto_iff
      ContinuousLinearMap.hasBasis_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Montel (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : 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
⊢ ∃ (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)
have 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)
Tactic: use ⟨closure a, b⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.PointwiseConvergence (goal)
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)
⊢ 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))))
have apply : Seminorm.IsBounded (PointwiseConvergenceCLM.seminormFamily σ E F) (PointwiseConvergenceCLM.seminormFamily τ D G) A
Tactic: apply PointwiseConvergenceCLM.withSeminorms.continuous_of_isBounded
      PointwiseConvergenceCLM.withSeminorms A
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.PointwiseConvergence (goal)
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),
    Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
      HSMul.hSMul (β := Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (s.sup (PointwiseConvergenceCLM.seminormFamily σ E F))
have 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))
Tactic: obtain ⟨s, C, h⟩ := hbound f
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.PointwiseConvergence (goal)
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)
⊢ ∃ (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))
have h₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.PointwiseConvergence (goal)
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)
⊢ Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
    HSMul.hSMul (β := Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (s.sup (PointwiseConvergenceCLM.seminormFamily σ E F))
have h₁ : Seminorm.comp (PointwiseConvergenceCLM.seminormFamily τ D G f) A ≤
  s.sup (HSMul.hSMul (β := E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)) C (PointwiseConvergenceCLM.seminormFamily σ E F))
Tactic: rw [← Seminorm.finset_sup_smul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.PointwiseConvergence (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨g, h₁, h₂⟩ := h ((toUniformConvergenceCLM _ _ _).symm B)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.PointwiseConvergence (goal)
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)
have 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 :
    ℝ)
Tactic: refine le_trans ?_ (Seminorm.le_finset_sup_apply h₁)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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] (B.polar s)
have 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))
Tactic: rw [polar_eq_biInter_preimage]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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).Nonempty
have h : 0 ∈ B.polar s
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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, {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1}
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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 →ₗ[𝕜] 𝕜
a : E
y : F
hy :
  Membership.mem (γ := Set F)
    {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1} y
x : E
hb : Membership.mem (γ := Set E) {a} x
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
have rw : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
Tactic: rw [Set.mem_singleton_iff.mp hb]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ norm.{u_1} (E := 𝕜) ((((B.flip : (a : F) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ≤ 1
have rw : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
Tactic: rw [B.flip_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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 '' {F : Set E | F.Finite ∧ F ⊆ s}) = B.polar s
have h : ∀ (x : F), x ∈ ⋂₀ (B.polar '' {F : Set E | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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 '' {F : Set E | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s
have h : (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s
Tactic: simp only [Set.sInter_image, Set.mem_setOf_eq, Set.mem_iInter, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
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
⊢ (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s
have h : ∀ (hx : ∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) (a : E) (ha : a ∈ s),
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) ≤ 1
Tactic: refine ⟨fun hx a ha ↦ ?_, fun hx F _ hF₂ => polar_antitone _ hF₂ hx⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ Eq (α := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) {0}
have rw : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) 0 ∧
  ∀ (x : F), Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) x → x = 0
Tactic: rw [Set.eq_singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) 0 ∧
    ∀ (x : F), Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) x → x = 0
have refine : ∀ (y : F) (hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y) (x : E),
  Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)
Tactic: refine ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => ?_⟩