awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ norm (E := 𝕜 →L[𝕜] E) ((toSpanSingletonLE 𝕜 𝕜 E : (a : E) → 𝕜 →L[𝕜] E) x : 𝕜 →L[𝕜] E) = ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ Eq (α := 𝕜 →L[𝕜] E) ((toSpanSingletonLIE 𝕜 E : (a : E) → 𝕜 →L[𝕜] E) x : 𝕜 →L[𝕜] E) (toSpanSingleton 𝕜 x : 𝕜 →L[𝕜] E)

Tactic:
rfl

Premises used: ContinuousLinearMap.toSpanSingleton, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →L[𝕜] E
⊢ Eq.{u_2 + 1} (α := E) ((LinearIsometryEquiv.symm (toSpanSingletonLIE 𝕜 E) : (a : 𝕜 →L[𝕜] E) → E) f : E)
    ((f : (a : 𝕜) → E) 1 : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Eq (α := E ≃ₗ[𝕜] 𝕜 →L[𝕜] E) (LinearIsometryEquiv.toLinearEquiv (E₂ := 𝕜 →L[𝕜] E) (toSpanSingletonLIE 𝕜 E))
    (toSpanSingletonLE 𝕜 𝕜 E)

Tactic:
rfl

Premises used: ContinuousLinearMap.toSpanSingletonLE, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Eq (α := E ≃L[𝕜] 𝕜 →L[𝕜] E) (↑(toSpanSingletonLIE 𝕜 E) : E ≃L[𝕜] 𝕜 →L[𝕜] E) toSpanSingletonCLE

Tactic:
rfl

Premises used: ContinuousLinearMap.toSpanSingletonLE, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearMap.toSpanSingletonCLE, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
c : R
x : E
⊢ norm (E := E)
      (((((AlgHom.toLinearMap (Algebra.lsmul 𝕜 𝕜 E) :
                    LinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (Module.End 𝕜 E)) :
                  (a : R) → E →ₗ[𝕜] E)
                c :
              E →ₗ[𝕜] E) :
            (a : E) → E)
          x :
        E) ≤
    1 * ‖c‖ * ‖x‖

Tactic:
simpa only [one_mul] using norm_smul_le c x

Premises used: norm_smul_le, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
c : R
x : E
⊢ (((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) c : E →L[𝕜] E) : (a : E) → E) x = c • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ Eq (α := 𝕜 →L[𝕜] E) ((flip (lsmul 𝕜 𝕜) : (a : E) → 𝕜 →L[𝕜] E) x : 𝕜 →L[𝕜] E) (toSpanSingleton 𝕜 x : 𝕜 →L[𝕜] E)

Tactic:
rfl

Premises used: LinearMap.mkContinuousOfExistsBound, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, LinearMap.toSpanSingleton, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
x y : E
h :
  Eq (α := R →L[𝕜] E) ((flip (lsmul 𝕜 R) : (a : E) → R →L[𝕜] E) x : R →L[𝕜] E)
    ((flip (lsmul 𝕜 R) : (a : E) → R →L[𝕜] E) y : R →L[𝕜] E)
⊢ x = y

Tactic:
simpa using congr($h 1)
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
x : R
⊢ norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ ‖x‖

Tactic:
ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x) fun y => norm_smul_le x y

Premises used: norm_smul_le, ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
refine : ∀ (x : R), norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ 1 * ‖x‖
⊢ norm (E := ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) (lsmul 𝕜 R) ≤ 1

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, zero_le_one
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
x : R
simp_rw : norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ ‖x‖
⊢ norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ 1 * ‖x‖

Tactic:
simp_rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
x : R
⊢ norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ ‖x‖

Tactic:
opNorm_lsmul_apply_le _

Premises used: ContinuousLinearMap.opNorm_lsmul_apply_le
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
x : R
⊢ norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ ‖x‖

Tactic:
exact opNorm_lsmul_apply_le _

Premises used: ContinuousLinearMap.opNorm_lsmul_apply_le
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalNormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
inst_5 : RegularNormedAlgebra 𝕜 R
inst_6 : Nontrivial R
⊢ norm (E := R →L[𝕜] R →L[𝕜] R) (mul 𝕜 R) = 1

Tactic:
(mulₗᵢ 𝕜 R).norm_toContinuousLinearMap

Premises used: LinearIsometry.norm_toContinuousLinearMap, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, ContinuousLinearMap.mulₗᵢ, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.mul, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalNormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
inst_5 : RegularNormedAlgebra 𝕜 R
inst_6 : Nontrivial R
⊢ nnnorm (E := R →L[𝕜] R →L[𝕜] R) (mul 𝕜 R) = 1

Tactic:
Subtype.ext <| opNorm_mul 𝕜 R

Premises used: ContinuousLinearMap.opNorm_mul, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
⊢ norm (E := ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) (lsmul 𝕜 R) = 1

Tactic:
ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_

Premises used: zero_le_one, ContinuousLinearMap.opNorm_eq_of_bounds
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
refine_1 :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      1 * ‖x‖
refine_2 :
  ∀ N ≥ 0,
    ∀
      (h :
        ∀ (x : R),
          norm.{u_2} (E := E →L[𝕜] E)
              (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) :
                    (a : R) → E →L[𝕜] E)
                  x :
                E →L[𝕜] E) ≤
            N * ‖x‖),
      1 ≤ N
⊢ norm (E := ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) (lsmul 𝕜 R) = 1

Tactic:
refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_

Premises used: zero_le_one, ContinuousLinearMap.opNorm_eq_of_bounds
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
x : R
refine_1 :
  norm.{u_2} (E := E →L[𝕜] E)
      (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
        E →L[𝕜] E) ≤
    ‖x‖
⊢ norm.{u_2} (E := E →L[𝕜] E)
      (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
        E →L[𝕜] E) ≤
    1 * ‖x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
x : R
⊢ norm.{u_2} (E := E →L[𝕜] E)
      (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
        E →L[𝕜] E) ≤
    ‖x‖

Tactic:
apply opNorm_lsmul_apply_le

Premises used: ContinuousLinearMap.opNorm_lsmul_apply_le
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
N : ℝ
h_1 : N ≥ 0
h :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      N * ‖x‖
refine_2 : ∀ (y : E) (hy : y ≠ 0), 1 ≤ N
⊢ 1 ≤ N

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : E)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
N : ℝ
h_1 : N ≥ 0
h :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      N * ‖x‖
y : E
hy : y ≠ 0
⊢ 1 ≤ N

Tactic:
le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)

Premises used: Iff.mpr, norm_pos_iff, le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
N : ℝ
h_1 : N ≥ 0
h :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      N * ‖x‖
y : E
hy : y ≠ 0
refine_2 : 1 * ‖y‖ ≤ N * ‖y‖
⊢ 1 ≤ N

Tactic:
refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)

Premises used: Iff.mpr, norm_pos_iff, le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
N : ℝ
h_1 : N ≥ 0
h :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      N * ‖x‖
y : E
hy : y ≠ 0
⊢ 1 * ‖y‖ ≤ N * ‖y‖

Tactic:
simpa using le_of_opNorm_le _ (h 1) y

Premises used: ContinuousLinearMap.le_of_opNorm_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
a : (↑‖f‖₊ : ℝ) = (↑(sInf {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}) : ℝ)
⊢ ‖f‖₊ = sInf {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
a :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})
⊢ (↑‖f‖₊ : ℝ) = (↑(sInf {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}) : ℝ)

Tactic:
rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image]

Premises used: ContinuousLinearMap.norm_def, coe_nnnorm, NNReal.coe_image, NNReal.coe_sInf
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
a :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑(c * ‖x‖₊) : ℝ)}
            (NNReal.mk x ⋯)})
a₁ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑c : ℝ) * (↑‖x‖₊ : ℝ)}
            (NNReal.mk x ⋯)})
a₂ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑c : ℝ) * ‖x‖} (NNReal.mk x ⋯)})
a₃ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          ∀ (x_1 : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x_1 : F) ≤ (↑(NNReal.mk x ⋯) : ℝ) * ‖x_1‖})
a₄ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf {x : ℝ | ∃ (_ : 0 ≤ x), ∀ (x_1 : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x_1 : F) ≤ x * ‖x_1‖})
⊢ Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})

Tactic:
simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]

Premises used: NNReal.coe_mk, Set.mem_setOf_eq, exists_prop, coe_nnnorm, NNReal.coe_mul, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : Subsingleton E
f : E →SL[σ₁₂] F
⊢ ‖f‖₊ = 0

Tactic:
NNReal.eq <| f.opNorm_subsingleton

Premises used: NNReal.eq, ContinuousLinearMap.opNorm_subsingleton
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖₊
⊢ ‖f‖₊ ≤ M

Tactic:
opNorm_le_bound f (zero_le (a := M)) hM

Premises used: zero_le, ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
rwa rwa₁ rwa₂ rwa₃ : (↑‖x‖₊ : ℝ) ≠ 0
⊢ ‖x‖₊ ≠ 0

Tactic:
rwa [← NNReal.coe_ne_zero]

Premises used: NNReal.coe_ne_zero
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ = 1
rwa rwa₁ rwa₂ rwa₃ : (↑‖x‖₊ : ℝ) = 1
⊢ ‖x‖₊ = 1

Tactic:
rwa [← NNReal.coe_eq_one]

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

Tactic:
opNorm_le_of_lipschitz hf

Premises used: NNReal.toReal, ContinuousLinearMap.opNorm_le_of_lipschitz
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
φ : E →SL[σ₁₂] F
M : ℝ≥0
h_above : ∀ (x : E), nnnorm.{u_5} (E := F) ((φ : (a : E) → F) x : F) ≤ M * ‖x‖₊
h_below : ∀ (N : ℝ≥0), (∀ (x : E), nnnorm.{u_5} (E := F) ((φ : (a : E) → F) x : F) ≤ N * ‖x‖₊) → M ≤ N
⊢ ‖φ‖₊ = M

Tactic:
Subtype.ext <| opNorm_eq_of_bounds (zero_le (a := M)) h_above <| Subtype.forall'.mpr h_below

Premises used: Iff.mpr, zero_le, NNReal, ContinuousLinearMap.opNorm_eq_of_bounds, Subtype.forall', Subtype.ext
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
C : ℝ≥0
⊢ ‖f‖₊ ≤ C ↔ ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖₊

Tactic:
opNorm_le_iff C.2

Premises used: ContinuousLinearMap.opNorm_le_iff, Subtype.property
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsLeast {C : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖₊} ‖f‖₊

Tactic:
simpa only [← opNNNorm_le_iff] using isLeast_Ici

Premises used: ContinuousLinearMap.opNNNorm_le_iff, isLeast_Ici
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : NontriviallyNormedField 𝕜₃
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
inst_12 : RingHomIsometric σ₁₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖h ∘SL f‖₊ ≤ ‖h‖₊ * ‖f‖₊

Tactic:
opNorm_comp_le h f

Premises used: ContinuousLinearMap.opNorm_comp_le
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : NontriviallyNormedField 𝕜₃
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
inst_12 : RingHomIsometric σ₁₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖h ∘SL f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_mul] using opNNNorm_comp_le h f

Premises used: ENNReal.coe_mul, ENorm.enorm, ContinuousLinearMap.opNNNorm_comp_le