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‖
⊢ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C

Tactic:
7

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‖
⊢ (∃ 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

Tactic:
5 ↔ 7

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‖
⊢ (∃ 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

Tactic:
exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)

Premises used: and_congr_right, exists_congr, forall_congr'
-- 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‖
refine :
  ∀ (C : ℝ) (hC : C ≥ 0) (i : ι), (∀ (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔ ‖f i‖ ≤ C
⊢ (∃ 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

Tactic:
refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)

Premises used: and_congr_right, exists_congr, forall_congr'
-- 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‖
C : ℝ
hC : C ≥ 0
i : ι
rw rw₁ :
  (∀ (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∀ (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ (∀ (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔ ‖f i‖ ≤ C

Tactic:
rw [ContinuousLinearMap.opNorm_le_iff hC]

Premises used: ContinuousLinearMap.opNorm_le_iff
-- 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‖
⊢ (∃ 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

Tactic:
tfae_have 5 ↔ 7 := by
    refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)
    rw [ContinuousLinearMap.opNorm_le_iff hC]
-- 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
⊢ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C

Tactic:
7

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
⊢ 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
⊢ (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)

Tactic:
7 ↔ 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
simp_rw :
  (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔
    ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) y → y ≤ x
⊢ (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)

Tactic:
simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]

Premises used: bddAbove_iff_exists_ge, Set.forall_mem_range, OfNat.ofNat
-- 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
⊢ (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)

Tactic:
tfae_have 7 ↔ 8 := by
    simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]
-- 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‖)
⊢ ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C

Tactic:
6

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‖)
⊢ 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‖)
⊢ (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)

Tactic:
6 ↔ 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‖)
⊢ (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)

Tactic:
tfae_have 6 ↔ 8 := by
    simp_rw [bddAbove_def, Set.forall_mem_range]