-- 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:
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✝
this : ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1
bdd : BddAbove (Set.range fun k => (q i).comp (f k))
x : E
hx : ∀ (k : κ), (q i) ((f k) x) ≤ 1
⊢ x ∈ (⨆ i_1, (q i).comp (f i_1)).closedBall 0 1

Tactic:
simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using hx

Result:
no goals

Proof state:
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

Tactic:
simpa using (hx k).le

Result:
no goals

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)
⊢ [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 3 → 2 := UniformEquicontinuous.equicontinuous

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)
⊢ [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
⊢ (List.map (fun p => p i)
      [fun k => EquicontinuousAt (DFunLike.coe ∘ f) 0, fun k => Equicontinuous (DFunLike.coe ∘ f), fun k =>
        UniformEquicontinuous (DFunLike.coe ∘ f), fun i => ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
        fun i => BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))]).TFAE

Tactic:
simp only [List.map]

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
⊢ [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