-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*}
    {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [UniformAddGroup E] [u : UniformSpace F]
    [hu : UniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E]
    (f : κ → E →ₛₗ[σ₁₂] F) : TFAE
    [ EquicontinuousAt ((↑) ∘ f) 0,
      Equicontinuous ((↑) ∘ f),
      UniformEquicontinuous ((↑) ∘ f),
      ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p,
      ∀ i, BddAbove (range fun k ↦ (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k)) ]

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : Nonempty ι'
κ : Type u_10
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : Nonempty ι'
κ : Type u_10
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : Nonempty ι'
κ : Type u_10
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
this : ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1
bdd : BddAbove (Set.range fun k => (q i).comp (f k))
⊢ BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))

Tactic:
rw [← Seminorm.coe_iSup_eq bdd]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : Nonempty ι'
κ : Type u_10
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
this : ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1
bdd : BddAbove (Set.range fun k => (q i).comp (f k))
⊢ BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous ⇑(⨆ i_1, (q i).comp (f i_1))

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : Nonempty ι'
κ : Type u_10
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
⊢ ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1

Tactic:
filter_upwards [Metric.equicontinuousAt_iff_right.mp (H.equicontinuous 0) 1 one_pos]
  with x hx k

Result:
case h
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι' : Type u_9
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : Nonempty ι'
κ : Type u_10
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
x : E
hx : ∀ (i : κ), dist ((DFunLike.coe ∘ f) i 0) ((DFunLike.coe ∘ f) i x) < 1
k : κ
⊢ (q i) ((f k) x) ≤ 1