awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
hc₁ : 1 < ‖c⁻¹‖
hf₁ : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ¬c = 0

Tactic:
rw [← inv_inv c, norm_inv, inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)] at hc

Premises used: Iff.mpr, norm_pos_iff, inv_lt_one₀, norm_inv, inv_inv, inv_ne_zero
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Tactic:
opNorm_le_of_shell ε_pos hC hc ?_

Premises used: ContinuousLinearMap.opNorm_le_of_shell
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
neg : ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_of_shell ε_pos hC hc ?_

Premises used: ContinuousLinearMap.opNorm_le_of_shell
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
neg : ∀ (x : E), ε / ‖c‖⁻¹ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
neg₁ : ∀ (x : E), ε * ‖c‖⁻¹⁻¹ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
neg₂ neg₃ neg₄ neg₅ : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
rwa [norm_inv, div_eq_mul_inv, inv_inv]

Premises used: div_eq_mul_inv, norm_inv, inv_inv
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
⊢ ‖f‖ ≤ C

Tactic:
opNorm_le_bound' f hC fun x hx => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound'
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
refine : ∀ (x : E) (hx : ‖x‖ ≠ 0), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_bound' f hC fun x hx => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound'
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1

Tactic:
simp [norm_smul, inv_mul_cancel₀ hx]

Premises used: norm_smul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1

Tactic:
have H₁ : ‖algebraMap _ 𝕜 ‖x‖⁻¹ • x‖ = 1 := by simp [norm_smul, inv_mul_cancel₀ hx]
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
⊢ ‖x‖⁻¹ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C

Tactic:
simpa [norm_smul] using hf _ H₁

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
⊢ ‖x‖⁻¹ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C

Tactic:
have H₂ : ‖x‖⁻¹ * ‖f x‖ ≤ C := by simpa [norm_smul] using hf _ H₁
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
H₂ : ‖x‖⁻¹ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
rwa : ∀ (H₂ : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) / ‖x‖ ≤ C), 0 < ‖x‖
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
rwa [← div_eq_inv_mul, div_le_iff₀] at H₂

Premises used: div_le_iff₀, div_eq_inv_mul
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
H₂ : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) / ‖x‖ ≤ C
⊢ 0 < ‖x‖

Tactic:
(norm_nonneg x).lt_of_ne' hx

Premises used: norm_nonneg, LE.le.lt_of_ne'
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
H₂ : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) / ‖x‖ ≤ C
⊢ 0 < ‖x‖

Tactic:
exact (norm_nonneg x).lt_of_ne' hx

Premises used: norm_nonneg, LE.le.lt_of_ne'
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f g : E →SL[σ₁₂] F
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
(f + g).opNorm_le_bound (add_nonneg f.opNorm_nonneg g.opNorm_nonneg) fun x =>
    (norm_add_le_of_le (f.le_opNorm x) (g.le_opNorm x)).trans_eq (add_mul _ _ _).symm

Premises used: add_mul, Norm.norm, LE.le.trans_eq, ContinuousLinearMap.le_opNorm, add_nonneg, ContinuousLinearMap.opNorm_le_bound, HAdd.hAdd, ContinuousLinearMap.opNorm_nonneg, norm_add_le_of_le, Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
let : ∀ (x : E) (hx : ‖x‖ ≠ 0), 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
⊢ 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)

Tactic:
let ⟨x, hx⟩ := exists_norm_ne_zero E
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
⊢ Norm.norm (E := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E) / ‖x‖ ≤
    Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)

Tactic:
have := (ContinuousLinearMap.id 𝕜 E).ratio_le_opNorm x
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
this :
  Norm.norm (E := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E) / ‖x‖ ≤
    Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
rwa :
  ∀ (this : ‖x‖ / ‖x‖ ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)),
    1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)),
    1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
⊢ 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)

Tactic:
rwa [id_apply, div_self hx] at this

Premises used: ContinuousLinearMap.id_apply, div_self
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
inst_15 : NontrivialTopology E
⊢ NormOneClass.{u_4} (E →L[𝕜] E)

Tactic:
⟨norm_id⟩

Premises used: NormOneClass.mk, ContinuousLinearMap.norm_id
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst_7 : DistribSMul 𝕜' F
inst_8 : SMulCommClass 𝕜₂ 𝕜' F
inst_9 : SeminormedAddCommGroup 𝕜'
inst_10 : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x : E
grw : ‖HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)‖ ≤ ‖c‖ * ‖f‖ * ‖x‖
grw₁ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
grw₂ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * (‖f‖ * ‖x‖)
grw₃ grw₄ : ‖c‖ * (‖f‖ * ‖x‖) ≤ ‖c‖ * (‖f‖ * ‖x‖)
⊢ Norm.norm.{u_5} (E := F) ((c • f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖

Tactic:
grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]

Premises used: norm_smul_le, ContinuousLinearMap.smul_apply, ContinuousLinearMap.le_opNorm, mul_assoc
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
K : ℝ≥0
h : ‖f‖ ≤ (↑K : ℝ)
⊢ LipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
simpa using AddMonoidHomClass.lipschitz_of_bound f K <| le_of_opNorm_le f h

Premises used: AddMonoidHomClass.lipschitz_of_bound, ContinuousLinearMap.le_of_opNorm_le, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
rw₂ : ‖f.1 + -f.2‖ = ‖f.1 - f.2‖
rw₃ rw₄ : ‖f.1 + -f.2‖ = ‖f.1 + -f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖

Tactic:
rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, neg_add, neg_neg, ContinuousLinearMap.opNorm_neg
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
⊢ ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖

Tactic:
have A (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)) : ‖-f.1 + f.2‖ = ‖f.1 - f.2‖ := by
    rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
simp :
  Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖f.1 - f.2‖ < r})
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖-f.1 + f.2‖ < r})

Tactic:
simp only [A]
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖f.1 - f.2‖ < r})

Tactic:
ContinuousLinearMap.seminorm (σ₁₂ := σ₁₂) (E := E) (F := F) |>.uniformity_eq_of_hasBasis
    (ContinuousLinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_

Premises used: _private.0.ContinuousLinearMap.uniformity_eq_seminorm.match_2, setOf, ContinuousLinearMap.opNorm, Exists, _private.0.ContinuousLinearMap.uniformity_eq_seminorm.match_1, HasSubset.Subset, GT.gt, And, Seminorm.ball, ContinuousLinearMap.hasBasis_nhds_zero_of_basis, ContinuousLinearMap.seminorm, Metric.nhds_basis_closedBall, OfNat.ofNat, Seminorm.uniformity_eq_of_hasBasis
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
refine_1 :
  ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
refine_2 :
  ∀ (x : Set E × ℝ) (s : Set E) (r : ℝ),
    IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2 →
      ∀ (hs : IsVonNBounded 𝕜 (s, r).1) (hr : 0 < (s, r).2),
        ∃ r_1 > 0,
          Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
            {f : E →SL[σ₁₂] F |
              ∀ x ∈ (s, r).1,
                Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖f.1 - f.2‖ < r})

Tactic:
refine ContinuousLinearMap.seminorm (σ₁₂ := σ₁₂) (E := E) (F := F) |>.uniformity_eq_of_hasBasis
    (ContinuousLinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_

Premises used: _private.0.ContinuousLinearMap.uniformity_eq_seminorm.match_2, setOf, Exists, _private.0.ContinuousLinearMap.uniformity_eq_seminorm.match_1, HasSubset.Subset, GT.gt, And, Seminorm.ball, ContinuousLinearMap.hasBasis_nhds_zero_of_basis, ContinuousLinearMap.seminorm, Metric.nhds_basis_closedBall, OfNat.ofNat, Seminorm.uniformity_eq_of_hasBasis
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
refine_1 :
  ∀ (c : 𝕜) (hc : 1 < ‖c‖),
    ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
⊢ ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)

Tactic:
rcases NormedField.exists_lt_norm 𝕜 1 with ⟨c, hc⟩

Premises used: NormedField.exists_lt_norm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)

Tactic:
⟨‖c‖, ContinuousLinearMap.hasBasis_nhds_zero.mem_iff.2
      ⟨(closedBall 0 1, closedBall 0 1), ?_⟩⟩

Premises used: Iff.mpr, Norm.norm, Filter.HasBasis.mem_iff, ContinuousLinearMap.hasBasis_nhds_zero, Prod.mk, Exists.intro, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
refine_1 :
  (IsVonNBounded.{u_1, u_4} 𝕜 (E := E) (closedBall 0 1, closedBall 0 1).1 ∧
      Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1, closedBall 0 1).2) ∧
    Subset (α := Set (E →SL[σ₁₂] F))
      {f : E →SL[σ₁₂] F |
        ∀ (x : E),
          Membership.mem (γ := Set E) (closedBall 0 1, closedBall 0 1).1 x →
            Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 1, closedBall 0 1).2
              ((f : (a : E) → F) x : F)}
      (Seminorm.closedBall ContinuousLinearMap.seminorm 0 ‖c‖)
⊢ ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)

Tactic:
refine ⟨‖c‖, ContinuousLinearMap.hasBasis_nhds_zero.mem_iff.2
      ⟨(closedBall 0 1, closedBall 0 1), ?_⟩⟩
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
this : ∀ (f : E →SL[σ₁₂] F), (∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1) → ‖f‖ ≤ ‖c‖
⊢ (IsVonNBounded.{u_1, u_4} 𝕜 (E := E) (closedBall 0 1, closedBall 0 1).1 ∧
      Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1, closedBall 0 1).2) ∧
    Subset (α := Set (E →SL[σ₁₂] F))
      {f : E →SL[σ₁₂] F |
        ∀ (x : E),
          Membership.mem (γ := Set E) (closedBall 0 1, closedBall 0 1).1 x →
            Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 1, closedBall 0 1).2
              ((f : (a : E) → F) x : F)}
      (Seminorm.closedBall ContinuousLinearMap.seminorm 0 ‖c‖)

Tactic:
simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, subset_def] using this

Premises used: Metric.closedBall_mem_nhds, Set.subset_def, NormedSpace.isVonNBounded_closedBall