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‖)
⊢ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)

Tactic:
8

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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‖)
⊢ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤

Tactic:
9

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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‖)
⊢ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤

Tactic:
8 ↔ 9

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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‖)
rw :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔
    BddAbove (Set.range.{0, u_8 + 1} (ι := ι) (NNReal.toReal ∘ fun (i : ι) ↦ ‖f i‖₊))
⊢ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤

Tactic:
rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp]

Premises used: Set.range_comp, ENNReal.iSup_coe_lt_top, NNReal.bddAbove_coe
-- 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‖)
⊢ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔
    BddAbove (Set.range.{0, u_8 + 1} (ι := ι) (NNReal.toReal ∘ fun (i : ι) ↦ ‖f i‖₊))

Tactic:
rfl
-- 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‖)
⊢ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤

Tactic:
tfae_have 8 ↔ 9 := by
    rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp]
    rfl
-- 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)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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:
3 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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:
((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
      ?_

Premises used: WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, norm_withSeminorms, Iff.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)) ⊤
refine :
  (∀ (i : Fin 1),
      ∃ (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‖
⊢ 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:
refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
      ?_

Premises used: WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, norm_withSeminorms, Iff.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)) ⊤
rw :
  (∃ (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‖
⊢ (∀ (i : Fin 1),
      ∃ (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:
rw [forall_const]

Premises used: forall_const