awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 x_2 : f.PreGNS
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) (x + x_1)) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
have rw : (f : (a : A) → ℂ)
    (HMul.hMul (β := A)
      (star
        (HAdd.hAdd (α := A) (β := A) ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_1 : A)))
      ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
  HAdd.hAdd (α := ℂ) (β := ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
      ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
      ℂ)
Tactic: rw [map_add, star_add, add_mul, map_add]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 x_2 : f.PreGNS
rw :
  (f : (a : A) → ℂ)
      (HMul.hMul (β := A)
        (star
          (HAdd.hAdd (α := A) (β := A) ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_1 : A)))
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) (x + x_1)) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
have rw₁ : (f : (a : A) → ℂ)
    (HMul.hMul (β := A)
      (HAdd.hAdd (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
        (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A))
      ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
  HAdd.hAdd (α := ℂ) (β := ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
      ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
      ℂ)
Tactic: rw [map_add, star_add, add_mul, map_add]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 x_2 : f.PreGNS
rw :
  (f : (a : A) → ℂ)
      (HMul.hMul (β := A)
        (star
          (HAdd.hAdd (α := A) (β := A) ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_1 : A)))
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
rw₁ :
  (f : (a : A) → ℂ)
      (HMul.hMul (β := A)
        (HAdd.hAdd (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
          (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A))
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) (x + x_1)) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
have rw₂ : (f : (a : A) → ℂ)
    (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A) +
      HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
  HAdd.hAdd (α := ℂ) (β := ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
      ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
      ℂ)
Tactic: rw [map_add, star_add, add_mul, map_add]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : f.PreGNS
⊢ HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2 =
    (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) a) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) a : A))
have this : LE.le (α := ℂ) (0 : ℂ)
  ((f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) a) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) a : A)) :
    ℂ)
Tactic: have : 0 ≤ f (star (f.ofPreGNS a) * f.ofPreGNS a) := f.map_nonneg (star_mul_self_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
⊢ norm (E := f.PreGNS)
      (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
              (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
            (a : f.PreGNS) → f.PreGNS)
          x :
        f.PreGNS) ≤
    ‖a‖ * ‖x‖
have rw : (f : (a : A) → ℂ)
    (HMul.hMul (α := A) (β := A)
      (star
          ((f.ofPreGNS : (a : f.PreGNS) → A)
            (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                    (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                      (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                  (a : f.PreGNS) → f.PreGNS)
                x :
              f.PreGNS)) :
        A)
      ((f.ofPreGNS : (a : f.PreGNS) → A)
          (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                  (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                    (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                (a : f.PreGNS) → f.PreGNS)
              x :
            f.PreGNS) :
        A)) ≤
  (↑(HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)
Tactic: rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, ← RCLike.ofReal_le_ofReal (K := ℂ),
      RCLike.ofReal_pow, RCLike.ofReal_eq_complex_ofReal, preGNS_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
⊢ HMul.hMul (α := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A) (star a) *
      HMul.hMul (β := A) a ((f.ofPreGNS : (a : f.PreGNS) → A) x : A) ≤
    HMul.hMul (β := A)
      (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
      ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
have rw : HMul.hMul (β := A) (HMul.hMul (α := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A) (star a * a))
    ((f.ofPreGNS : (a : f.PreGNS) → A) x : A) ≤
  ‖star a * a‖ •
    HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
      ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
Tactic: rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
        smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A)
        (star
            ((f.ofPreGNS : (a : f.PreGNS) → A)
              (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                      (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                        (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                    (a : f.PreGNS) → f.PreGNS)
                  x :
                f.PreGNS)) :
          A)
        ((f.ofPreGNS : (a : f.PreGNS) → A)
            (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                    (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                      (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                  (a : f.PreGNS) → f.PreGNS)
                x :
              f.PreGNS) :
          A)) ≤
    (↑(HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)
have this : HMul.hMul (α := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A) (star a) *
    HMul.hMul (β := A) a ((f.ofPreGNS : (a : f.PreGNS) → A) x : A) ≤
  HMul.hMul (β := A) (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
    ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
Tactic: have : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤
        ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x := by
      rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
        smul_mul_assoc]
      exact CStarAlgebra.star_left_conjugate_le_norm_smul
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
this :
  HMul.hMul (α := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A) (star a) *
      HMul.hMul (β := A) a ((f.ofPreGNS : (a : f.PreGNS) → A) x : A) ≤
    HMul.hMul (β := A)
      (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
      ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A)
        (star
            ((f.ofPreGNS : (a : f.PreGNS) → A)
              (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                      (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                        (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                    (a : f.PreGNS) → f.PreGNS)
                  x :
                f.PreGNS)) :
          A)
        ((f.ofPreGNS : (a : f.PreGNS) → A)
            (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                    (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                      (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                  (a : f.PreGNS) → f.PreGNS)
                x :
              f.PreGNS) :
          A)) ≤
    (↑(HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)
have _ : LE.le (α := ℂ)
  ((f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A)
        (star
            ((f.ofPreGNS : (a : f.PreGNS) → A)
              (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                      (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                        (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                    (a : f.PreGNS) → f.PreGNS)
                  x :
                f.PreGNS)) :
          A)
        ((f.ofPreGNS : (a : f.PreGNS) → A)
            (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                    (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                      (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                  (a : f.PreGNS) → f.PreGNS)
                x :
              f.PreGNS) :
          A)) :
    ℂ)
  ((f : (a : A) → ℂ)
      (HMul.hMul (β := A)
        (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
        ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)) :
    ℂ)
Tactic: calc
      _ ≤ f (‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x) := by
        simpa using OrderHomClass.mono f this
      _ = _ := by simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
this :
  HMul.hMul (α := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A) (star a) *
      HMul.hMul (β := A) a ((f.ofPreGNS : (a : f.PreGNS) → A) x : A) ≤
    HMul.hMul (β := A)
      (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
      ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
_ :
  LE.le (α := ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A)
          (star
              ((f.ofPreGNS : (a : f.PreGNS) → A)
                (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                        (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                          (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                      (a : f.PreGNS) → f.PreGNS)
                    x :
                  f.PreGNS)) :
            A)
          ((f.ofPreGNS : (a : f.PreGNS) → A)
              (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                      (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                        (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                    (a : f.PreGNS) → f.PreGNS)
                  x :
                f.PreGNS) :
            A)) :
      ℂ)
    ((f : (a : A) → ℂ)
        (HMul.hMul (β := A)
          (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
          ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)) :
      ℂ)
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A)
        (star
            ((f.ofPreGNS : (a : f.PreGNS) → A)
              (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                      (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                        (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                    (a : f.PreGNS) → f.PreGNS)
                  x :
                f.PreGNS)) :
          A)
        ((f.ofPreGNS : (a : f.PreGNS) → A)
            (((↑f.toPreGNS : A →ₗ[ℂ] f.PreGNS) ∘ₗ
                    (↑((ContinuousLinearMap.mul ℂ A : (a : A) → A →L[ℂ] A) a) : A →ₗ[ℂ] A) ∘ₗ
                      (↑f.ofPreGNS : f.PreGNS →ₗ[ℂ] A) :
                  (a : f.PreGNS) → f.PreGNS)
                x :
              f.PreGNS) :
          A)) ≤
    (↑(HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)
have _₁ : (f : (a : A) → ℂ)
    (HMul.hMul (β := A)
      (HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) ‖a‖ 2) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A))
      ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)) =
  (↑(HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)
Tactic: calc
      _ ≤ f (‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x) := by
        simpa using OrderHomClass.mono f this
      _ = _ := by simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a b : A
⊢ Eq (α := f.PreGNS →L[ℂ] f.PreGNS) (f.leftMulMapPreGNS (a * b)) (f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b)
have h : ∀ (c : f.PreGNS),
  Eq (α := f.PreGNS) ((f.leftMulMapPreGNS (a * b) : (a : f.PreGNS) → f.PreGNS) c : f.PreGNS)
    ((f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b : (a : f.PreGNS) → f.PreGNS) c : f.PreGNS)
Tactic: ext c
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
⊢ completion (f.leftMulMapPreGNS (m • x)) =
    HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x))
have h : ∀ (a : Completion f.PreGNS),
  Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
      Completion f.PreGNS)
    ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        a :
      Completion f.PreGNS)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
⊢ IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
have h : Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
  (⇑(completion (f.leftMulMapPreGNS (m • x))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
h :
  Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (m • x))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
⊢ IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
have h₁ : Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
  (⇑(HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x))) :
    (a : Completion f.PreGNS) → Completion f.PreGNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
a : Completion f.PreGNS
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
      Completion f.PreGNS)
    ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        a :
      Completion f.PreGNS)
have h : IsClosed.{u_1} (X := Completion f.PreGNS)
  {a : Completion f.PreGNS |
    Eq (α := Completion f.PreGNS)
      ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
        Completion f.PreGNS)
      ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
            (a : Completion f.PreGNS) → Completion f.PreGNS)
          a :
        Completion f.PreGNS)}
Tactic: induction a using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih a => simp [smul_mul_assoc]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
a : Completion f.PreGNS
h :
  IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
      Completion f.PreGNS)
    ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        a :
      Completion f.PreGNS)
have h₁ : ∀ (a : f.PreGNS),
  Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑a : Completion f.PreGNS) :
      Completion f.PreGNS)
    ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑a : Completion f.PreGNS) :
      Completion f.PreGNS)
Tactic: induction a using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih a => simp [smul_mul_assoc]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ completion (f.leftMulMapPreGNS (x + x_1)) =
    HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1))
have h : ∀ (c : Completion f.PreGNS),
  Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) c :
      Completion f.PreGNS)
    ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        c :
      Completion f.PreGNS)
Tactic: ext c