awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩))
h₁ :
  norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))) ≤
    ‖a‖
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))) ≤
      ‖a‖

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h : LE.le.{u_2} (α := A) 0 (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
⊢ LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0 (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩))
h₁ :
  norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))) ≤
    ‖a‖
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))) ≤
      ‖a‖

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h : LE.le.{u_2} (α := A) 0 (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻
⊢ LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0 (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩))
h₁ :
  norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))) ≤
    ‖a‖
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))) ≤
      ‖a‖

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h : LE.le.{u_2} (α := A) 0 (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻
⊢ LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0 (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
CStarAlgebra.norm_posPart_le _ |>.trans <| realPart.norm_le a

Premises used: Eq.mpr, Fin.cons, realPart.norm_le, Fin.induction.go, CStarAlgebra.norm_posPart_le, Fin.induction, Fin.cases, LE.le.trans, Matrix.vecCons
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
exact CStarAlgebra.norm_posPart_le _ |>.trans <| realPart.norm_le a

Premises used: realPart.norm_le, CStarAlgebra.norm_posPart_le, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
CStarAlgebra.norm_posPart_le _ |>.trans <| imaginaryPart.norm_le a

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, CStarAlgebra.norm_posPart_le, imaginaryPart.norm_le, Fin.induction, Fin.cases, LE.le.trans, Matrix.vecCons
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
exact CStarAlgebra.norm_posPart_le _ |>.trans <| imaginaryPart.norm_le a

Premises used: CStarAlgebra.norm_posPart_le, imaginaryPart.norm_le, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
CStarAlgebra.norm_negPart_le _ |>.trans <| realPart.norm_le a

Premises used: Eq.mpr, Fin.cons, realPart.norm_le, Fin.induction.go, Fin.induction, CStarAlgebra.norm_negPart_le, Fin.cases, LE.le.trans, Matrix.vecCons
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
exact CStarAlgebra.norm_negPart_le _ |>.trans <| realPart.norm_le a

Premises used: realPart.norm_le, CStarAlgebra.norm_negPart_le, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
CStarAlgebra.norm_negPart_le _ |>.trans <| imaginaryPart.norm_le a

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, imaginaryPart.norm_le, Fin.induction, CStarAlgebra.norm_negPart_le, Fin.cases, LE.le.trans, Matrix.vecCons
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ norm.{u_2} (E := A)
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))) ≤
    ‖a‖

Tactic:
exact CStarAlgebra.norm_negPart_le _ |>.trans <| imaginaryPart.norm_le a

Premises used: imaginaryPart.norm_le, CStarAlgebra.norm_negPart_le, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
    ∑ i : Fin 4,
      HSMul.hSMul (β := A) (I ^ (↑i : ℕ))
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          i)
⊢ a =
    ∑ i : Fin 4,
      HSMul.hSMul (β := A) (I ^ (↑i : ℕ))
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          i)

Tactic:
nth_rw 1 [← CStarAlgebra.linear_combination_nonneg a]

Premises used: CStarAlgebra.linear_combination_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
    HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) I 0)
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ +
          HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) I 1)
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ +
        HSMul.hSMul (α := ℂ) (β := A) (-1)
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      HSMul.hSMul (β := A) (-I) (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻
⊢ HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
    ∑ i : Fin 4,
      HSMul.hSMul (β := A) (I ^ (↑i : ℕ))
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          i)

Tactic:
simp only [Fin.sum_univ_four, Fin.coe_ofNat_eq_mod, Matrix.cons_val, Nat.reduceMod, I_sq,
      I_pow_three]

Premises used: Nat.reduceMod, Complex.I_pow_three, Fin.sum_univ_four, Complex.I_sq, Fin.coe_ofNat_eq_mod, Matrix.cons_val
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
    HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) I 0)
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ +
          HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) I 1)
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ +
        HSMul.hSMul (α := ℂ) (β := A) (-1)
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      HSMul.hSMul (β := A) (-I) (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻

Tactic:
module
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
⊢ σ 𝕜 (↑u : E) ⊆ Metric.sphere 0 1

Tactic:
fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm ?_ ?_)

Premises used: Iff.mpr, Set.Mem, mem_sphere_zero_iff_norm, Set.Subset, le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
refine_1 : ∀ (k : 𝕜) (hk : k ∈ σ 𝕜 (↑u : E)), ‖k‖ ≤ 1
refine_2 : ∀ (k : 𝕜) (hk : k ∈ σ 𝕜 (↑u : E)), 1 ≤ ‖k‖
⊢ σ 𝕜 (↑u : E) ⊆ Metric.sphere 0 1

Tactic:
refine fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm ?_ ?_)

Premises used: Iff.mpr, mem_sphere_zero_iff_norm, le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 (↑u : E)
⊢ ‖k‖ ≤ 1

Tactic:
simpa only [CStarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk

Premises used: spectrum.norm_le_norm_of_mem, CStarRing.norm_coe_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 (↑u : E)
⊢ k ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u) : E)

Tactic:
rw [← Unitary.val_toUnits_apply u] at hk

Premises used: Unitary.val_toUnits_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u) : E)
⊢ k ≠ 0

Tactic:
have hnk := ne_zero_of_mem_of_unit hk
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u) : E)
hnk : k ≠ 0
⊢ k⁻¹ ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)

Tactic:
rw [← inv_inv (Unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk

Premises used: Unitary.toUnits, spectrum.map_inv, inv_inv, DFunLike.coe, Set.mem_inv