awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
⊢ ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2

Tactic:
have h1 b : C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 := by grw [f.le_opNNNorm b]; ring_nf; rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
⊢ ∀ (x : A),
    nnnorm (E := A) ((f : (a : A) → A) x : A) ≤
      HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) C : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) * ‖x‖₊

Tactic:
simpa only [sqrt_sq, sqrt_mul] using fun b ↦ sqrt_le_sqrt.2 <| (h b).trans (h1 b)

Premises used: Iff.mpr, NNReal.sqrt_sq, NNReal.sqrt_le_sqrt, NNReal.sqrt_mul, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
⊢ HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) C

Tactic:
have := NNReal.div_le_of_le_mul <| f.opNNNorm_le_bound _ <| by
      simpa only [sqrt_sq, sqrt_mul] using fun b ↦ sqrt_le_sqrt.2 <| (h b).trans (h1 b)
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
this : HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) C
⊢ HPow.hPow (β := ℝ) (HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0)) 2 ≤
    HPow.hPow (α := ℝ≥0) (β := ℝ) ((sqrt : (a : ℝ≥0) → ℝ≥0) C : ℝ≥0) 2

Tactic:
NNReal.rpow_le_rpow this two_pos.le

Premises used: NNReal.rpow_le_rpow, two_pos, LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
this : HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) C
h₁ : ‖f‖₊ = HPow.hPow (β := ℝ) (HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0)) 2
h₂ : C = HPow.hPow (α := ℝ≥0) (β := ℝ) ((sqrt : (a : ℝ≥0) → ℝ≥0) C : ℝ≥0) 2
⊢ ‖f‖₊ ≤ C

Tactic:
convert! NNReal.rpow_le_rpow this two_pos.le

Premises used: NNReal.rpow_le_rpow, two_pos, LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
this : HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) C
h₁ : ‖f‖₊ = HPow.hPow (β := ℕ) ‖f‖₊ 2 / ‖f‖₊
⊢ ‖f‖₊ = HPow.hPow (β := ℝ) (HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0)) 2

Tactic:
simp only [NNReal.rpow_two, div_pow, sq_sqrt]

Premises used: NNReal.rpow_two, div_pow, NNReal.sq_sqrt
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
this : HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) C
⊢ ‖f‖₊ = HPow.hPow (β := ℕ) ‖f‖₊ 2 / ‖f‖₊

Tactic:
simp only [sq, mul_self_div_self]

Premises used: sq, mul_self_div_self
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
h1 : ∀ (b : A), C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
this : HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0) ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) C
⊢ C = HPow.hPow (α := ℝ≥0) (β := ℝ) ((sqrt : (a : ℝ≥0) → ℝ≥0) C : ℝ≥0) 2

Tactic:
simp only [NNReal.rpow_two, sq_sqrt]

Premises used: NNReal.rpow_two, NNReal.sq_sqrt
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
⊢ ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C

Tactic:
have h0 : ∀ f : A →L[𝕜] A, ∀ C : ℝ≥0, (∀ b : A, ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C := by
    intro f C h
    have h1 b : C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 := by grw [f.le_opNNNorm b]; ring_nf; rfl
    have := NNReal.div_le_of_le_mul <| f.opNNNorm_le_bound _ <| by
      simpa only [sqrt_sq, sqrt_mul] using fun b ↦ sqrt_le_sqrt.2 <| (h b).trans (h1 b)
    convert! NNReal.rpow_le_rpow this two_pos.le
    · simp only [NNReal.rpow_two, div_pow, sq_sqrt]
      simp only [sq, mul_self_div_self]
    · simp only [NNReal.rpow_two, sq_sqrt]
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
b : A
⊢ HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 =
    ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) b) : A) ((a.toProd.1 : (a : A) → A) b : A)‖₊

Tactic:
simpa only [← sq] using CStarRing.nnnorm_star_mul_self.symm

Premises used: sq, Eq.symm, CStarRing.nnnorm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
b : A
⊢ ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) b) : A) ((a.toProd.1 : (a : A) → A) b : A)‖₊ ≤
    nnnorm (E := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) b) : A) : A) * ‖b‖₊

Tactic:
(a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)

Premises used: nnnorm_mul_le, DoubleCentralizer.central, Eq.rec, Prod.fst, DFunLike.coe, DoubleCentralizer.toProd, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
b : A
⊢ nnnorm (E := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) b) : A) : A) * ‖b‖₊ ≤
    ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊

Tactic:
nnnorm_star (a.fst b) ▸ mul_le_mul_left (a.snd.le_opNNNorm _) _

Premises used: nnnorm_star, Eq.rec, Prod.fst, ContinuousLinearMap.le_opNNNorm, mul_le_mul_left, Prod.snd, DFunLike.coe, DoubleCentralizer.toProd
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
b : A
simpa :
  HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 =
    ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) b) : A) ((a.toProd.1 : (a : A) → A) b : A)‖₊
⊢ HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
    ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊

Tactic:
calc
      ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by
        simpa only [← sq] using CStarRing.nnnorm_star_mul_self.symm
      _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
      _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ :=
        nnnorm_star (a.fst b) ▸ mul_le_mul_left (a.snd.le_opNNNorm _) _

Premises used: Prod.fst, Prod.snd, DFunLike.coe, DoubleCentralizer.toProd, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
⊢ ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊

Tactic:
have h1 : ∀ b, ‖a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ := by
    intro b
    calc
      ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by
        simpa only [← sq] using CStarRing.nnnorm_star_mul_self.symm
      _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
      _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ :=
        nnnorm_star (a.fst b) ▸ mul_le_mul_left (a.snd.le_opNNNorm _) _
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
b : A
⊢ HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A)) 2 =
    ‖HMul.hMul (α := A) (β := A) ((a.toProd.2 : (a : A) → A) b : A) (star ((a.toProd.2 : (a : A) → A) b) : A)‖₊

Tactic:
simpa only [← sq] using CStarRing.nnnorm_self_mul_star.symm

Premises used: sq, CStarRing.nnnorm_self_mul_star, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
b : A
⊢ ‖HMul.hMul (α := A) (β := A) ((a.toProd.2 : (a : A) → A) b : A) (star ((a.toProd.2 : (a : A) → A) b) : A)‖₊ ≤
    ‖b‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) (star ((a.toProd.2 : (a : A) → A) b) : A) : A)

Tactic:
((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)

Premises used: nnnorm_mul_le, DoubleCentralizer.central, Eq.rec, Eq.symm, Prod.snd, DFunLike.coe, DoubleCentralizer.toProd, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
b : A
⊢ ‖b‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) (star ((a.toProd.2 : (a : A) → A) b) : A) : A) =
    nnnorm (E := A) ((a.toProd.1 : (a : A) → A) (star ((a.toProd.2 : (a : A) → A) b) : A) : A) * ‖b‖₊

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
b : A
⊢ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) (star ((a.toProd.2 : (a : A) → A) b) : A) : A) * ‖b‖₊ ≤
    ‖a.toProd.1‖₊ * nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A) * ‖b‖₊

Tactic:
nnnorm_star (a.snd b) ▸ mul_le_mul_left (a.fst.le_opNNNorm _) _

Premises used: nnnorm_star, Eq.rec, Prod.fst, ContinuousLinearMap.le_opNNNorm, mul_le_mul_left, Prod.snd, DFunLike.coe, DoubleCentralizer.toProd
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
b : A
b₁ :
  HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A)) 2 =
    ‖HMul.hMul (α := A) (β := A) ((a.toProd.2 : (a : A) → A) b : A) (star ((a.toProd.2 : (a : A) → A) b) : A)‖₊
⊢ HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A)) 2 ≤
    ‖a.toProd.1‖₊ * nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A) * ‖b‖₊

Tactic:
calc
      ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by
        simpa only [← sq] using CStarRing.nnnorm_self_mul_star.symm
      _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ :=
        ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
      _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := mul_comm _ _
      _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ :=
        nnnorm_star (a.snd b) ▸ mul_le_mul_left (a.fst.le_opNNNorm _) _

Premises used: Prod.fst, mul_comm, Prod.snd, DFunLike.coe, DoubleCentralizer.toProd, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
⊢ ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.1‖₊ * nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A) * ‖b‖₊

Tactic:
have h2 : ∀ b, ‖a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ := by
    intro b
    calc
      ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by
        simpa only [← sq] using CStarRing.nnnorm_self_mul_star.symm
      _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ :=
        ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
      _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := mul_comm _ _
      _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ :=
        nnnorm_star (a.snd b) ▸ mul_le_mul_left (a.fst.le_opNNNorm _) _
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
h2 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.1‖₊ * nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A) * ‖b‖₊
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖

Tactic:
le_antisymm (h0 _ _ h1) (h0 _ _ h2)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
h0 :
  ∀ (f : A →L[𝕜] A) (C : ℝ≥0),
    (∀ (b : A),
        HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
          C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊) →
      ‖f‖₊ ≤ C
h1 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.2‖₊ * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) b : A) * ‖b‖₊
h2 :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A)) 2 ≤
      ‖a.toProd.1‖₊ * nnnorm (E := A) ((a.toProd.2 : (a : A) → A) b : A) * ‖b‖₊
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖

Tactic:
exact le_antisymm (h0 _ _ h1) (h0 _ _ h2)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.1‖₊ = ‖a.toProd.2‖₊

Tactic:
Subtype.ext <| norm_fst_eq_snd a

Premises used: DoubleCentralizer.norm_fst_eq_snd, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.1‖ = ‖a‖

Tactic:
simp only [norm_def, toProdHom_apply, Prod.norm_def, norm_fst_eq_snd, max_eq_right le_rfl]

Premises used: le_rfl, DoubleCentralizer.norm_fst_eq_snd, DoubleCentralizer.norm_def, Prod.norm_def, max_eq_right, DoubleCentralizer.toProdHom_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
rw : ‖a.toProd.2‖ = ‖a.toProd.1‖
rw₁ rw₂ : ‖a.toProd.2‖ = ‖a.toProd.2‖
⊢ ‖a.toProd.2‖ = ‖a‖

Tactic:
rw [← norm_fst, norm_fst_eq_snd]

Premises used: DoubleCentralizer.norm_fst_eq_snd, DoubleCentralizer.norm_fst
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.1‖₊ = ‖a‖₊

Tactic:
Subtype.ext (norm_fst a)

Premises used: NNReal, DoubleCentralizer.norm_fst, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.2‖₊ = ‖a‖₊

Tactic:
Subtype.ext (norm_snd a)

Premises used: NNReal, DoubleCentralizer.norm_snd, Subtype.ext