-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem continuous_of_continuous_comp {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E]
    [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q)
    (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i, Continuous ((q i).comp f)) : Continuous f

Proof state:
case h.e'_5.h.e'_3
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : NormedField 𝕝
inst✝⁸ : Module 𝕝 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι'
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ 0 = ((q i).comp f) 0

Tactic:
exact (map_zero _).symm

Result:
no goals

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : NormedField 𝕝
inst✝⁸ : Module 𝕝 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι'
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ ∀ (i : ι'), Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)

Tactic:
intro i

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

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

Tactic:
refine continuous_of_continuousAt_zero f ?_

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

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : NormedField 𝕝
inst✝⁸ : Module 𝕝 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι'
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ ContinuousAt (⇑f) 0

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

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

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : NormedField 𝕝
inst✝⁸ : Module 𝕝 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι'
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)

Tactic:
convert (hf i).continuousAt.tendsto

Result:
case h.e'_5.h.e'_3
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : NormedField 𝕝
inst✝⁸ : Module 𝕝 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι'
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ 0 = ((q i).comp f) 0

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

Tactic:
have : IsTopologicalAddGroup F := hq.topologicalAddGroup

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