-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem continuous_from_bounded {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'}
    {_ : TopologicalSpace E} (hp : WithSeminorms p) {_ : TopologicalSpace F} (hq : WithSeminorms q)
    (f : E →ₛₗ[τ₁₂] F) (hf : Seminorm.IsBounded p q f) : Continuous f

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
⊢ Continuous ⇑f

Tactic:
have : IsTopologicalAddGroup E := hp.topologicalAddGroup

Result:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
⊢ Continuous ⇑f

Proof state:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous ⇑(∑ i ∈ s, (C • p) i)

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

Result:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous fun x => (coeFnAddMonoidHom 𝕝 E) (∑ i ∈ s, C • p i) x

Proof state:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ C • s.sup p
⊢ Continuous ⇑((q i).comp f)

Tactic:
rw [← Seminorm.finset_sup_smul] at hC

Result:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous ⇑((q i).comp f)

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
⊢ Continuous ⇑f

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

Result:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
⊢ Continuous ⇑((q i).comp f)

Proof state:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous ⇑((q i).comp f)

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

Result:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous ⇑(∑ i ∈ s, (C • p) i)

Proof state:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous fun x => ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E) (C • p c) x

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

Result:
no goals