awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
⊢ ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ ((q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F) : (a : E) → ℝ) x)

Tactic:
H k
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
⊢ ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ ((q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F) : (a : E) → ℝ) x)

Tactic:
exact H k
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
⊢ BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (i : ι) ↦ (q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F))

Tactic:
have : BddAbove (range fun i ↦ (q k).comp (𝓕 i).toLinearMap) := by
    rw [Seminorm.bddAbove_range_iff]
    exact H k
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
this : BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (i : ι) ↦ (q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F))
⊢ BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (k_1 : ι) ↦ (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous[inst_7.toTopologicalSpace, _] (⨆ (k_1 : ι), (⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)) : (a : E) → ℝ))

Tactic:
⟨this, Seminorm.continuous_iSup _
    (fun i ↦ (hq.continuous_seminorm k).comp (𝓕 i).continuous) this⟩

Premises used: Continuous.comp, WithSeminorms.continuous_seminorm, ContinuousLinearMap.continuous, Seminorm.continuous_iSup, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
this : BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (i : ι) ↦ (q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F))
⊢ BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (k_1 : ι) ↦ (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous[inst_7.toTopologicalSpace, _] (⨆ (k_1 : ι), (⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)) : (a : E) → ℝ))

Tactic:
exact ⟨this, Seminorm.continuous_iSup _
    (fun i ↦ (hq.continuous_seminorm k).comp (𝓕 i).continuous) this⟩
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
⊢ WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)

Tactic:
have hp := PolynormableSpace.withSeminorms 𝕜₂ F
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)

Tactic:
hp.banach_steinhaus ?_

Premises used: WithSeminorms.banach_steinhaus
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
refine :
  ∀ (k : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) (x : E),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ ((↑k : Seminorm 𝕜₂ F) : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)

Tactic:
refine hp.banach_steinhaus ?_

Premises used: WithSeminorms.banach_steinhaus
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
⊢ ∀ (x : E) (i : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }),
    BddAbove (α := ℝ)
      (range.{0, u_2 + 1} (ι := ι)
        (Function.comp (β := F) (⇑(↑i : Seminorm 𝕜₂ F) : (a : F) → ℝ) fun (i : ι) ↦ (𝓕 i : (a : E) → F) x))

Tactic:
simp_rw [hp.isVonNBounded_iff_seminorm_bddAbove, ← range_comp] at H

Premises used: Set.range_comp, WithSeminorms.isVonNBounded_iff_seminorm_bddAbove
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
H :
  ∀ (x : E) (i : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }),
    BddAbove (α := ℝ)
      (range.{0, u_2 + 1} (ι := ι)
        (Function.comp (β := F) (⇑(↑i : Seminorm 𝕜₂ F) : (a : F) → ℝ) fun (i : ι) ↦ (𝓕 i : (a : E) → F) x))
⊢ ∀ (k : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) (x : E),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ ((↑k : Seminorm 𝕜₂ F) : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))

Tactic:
fun q x ↦ H x q
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
H :
  ∀ (x : E) (i : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }),
    BddAbove (α := ℝ)
      (range.{0, u_2 + 1} (ι := ι)
        (Function.comp (β := F) (⇑(↑i : Seminorm 𝕜₂ F) : (a : F) → ℝ) fun (i : ι) ↦ (𝓕 i : (a : E) → F) x))
⊢ ∀ (k : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) (x : E),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ ((↑k : Seminorm 𝕜₂ F) : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))

Tactic:
exact fun q x ↦ H x q
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
rcases :
  ∀ (u : ℕ → α) (hu : Tendsto u atTop l),
    Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
      (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun
⊢ Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
    (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun

Tactic:
rcases l.exists_seq_tendsto with ⟨u, hu⟩

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
⊢ Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
    (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun

Tactic:
(h.comp hu).continuous_of_equicontinuous
      (PolynormableSpace.banach_steinhaus ?_).equicontinuous

Premises used: UniformEquicontinuous.equicontinuous, PolynormableSpace.banach_steinhaus, Filter.Tendsto.continuous_of_equicontinuous, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
refine : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)
⊢ Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
    (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun

Tactic:
refine (h.comp hu).continuous_of_equicontinuous
      (PolynormableSpace.banach_steinhaus ?_).equicontinuous

Premises used: UniformEquicontinuous.equicontinuous, PolynormableSpace.banach_steinhaus, Filter.Tendsto.continuous_of_equicontinuous, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
x : E
rw :
  ∀ (h : ∀ (x : E), Tendsto (fun (i : α) ↦ (g i : (a : E) → F) x) l (𝓝 (f x))) (u : ℕ → α) (hu : Tendsto u atTop l)
    (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)
⊢ IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)

Tactic:
rw [tendsto_pi_nhds] at h

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h_1 : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
h : ∀ (x : E), Tendsto (fun (i : α) ↦ (g i : (a : E) → F) x) l (𝓝 (f x))
__LinearMap : E →ₛₗ[σ₁₂] F := linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h_1
u : ℕ → α
hu : Tendsto u atTop l
x : E
⊢ IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)

Tactic:
((h x).comp hu).isVonNBounded_range 𝕜₂

Premises used: Filter.Tendsto.isVonNBounded_range, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h_1 : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
h : ∀ (x : E), Tendsto (fun (i : α) ↦ (g i : (a : E) → F) x) l (𝓝 (f x))
__LinearMap : E →ₛₗ[σ₁₂] F := linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h_1
u : ℕ → α
hu : Tendsto u atTop l
x : E
⊢ IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)

Tactic:
exact ((h x).comp hu).isVonNBounded_range 𝕜₂

Premises used: Filter.Tendsto.isVonNBounded_range, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
A B : Set E
simp :
  (∃ (i : ℝ), ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Ici i) x → B ⊆ x • A) ↔
    ∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
⊢ (∃ (i : ℝ), True ∧ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Ici i) x → B ⊆ x • A) ↔
    ∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
A B : Set E
⊢ (∃ (i : ℝ), ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Ici i) x → B ⊆ x • A) ↔
    ∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
A B : Set E
h : Absorbs 𝕜 A B
⊢ ∃ r > 0, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Tactic:
let ⟨r, hr₁, hr⟩ := (Filter.atTop_basis' 1).cobounded_of_norm.eventually_iff.1 h
  ⟨r, one_pos.trans_le hr₁, hr⟩

Premises used: Exists, GT.gt, And, Filter.HasBasis.cobounded_of_norm, LT.lt.trans_le, And.intro, Exists.intro, Iff.mp, Filter.HasBasis.eventually_iff, Filter.atTop_basis', OfNat.ofNat, one_pos, _private.0.Absorbs.exists_pos.match_1
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
⊢ Balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s

Tactic:
forall₂_congr fun _a _ha => smul_set_subset_iff

Premises used: forall₂_congr, Balanced, Set.smul_set_subset_iff
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
⊢ Balanced 𝕜 s ↔ HSMul.hSMul.{u_1, u_3, u_3} (α := Set 𝕜) (Metric.closedBall 0 1) s ⊆ s

Tactic:
simp [balanced_iff_smul_mem, smul_subset_iff]

Premises used: balanced_iff_smul_mem, Set.smul_subset_iff
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
x : 𝕜
h : ‖x‖ ≤ 1
rw rw₁ : Subset.{u_3} (α := Set E) ∅ ∅
⊢ HSMul.hSMul (β := Set E) x ∅ ⊆ ∅

Tactic:
rw [smul_set_empty]

Premises used: Set.smul_set_empty
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) univ

Tactic:
fun _a _ha => subset_univ _

Premises used: Set.subset_univ, Set.univ, HSMul.hSMul, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
A B : Set E
hA : Balanced 𝕜 A
hB : Balanced 𝕜 B
⊢ Balanced 𝕜 (A ∪ B)

Tactic:
fun _a ha =>
  smul_set_union.subset.trans <| union_subset_union (hA _ ha) <| hB _ ha

Premises used: Set.union_subset_union, HasSubset.Subset.trans, Set.smul_set_union, Eq.subset, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
A B : Set E
hA : Balanced 𝕜 A
hB : Balanced 𝕜 B
⊢ Balanced 𝕜 (A ∩ B)

Tactic:
fun _a ha =>
  smul_set_inter_subset.trans <| inter_subset_inter (hA _ ha) <| hB _ ha

Premises used: Set.smul_set_inter_subset, HasSubset.Subset.trans, Set.inter_subset_inter, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Sort u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
f : ι → Set E
h : ∀ (i : ι), Balanced 𝕜 (f i)
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) (⋃ (i : ι), f i)

Tactic:
fun _a ha => (smul_set_iUnion _ _).subset.trans <| iUnion_mono fun _ => h _ _ ha

Premises used: HasSubset.Subset.trans, Eq.subset, Set.smul_set_iUnion, Set.iUnion_mono, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
f : (i : ι) → κ i → Set E
h : ∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) (⋃ (i : ι), ⋃ (j : κ i), f i j)

Tactic:
balanced_iUnion fun _ => balanced_iUnion <| h _

Premises used: balanced_iUnion
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
S : Set (Set E)
h : ∀ s ∈ S, Balanced 𝕜 s
x : 𝕜
h_1 : ‖x‖ ≤ 1
x_1 : E
h_2 : Membership.mem (γ := Set E) (⋂ s ∈ S, x • s) x_1
⊢ x_1 ∈ ⋂₀ S

Tactic:
aesop