awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
h : ∀ i ∈ Insert.insert j s, IsSelfAdjoint (f i)
insert : f j * ∑ i ∈ s, f i = 0
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
i : ι
hi : i ∈ s
⊢ j ≠ i

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
⊢ f j * ∑ i ∈ s, f i = 0

Tactic:
simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)),
    nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
insert :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊)
    (h : ∀ i ∈ Insert.insert j s, IsSelfAdjoint (f i)),
    nnnorm.{u_1} (E := A) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)),
    nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
insert :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊)
    (h : ∀ i ∈ Insert.insert j s, IsSelfAdjoint (f i)),
    nnnorm.{u_1} (E := A) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : StarRing A
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_4)), (↑(characterSpace 𝕜 A) : Type (max u_1 u_4))))
    (compContinuousMap (StarAlgHom.id 𝕜 A)) (ContinuousMap.id (↑(characterSpace 𝕜 A) : Type (max u_1 u_4)))

Tactic:
ContinuousMap.ext fun _a => ext fun _x => rfl

Premises used: WeakDual.CharacterSpace.ext, ContinuousMap.ext, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : StarRing A
inst_5 : NormedRing B
inst_6 : NormedAlgebra 𝕜 B
inst_7 : CompleteSpace B
inst_8 : StarRing B
inst_9 : NormedRing C
inst_10 : NormedAlgebra 𝕜 C
inst_11 : CompleteSpace C
inst_12 : StarRing C
ψ₂ : B →⋆ₐ[𝕜] C
ψ₁ : A →⋆ₐ[𝕜] B
⊢ compContinuousMap (ψ₂.comp ψ₁) = (compContinuousMap ψ₁).comp (compContinuousMap ψ₂)

Tactic:
ContinuousMap.ext fun _a => ext fun _x => rfl

Premises used: WeakDual.CharacterSpace.ext, ContinuousMap.ext, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
B : Type u_2
inst : CommCStarAlgebra A
inst_1 : CommCStarAlgebra B
φ : A →⋆ₐ[ℂ] B
⊢ Eq (α := StarAlgHom.{0, u_1, u_2} ℂ A C((↑(characterSpace ℂ B) : Type u_2), ℂ))
    (StarAlgHom.comp (↑(gelfandStarTransform B) : B →⋆ₐ[ℂ] C((↑(characterSpace ℂ B) : Type u_2), ℂ)) φ)
    (StarAlgHom.comp (ContinuousMap.compStarAlgHom' ℂ ℂ (compContinuousMap φ))
      (↑(gelfandStarTransform A) : A →⋆ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)))

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
X : Type u_1
Y : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : T2Space Y
f : C(X, Y)
⊢ Eq (α := C(X, (↑(characterSpace 𝕜 C(Y, 𝕜)) : Type (max u_2 u_3))))
    (ContinuousMap.comp (↑(homeoEval Y 𝕜) : C(Y, (↑(characterSpace 𝕜 C(Y, 𝕜)) : Type (max u_2 u_3)))) f)
    (ContinuousMap.comp (β := (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_3)))
      (compContinuousMap (ContinuousMap.compStarAlgHom' 𝕜 𝕜 f))
      (↑(homeoEval X 𝕜) : C(X, (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_3)))))

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Set.Mem, ContinuousMap.comp, toContinuousMap, rfl, WeakDual.CharacterSpace.compContinuousMap, AlgHom.toContinuousLinearMap
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
a : f.PreGNS
⊢ (f.toPreGNS : (a : A) → f.PreGNS) ((f.ofPreGNS : (a : f.PreGNS) → A) a) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
a : A
⊢ (f.ofPreGNS : (a : f.PreGNS) → A) ((f.toPreGNS : (a : A) → f.PreGNS) a : f.PreGNS) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
⊢ ∀ (x y : f.PreGNS),
    Eq (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ)
          ((f : (a : A) → ℂ)
              (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) y) : A)
                ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)) :
            ℂ) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) y : A)) :
        ℂ)

Tactic:
simp [← Complex.star_def, ← map_star f]

Premises used: Complex.star_def, StarHomClass.map_star
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
⊢ ∀ (x y : f.PreGNS) (r : ℂ),
    (f : (a : A) → ℂ)
        (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) (r • x)) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) y : A)) =
      HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) r : ℂ)
        ((f : (a : A) → ℂ)
            (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
              ((f.ofPreGNS : (a : f.PreGNS) → A) y : A)) :
          ℂ)

Tactic:
simp [smul_mul_assoc]

Premises used: smul_mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a b : f.PreGNS
⊢ ⟪a, b⟫_ℂ =
    (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) a) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) b : A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : f.PreGNS
⊢ ‖a‖ =
    √(re
        ((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:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : f.PreGNS
⊢ 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 _)
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : f.PreGNS
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)) :
      ℂ)
⊢ 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))

Tactic:
simp [preGNS_norm_def, ← ofReal_pow, Real.sq_sqrt this.1, conj_eq_iff_re.mp this.star_eq]

Premises used: LE.le.star_eq, PositiveLinearMap.preGNS_norm_def, Real.sq_sqrt, Complex.conj_eq_iff_re, And.left, Iff.mp, Complex.ofReal_pow
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
⊢ 0 ≤
    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)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
⊢ 0 ≤ ‖a‖ * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
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) : ℂ)
⊢ 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‖

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]

Premises used: RCLike.ofReal_le_ofReal, sq_le_sq₀, RCLike.ofReal_pow, RCLike.ofReal_eq_complex_ofReal, mul_pow, PositiveLinearMap.preGNS_norm_sq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x : f.PreGNS
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)
⊢ 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:
rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
        smul_mul_assoc]

Premises used: mul_assoc, smul_mul_assoc, sq, CStarRing.norm_star_mul_self, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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) (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:
CStarAlgebra.star_left_conjugate_le_norm_smul

Premises used: CStarAlgebra.star_left_conjugate_le_norm_smul
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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) (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:
exact CStarAlgebra.star_left_conjugate_le_norm_smul

Premises used: CStarAlgebra.star_left_conjugate_le_norm_smul
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)

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
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)) :
      ℂ)

Tactic:
simpa using OrderHomClass.mono f this

Premises used: OrderHomClass.mono
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)
        (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:
simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]

Premises used: smul_mul_assoc, Complex.coe_smul, PositiveLinearMap.preGNS_norm_sq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)
        (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) : ℂ)
⊢ (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:
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]

Premises used: Norm.norm, HMul.hMul, PositiveLinearMap.ofPreGNS, HPow.hPow, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a b : A
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)
⊢ Eq (α := f.PreGNS →L[ℂ] f.PreGNS) (f.leftMulMapPreGNS (a * b)) (f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b)

Tactic:
ext c
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a b : A
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:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
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)
⊢ completion (f.leftMulMapPreGNS (m • x)) =
    HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x))

Tactic:
ext a