awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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 : CompleteSpace A
⊢ IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)
have h : IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
  (⋂ (i : A),
    ⋂ (i_1 : A),
      {x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ |
        HMul.hMul (α := A) ((unop x.2 : (a : A) → A) i : A) i_1 = HMul.hMul (β := A) i ((x.1 : (a : A) → A) i_1 : A)})
Tactic: simp only [range_toProdMulOpposite, Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
have grw : C * (‖f‖₊ * ‖b‖₊) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
Tactic: grw [f.le_opNNNorm b]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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 * (‖f‖₊ * ‖b‖₊) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
have ring_nf : C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2 ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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‖₊
⊢ ‖f‖₊ ≤ C
have h1 : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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
⊢ ‖f‖₊ ≤ C
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖₊ ≤ C
have h₁ : ‖f‖₊ = HPow.hPow (β := ℝ) (HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0)) 2
Tactic: convert! NNReal.rpow_le_rpow this two_pos.le
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ ‖f‖₊ ≤ C
have h₂ : C = HPow.hPow (α := ℝ≥0) (β := ℝ) ((sqrt : (a : ℝ≥0) → ℝ≥0) C : ℝ≥0) 2
Tactic: convert! NNReal.rpow_le_rpow this two_pos.le
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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 (β := ℝ) (HDiv.hDiv (β := ℝ≥0) ‖f‖₊ ((sqrt : (a : ℝ≥0) → ℝ≥0) ‖f‖₊ : ℝ≥0)) 2
have h₁ : ‖f‖₊ = HPow.hPow (β := ℕ) ‖f‖₊ 2 / ‖f‖₊
Tactic: simp only [NNReal.rpow_two, div_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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‖
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖₊
have 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)‖₊
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 _) _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖
have 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‖₊
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 _) _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖₊
have 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)‖₊
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 _) _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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‖₊
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖
have 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‖₊
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 _) _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖
have rw : ‖a.toProd.2‖ = ‖a.toProd.1‖
Tactic: rw [← norm_fst, norm_fst_eq_snd]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖
⊢ ‖a.toProd.2‖ = ‖a‖
have rw₁ : ‖a.toProd.2‖ = ‖a.toProd.2‖
Tactic: rw [← norm_fst, norm_fst_eq_snd]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
have hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
Tactic: have hball : (Metric.closedBall (0 : A) 1).Nonempty :=
        Metric.nonempty_closedBall.2 zero_le_one
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
    ‖a‖₊ * ‖a‖₊
have rw : ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) ((a.toProd.1 : (a : A) → A) y : A)‖₊ ≤
  ‖a‖₊ * ‖a‖₊
Tactic: rw [a.central]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) ((a.toProd.1 : (a : A) → A) y : A)‖₊ ≤
    ‖a‖₊ * ‖a‖₊
have nnnorm_star : ‖a.toProd.1‖₊ * 1 * (‖a.toProd.1‖₊ * 1) ≤ ‖a‖₊ * ‖a‖₊
Tactic: calc
          ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
            nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
          _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
            (mul_le_mul' (a.fst.le_opNorm_of_le ((nnnorm_star x).trans_le hx))
              (a.fst.le_opNorm_of_le hy))
          _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
have key : ∀ (x y : A),
  ‖x‖₊ ≤ 1 →
    ‖y‖₊ ≤ 1 →
      ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
        ‖a‖₊ * ‖a‖₊
Tactic: have key :
        ∀ x y, ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.snd (star (a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊ := by
        intro x y hx hy
        rw [a.central]
        calc
          ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
            nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
          _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
            (mul_le_mul' (a.fst.le_opNorm_of_le ((nnnorm_star x).trans_le hx))
              (a.fst.le_opNorm_of_le hy))
          _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
have rw : ‖(star a * a).toProd.2‖₊ = ‖a‖₊ * ‖a‖₊
Tactic: rw [← nnnorm_snd]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
⊢ ‖(star a * a).toProd.2‖₊ = ‖a‖₊ * ‖a‖₊
have simp : sSup
    ((fun (a_1 : A) ↦
        nnnorm (E := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)) ''
      Metric.closedBall 0 1) =
  ‖a‖₊ * ‖a‖₊
Tactic: simp only [mul_snd, ← sSup_unitClosedBall_eq_nnnorm, star_snd, mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          nnnorm (E := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
have simp : sSup
    ((fun (a_1 : A) ↦
        nnnorm (E := A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A)
              ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A) :
            A →L[𝕜] A)) ''
      Metric.closedBall 0 1) =
  ‖a‖₊ * ‖a‖₊
Tactic: simp only [← @opNNNorm_mul_apply 𝕜 _ A]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          nnnorm (E := A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A)
                ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A) :
              A →L[𝕜] A)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
have simp : sSup
    ((fun (a_1 : A) ↦
        sSup
          ((fun (a_2 : A) ↦
              ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                  a_2‖₊) ''
            Metric.closedBall 0 1)) ''
      Metric.closedBall 0 1) =
  ‖a‖₊ * ‖a‖₊
Tactic: simp only [← sSup_unitClosedBall_eq_nnnorm, mul_apply']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
have refine_1 : ∀ (a_1 : ℝ≥0),
  Membership.mem (γ := Set ℝ≥0)
      ((fun (a_2 : A) ↦
          sSup
            ((fun (a_3 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_2)) : A) : A)
                    a_3‖₊) ''
              Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1)
      a_1 →
    a_1 ≤ ‖a‖₊ * ‖a‖₊
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
refine_1 :
  ∀ (a_1 : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
        ((fun (a_2 : A) ↦
            sSup
              ((fun (a_3 : A) ↦
                  ‖HMul.hMul (α := A)
                      ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_2)) : A) : A) a_3‖₊) ''
                Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1)
        a_1 →
      a_1 ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
have refine_2 : ∀ (r : ℝ≥0) (hr : r < ‖a‖₊ * ‖a‖₊),
  ∃ (a_1 : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
        ((fun (a_2 : A) ↦
            sSup
              ((fun (a_3 : A) ↦
                  ‖HMul.hMul (α := A)
                      ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_2)) : A) : A) a_3‖₊) ''
                Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_