awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
simp_rw :
  ∀ (i : ι'),
    Tendsto.{u_6, 0} (α := E) (β := ℝ) (Function.comp (β := F) (⇑(q i) : (a : F) → ℝ) (⇑f : (a : E) → F)) (𝓝 0) (𝓝 0)
⊢ ContinuousAt.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F) 0

Tactic:
simp_rw [ContinuousAt, f.map_zero, q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.tendsto_iInf,
    Filter.tendsto_comap_iff]

Premises used: ContinuousAt, LinearMap.map_zero, Filter.tendsto_comap_iff, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, Iff.mp, Filter.tendsto_iInf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
i : ι'
⊢ Tendsto.{u_6, 0} (α := E) (β := ℝ) ((⇑((q i).comp f) : (a : E) → ℝ) : (a : E) → ℝ) (𝓝 0)
    (𝓝 (((q i).comp f : (a : E) → ℝ) 0) : Filter ℝ)

Tactic:
(hf i).continuousAt.tendsto

Premises used: Continuous.continuousAt, ContinuousAt.tendsto
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
i : ι'
h : Eq (α := ℝ) (0 : ℝ) (((q i).comp f : (a : E) → ℝ) 0 : ℝ)
⊢ Tendsto.{u_6, 0} (α := E) (β := ℝ) (Function.comp (β := F) (⇑(q i) : (a : F) → ℝ) (⇑f : (a : E) → F)) (𝓝 0) (𝓝 0)

Tactic:
convert! (hf i).continuousAt.tendsto

Premises used: Continuous.continuousAt, ContinuousAt.tendsto
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
i : ι'
⊢ Eq (α := ℝ) (0 : ℝ) (((q i).comp f : (a : E) → ℝ) 0 : ℝ)

Tactic:
(map_zero _).symm

Premises used: map_zero, Eq.symm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
i : ι'
⊢ Eq (α := ℝ) (0 : ℝ) (((q i).comp f : (a : E) → ℝ) 0 : ℝ)

Tactic:
exact (map_zero _).symm

Premises used: map_zero, Eq.symm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
⊢ Continuous[inst_7, inst_9] (⇑f : (a : E) → F) ↔ ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)

Tactic:
⟨fun h i => (hq.continuous_seminorm i).comp h, continuous_of_continuous_comp hq f⟩

Premises used: Continuous.comp, WithSeminorms.continuous_of_continuous_comp, WithSeminorms.continuous_seminorm, Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
⊢ IsTopologicalAddGroup E

Tactic:
have : IsTopologicalAddGroup E := hp.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
⊢ Continuous[x, x_1] (⇑f : (a : E) → F)

Tactic:
continuous_of_continuous_comp hq _ fun i => ?_

Premises used: WithSeminorms.continuous_of_continuous_comp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
refine : ∀ (i : ι'), Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
⊢ Continuous[x, x_1] (⇑f : (a : E) → F)

Tactic:
refine continuous_of_continuous_comp hq _ fun i => ?_

Premises used: WithSeminorms.continuous_of_continuous_comp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
rcases : ∀ (s : Finset ι) (C : ℝ≥0) (hC : (q i).comp f ≤ C • s.sup p), Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
⊢ Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)

Tactic:
rcases hf i with ⟨s, C, hC⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ C • s.sup p
⊢ (q i).comp f ≤ s.sup (C • p)

Tactic:
rw [← Seminorm.finset_sup_smul] at hC

Premises used: Seminorm.finset_sup_smul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_le ?_ (hC.trans <| Seminorm.finset_sup_le_sum _ _)

Premises used: LE.le.trans, Seminorm.finset_sup_le_sum, Seminorm.continuous_of_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
refine : Continuous[x, _] (⇑(∑ i ∈ s, (C • p) i) : (a : E) → ℝ)
⊢ Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)

Tactic:
refine Seminorm.continuous_of_le ?_ (hC.trans <| Seminorm.finset_sup_le_sum _ _)

Premises used: LE.le.trans, Seminorm.finset_sup_le_sum, Seminorm.continuous_of_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
change : Continuous[x, _] fun (x : E) ↦ (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (∑ i ∈ s, C • p i) x
⊢ Continuous[x, _] (⇑(∑ i ∈ s, (C • p) i) : (a : E) → ℝ)

Tactic:
change Continuous (fun x ↦ Seminorm.coeFnAddMonoidHom _ _ (∑ i ∈ s, C • p i) x)

Premises used: Continuous, HSMul.hSMul, Seminorm.coeFnAddMonoidHom, DFunLike.coe, Finset.sum
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
simp_rw : Continuous[x, _] fun (x : E) ↦ ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (C • p c) x
⊢ Continuous[x, _] fun (x : E) ↦ (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (∑ i ∈ s, C • p i) x

Tactic:
simp_rw [map_sum, Finset.sum_apply]

Premises used: Finset.sum_apply, map_sum
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x, _] fun (x : E) ↦ ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (C • p c) x

Tactic:
(continuous_finsetSum _ fun i _ ↦ (hp.continuous_seminorm i).const_smul (C : ℝ))

Premises used: WithSeminorms.continuous_seminorm, continuous_finsetSum, Continuous.const_smul, NNReal.toReal
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x, _] fun (x : E) ↦ ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (C • p c) x

Tactic:
exact (continuous_finsetSum _ fun i _ ↦ (hp.continuous_seminorm i).const_smul (C : ℝ))

Premises used: WithSeminorms.continuous_seminorm, continuous_finsetSum, Continuous.const_smul, NNReal.toReal
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
ι : Type u_9
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
F : Type u_11
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕝₂ F
inst_7 : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : ∃ (s : Finset ι) (C : ℝ≥0), comp (normSeminorm 𝕝₂ F) f ≤ C • s.sup p
⊢ Seminorm.IsBounded.{u_4, u_5, u_6, u_11, u_9, 0} (𝕜₂ := 𝕝₂) (F := F) (σ₁₂ := τ₁₂) p
    (fun (x : Fin 1) ↦ normSeminorm 𝕝₂ F) f

Tactic:
rw [← Seminorm.isBounded_const (Fin 1)] at hf

Premises used: Seminorm.isBounded_const, OfNat.ofNat, Fin
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
ι : Type u_9
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
F : Type u_11
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕝₂ F
inst_7 : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf :
  Seminorm.IsBounded.{u_4, u_5, u_6, u_11, u_9, 0} (𝕜₂ := 𝕝₂) (F := F) (σ₁₂ := τ₁₂) p
    (fun (x : Fin 1) ↦ normSeminorm 𝕝₂ F) f
⊢ Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → F)

Tactic:
continuous_of_isBounded hp (norm_withSeminorms 𝕝₂ F) f hf

Premises used: norm_withSeminorms, WithSeminorms.continuous_of_isBounded
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
ι : Type u_9
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
F : Type u_11
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕝₂ F
inst_7 : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf :
  Seminorm.IsBounded.{u_4, u_5, u_6, u_11, u_9, 0} (𝕜₂ := 𝕝₂) (F := F) (σ₁₂ := τ₁₂) p
    (fun (x : Fin 1) ↦ normSeminorm 𝕝₂ F) f
⊢ Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → F)

Tactic:
exact continuous_of_isBounded hp (norm_withSeminorms 𝕝₂ F) f hf

Premises used: norm_withSeminorms, WithSeminorms.continuous_of_isBounded
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
F : Type u_7
ι : Type u_9
inst : NormedField 𝕝
inst_1 : AddCommGroup F
inst_2 : NormedField 𝕝₂
inst_3 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
E : Type u_11
inst_5 : SeminormedAddCommGroup E
inst_6 : NormedSpace 𝕝 E
inst_7 : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι), ∃ (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕝 E) C (normSeminorm 𝕝 E)
⊢ Seminorm.IsBounded.{u_4, u_5, u_11, u_7, 0, u_9} (𝕜 := 𝕝) (E := E) (σ₁₂ := τ₁₂) (fun (x : Fin 1) ↦ normSeminorm 𝕝 E) q
    f

Tactic:
rw [← Seminorm.const_isBounded (Fin 1)] at hf

Premises used: Seminorm.const_isBounded, OfNat.ofNat, Fin
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
F : Type u_7
ι : Type u_9
inst : NormedField 𝕝
inst_1 : AddCommGroup F
inst_2 : NormedField 𝕝₂
inst_3 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
E : Type u_11
inst_5 : SeminormedAddCommGroup E
inst_6 : NormedSpace 𝕝 E
inst_7 : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf :
  Seminorm.IsBounded.{u_4, u_5, u_11, u_7, 0, u_9} (𝕜 := 𝕝) (E := E) (σ₁₂ := τ₁₂) (fun (x : Fin 1) ↦ normSeminorm 𝕝 E) q
    f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7] (⇑f : (a : E) → F)

Tactic:
continuous_of_isBounded (norm_withSeminorms 𝕝 E) hq f hf

Premises used: norm_withSeminorms, WithSeminorms.continuous_of_isBounded
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
F : Type u_7
ι : Type u_9
inst : NormedField 𝕝
inst_1 : AddCommGroup F
inst_2 : NormedField 𝕝₂
inst_3 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
E : Type u_11
inst_5 : SeminormedAddCommGroup E
inst_6 : NormedSpace 𝕝 E
inst_7 : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf :
  Seminorm.IsBounded.{u_4, u_5, u_11, u_7, 0, u_9} (𝕜 := 𝕝) (E := E) (σ₁₂ := τ₁₂) (fun (x : Fin 1) ↦ normSeminorm 𝕝 E) q
    f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7] (⇑f : (a : E) → F)

Tactic:
exact continuous_of_isBounded (norm_withSeminorms 𝕝 E) hq f hf

Premises used: norm_withSeminorms, WithSeminorms.continuous_of_isBounded
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst_7 : UniformSpace E
inst_8 : IsUniformAddGroup E
u : UniformSpace F
inst_9 : IsUniformAddGroup F
hq : WithSeminorms q
inst_10 : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ UniformEquicontinuous.{u_11, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) ↔
    ∀ (i : ι'),
      ∃ (p : Seminorm 𝕜 E),
        Continuous[inst_7.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧ ∀ (k : κ), (q i).comp (f k) ≤ p

Tactic:
(hq.equicontinuous_TFAE f).out 2 3

Premises used: WithSeminorms.equicontinuous_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst_7 : UniformSpace E
inst_8 : IsUniformAddGroup E
u : UniformSpace F
inst_9 : IsUniformAddGroup F
hq : WithSeminorms q
inst_10 : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ UniformEquicontinuous.{u_11, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) ↔
    ∀ (i : ι'),
      BddAbove.{u_6} (α := Seminorm 𝕜 E) (Set.range fun (k : κ) ↦ (q i).comp (f k)) ∧
        Continuous[inst_7.toTopologicalSpace, _] (⨆ (k : κ), (⇑((q i).comp (f k)) : (a : E) → ℝ))

Tactic:
(hq.equicontinuous_TFAE f).out 2 4

Premises used: WithSeminorms.equicontinuous_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
topology_eq_withSeminorms : t = q.moduleFilterBasis.topology
⊢ WithSeminorms q

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
topology_eq_withSeminorms : p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
⊢ t = q.moduleFilterBasis.topology

Tactic:
rw [hp.topology_eq_withSeminorms]

Premises used: WithSeminorms.topology_eq_withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
topology_eq_withSeminorms : p.moduleFilterBasis.topology ≤ q.moduleFilterBasis.topology
topology_eq_withSeminorms₁ : q.moduleFilterBasis.topology ≤ p.moduleFilterBasis.topology
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
topology_eq_withSeminorms : Continuous[p.moduleFilterBasis.topology, q.moduleFilterBasis.topology] id
⊢ p.moduleFilterBasis.topology ≤ q.moduleFilterBasis.topology

Tactic:
rw [← continuous_id_iff_le]

Premises used: continuous_id_iff_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
topology_eq_withSeminorms : Continuous[q.moduleFilterBasis.topology, p.moduleFilterBasis.topology] id
⊢ q.moduleFilterBasis.topology ≤ p.moduleFilterBasis.topology

Tactic:
rw [← continuous_id_iff_le]

Premises used: continuous_id_iff_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded p q LinearMap.id

Tactic:
assumption