awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
tfae_4_iff_5 : IsStarProjection (q - p) ↔ IsIdempotentElem (q - p)
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p ≤ q ↔ q * p = p

Tactic:
hp.le_tfae hq |>.out 0 1

Premises used: IsStarProjection.le_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p ≤ q ↔ p * q = p

Tactic:
hp.le_tfae hq |>.out 0 2

Premises used: IsStarProjection.le_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p ≤ q ↔ IsStarProjection (q - p)

Tactic:
hp.le_tfae hq |>.out 0 3

Premises used: IsStarProjection.le_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p ≤ q ↔ IsIdempotentElem (q - p)

Tactic:
hp.le_tfae hq |>.out 0 4

Premises used: IsStarProjection.le_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
h : p ≤ q
rw : p * q = q * p
rw₁ : p * q = p
rw₂ rw₃ : p = p
⊢ Commute p q

Tactic:
rw [commute_iff_eq, hp.le_iff_mul_eq_right hq |>.mp h, hp.le_iff_mul_eq_left hq |>.mp h]

Premises used: commute_iff_eq, IsStarProjection.le_iff_mul_eq_left, Iff.mp, IsStarProjection.le_iff_mul_eq_right
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
rw : {a : A | 0 ≤ a} ⊆ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) ⊤

Tactic:
rw [eq_top_iff, ← span_nonneg, span_le]

Premises used: eq_top_iff, CStarAlgebra.span_nonneg, Submodule.span_le
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
inl :
  ∀ (hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} 0),
    0 ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
inr : ∀ (hx_pos : 0 < ‖x‖), x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
obtain (rfl | hx_pos) := eq_zero_or_norm_pos x

Premises used: eq_zero_or_norm_pos, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} 0
⊢ 0 ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} 0
⊢ 0 ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
rw :
  ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x ∈
    (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
⊢ ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x ∈
    (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
smul_mem _ _ (subset_span <| Set.mem_inter ?_ ?_)

Premises used: Set.Mem, Set.mem_inter, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
refine_1 : Membership.mem (γ := Set A) {x : A | 0 ≤ x} (((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x)
refine_2 : Membership.mem (γ := Set A) (Metric.closedBall 0 r) (((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x)
⊢ ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x ∈
    (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
refine smul_mem _ _ (subset_span <| Set.mem_inter ?_ ?_)

Premises used: Set.mem_inter, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
refine_1 : Membership.mem (γ := Set A) {x : A | 0 ≤ x} ((r * ‖x‖⁻¹) • x)
⊢ Membership.mem (γ := Set A) {x : A | 0 ≤ x} (((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
⊢ 0 ≤ r * ‖x‖⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
⊢ Membership.mem (γ := Set A) {x : A | 0 ≤ x} ((r * ‖x‖⁻¹) • x)

Tactic:
exact smul_nonneg (by positivity) hx

Premises used: smul_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
this : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
⊢ Membership.mem (γ := Set A) (Metric.closedBall 0 r) (((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x)

Tactic:
simp [mul_smul, norm_smul, abs_of_pos hr, inv_mul_cancel₀ hx_pos.ne']

Premises used: norm_smul, LT.lt.ne', abs_of_pos, inv_mul_cancel₀, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
inr : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)

Tactic:
suffices (r * ‖x‖⁻¹ : ℂ)⁻¹ • ((r * ‖x‖⁻¹ : ℂ) • x) = x by
      rw [← this]
      refine smul_mem _ _ (subset_span <| Set.mem_inter ?_ ?_)
      · norm_cast
        exact smul_nonneg (by positivity) hx
      · simp [mul_smul, norm_smul, abs_of_pos hr, inv_mul_cancel₀ hx_pos.ne']
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
inr : (↑r : ℂ) * (↑‖x‖⁻¹ : ℂ) ≠ 0
⊢ ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x

Tactic:
apply inv_smul_smul₀

Premises used: inv_smul_smul₀
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
inr : ¬r * ‖x‖⁻¹ = 0
⊢ (↑r : ℂ) * (↑‖x‖⁻¹ : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} x
hx_pos : 0 < ‖x‖
⊢ ¬r * ‖x‖⁻¹ = 0

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
rw :
  LE.le.{u_1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 (r / 2)))
    (span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r))
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r)) ⊤

Tactic:
rw [eq_top_iff, ← span_nonneg_inter_closedBall (half_pos hr)]

Premises used: eq_top_iff, half_pos, CStarAlgebra.span_nonneg_inter_closedBall
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
h : Subset.{u_1} (α := Set A) (Metric.closedBall 0 (r / 2)) (Metric.ball 0 r)
⊢ LE.le.{u_1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 (r / 2)))
    (span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r))

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Subset.{u_1} (α := Set A) (Metric.closedBall 0 (r / 2)) (Metric.ball 0 r)

Tactic:
Metric.closedBall_subset_ball <| half_lt_self hr

Premises used: half_lt_self, Metric.closedBall_subset_ball
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Subset.{u_1} (α := Set A) (Metric.closedBall 0 (r / 2)) (Metric.ball 0 r)

Tactic:
exact Metric.closedBall_subset_ball <| half_lt_self hr

Premises used: half_lt_self, Metric.closedBall_subset_ball
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 1)) ⊤

Tactic:
span_nonneg_inter_closedBall zero_lt_one

Premises used: zero_lt_one, CStarAlgebra.span_nonneg_inter_closedBall
-- Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 1)) ⊤

Tactic:
span_nonneg_inter_ball zero_lt_one

Premises used: zero_lt_one, CStarAlgebra.span_nonneg_inter_ball
-- 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 :
  (∀ (i : Fin 4),
      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)⁻]
          i)) ∧
    (∀ (i : Fin 4),
        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)⁻]
              i) ≤
          ‖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)
⊢ ∃ (x : Fin 4 → A), (∀ (i : Fin 4), 0 ≤ x i) ∧ (∀ (i : Fin 4), ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i : Fin 4, I ^ (↑i : ℕ) • x i

Tactic:
use ![(realPart a)⁺, (imaginaryPart a)⁺, (realPart a)⁻, (imaginaryPart a)⁻]

Premises used: imaginaryPart, realPart, DFunLike.coe
-- 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 :
  (∀ (x : Fin 4),
      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)⁻]
            x) ∧
        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)⁻]
              x) ≤
          ‖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)
⊢ (∀ (i : Fin 4),
      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)⁻]
          i)) ∧
    (∀ (i : Fin 4),
        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)⁻]
              i) ≤
          ‖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:
rw [← and_assoc, ← forall_and]

Premises used: and_assoc, forall_and
-- 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 :
  ∀ (x : Fin 4),
    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)⁻]
          x) ∧
      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)⁻]
            x) ≤
        ‖a‖
h₁ :
  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)
⊢ (∀ (x : Fin 4),
      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)⁻]
            x) ∧
        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)⁻]
              x) ≤
          ‖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:
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)⁺,
        (↑(((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, ⋯⟩))
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) (⟨0, ⋯⟩ : 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) ⟨0, ⋯⟩)) ∧
    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:
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) ⟨0, ⋯⟩))

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