awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
mp :
  (∃ (p : Seminorm 𝕜 E),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
        ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p) →
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
mpr :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) →
    ∃ (p : Seminorm 𝕜 E),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
        ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
⊢ (∃ (p : Seminorm 𝕜 E),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
        ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p) ↔
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
p : Seminorm 𝕜 E
hp : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
hpf : ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
mp :
  ∀ (C : ℝ) (hC : ∀ (x : E), (p : (a : E) → ℝ) x ≤ C * ‖x‖),
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩

Premises used: Seminorm.bound_of_continuous_normedSpace
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
p : Seminorm 𝕜 E
hp : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
hpf : ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
C : ℝ
hC : ∀ (x : E), (p : (a : E) → ℝ) x ≤ C * ‖x‖
⊢ ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩

Premises used: Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
p : Seminorm 𝕜 E
hp : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
hpf : ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
C : ℝ
hC : ∀ (x : E), (p : (a : E) → ℝ) x ≤ C * ‖x‖
⊢ ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
exact ⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ∃ (p : Seminorm 𝕜 E),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
      ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p

Tactic:
⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩

Premises used: WithSeminorms.continuous_seminorm, normSeminorm, And.intro, Exists.intro, norm_withSeminorms, HSMul.hSMul, OfNat.ofNat, Continuous.const_smul, Real.toNNReal
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
mpr :
  ∀ (i : ι) (x : E),
    LE.le (α := (fun (a : E) ↦ ℝ) x)
      ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
        (Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f i) : E →ₛₗ[σ₁₂] F)) x)
      ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
        (HSMul.hSMul (β := Seminorm 𝕜 E) C.toNNReal (normSeminorm 𝕜 E)) x)
⊢ ∃ (p : Seminorm 𝕜 E),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
      ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p

Tactic:
refine ⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
i : ι
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
      (Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f i) : E →ₛₗ[σ₁₂] F)) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
      (HSMul.hSMul (β := Seminorm 𝕜 E) C.toNNReal (normSeminorm 𝕜 E)) x)

Tactic:
(hC i x).trans (mul_le_mul_of_nonneg_right (C.le_coe_toNNReal) (norm_nonneg x))

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, norm_nonneg, Real.le_coe_toNNReal
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
i : ι
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
      (Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f i) : E →ₛₗ[σ₁₂] F)) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
      (HSMul.hSMul (β := Seminorm 𝕜 E) C.toNNReal (normSeminorm 𝕜 E)) x)

Tactic:
exact (hC i x).trans (mul_le_mul_of_nonneg_right (C.le_coe_toNNReal) (norm_nonneg x))

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, norm_nonneg, Real.le_coe_toNNReal
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
⊢ UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) ↔
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
tfae_have 3 ↔ 4 := by
    refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
      ?_
    rw [forall_const]
    constructor
    · intro ⟨p, hp, hpf⟩
      rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩
      exact ⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩
    · intro ⟨C, hC⟩
      refine ⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩
      exact (hC i x).trans (mul_le_mul_of_nonneg_right (C.le_coe_toNNReal) (norm_nonneg x))
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
tfae_3_iff_4 :
  UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) ↔
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ [EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0,
      Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖),
      LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
ι : Type u_8
inst : Fintype ι
inst_1 : DecidableEq ι
𝕜 : Type u_9
inst_2 : NontriviallyNormedField 𝕜
E : ι → Type u_10
inst_3 : (i : ι) → SeminormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_9, u_10} 𝕜 (E i)
i : ι
⊢ norm (E := E i →L[𝕜] (i : ι) → E i) (single 𝕜 E i : E i →L[𝕜] (i : ι) → E i) ≤ 1

Tactic:
(LinearIsometry.single 𝕜 E i).norm_toContinuousLinearMap_le

Premises used: ContinuousLinearMap.single, LinearMap.single, LinearIsometry.norm_toContinuousLinearMap_le, LinearIsometry.single, LinearIsometry.toContinuousLinearMap