awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
this :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
rw : e * t • a * e = t • e
rw₁ : t • a ≤ e
⊢ a = e

Tactic:
rw [← h0t.ne'.isUnit.smul_left_cancel, ← he.conjugate_of_nonneg_of_le
          (smul_nonneg h0t.le ha) ?hae]

Premises used: smul_nonneg, Ne.isUnit, IsStarProjection.conjugate_of_nonneg_of_le, LT.lt.le, LT.lt.ne', IsUnit.smul_left_cancel
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
this :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
⊢ 0 ≤ s • b

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
this :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
⊢ t • a ≤ e

Tactic:
simpa [hlin] using le_add_of_nonneg_right (a := t • a) (by positivity : 0 ≤ s • b)

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
this :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
⊢ t • a ≤ e

Tactic:
case hae => simpa [hlin] using le_add_of_nonneg_right (a := t • a) (by positivity : 0 ≤ s • b)

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
this :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
apply : Eq (α := Unitization ℂ A) (↑(t • e) : Unitization ℂ A) (↑(e * t • a * e) : Unitization ℂ A)
⊢ e * t • a * e = t • e

Tactic:
apply inr_injective (R := ℂ) <| Eq.symm ?_

Premises used: Unitization.inr_injective, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
this :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
⊢ Eq (α := Unitization ℂ A) (↑(t • e) : Unitization ℂ A) (↑(e * t • a * e) : Unitization ℂ A)

Tactic:
simpa only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, sub_eq_zero,
        smul_mul_assoc, mul_smul_comm, smul_sub, inr_mul, inr_smul]

Premises used: IsStarProjection.isIdempotentElem, sub_eq_zero, Unitization.inr_mul, Unitization.inr_smul, smul_mul_assoc, mul_one_sub_mul, IsStarProjection.inr, smul_sub, mul_smul_comm, IsIdempotentElem.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
refine_1 :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
⊢ a = e

Tactic:
suffices t • (e * (1 - a : A⁺¹) * e) = 0 by
      rw [← h0t.ne'.isUnit.smul_left_cancel, ← he.conjugate_of_nonneg_of_le
          (smul_nonneg h0t.le ha) ?hae]
      case hae => simpa [hlin] using le_add_of_nonneg_right (a := t • a) (by positivity : 0 ≤ s • b)
      apply inr_injective (R := ℂ) <| Eq.symm ?_
      simpa only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, sub_eq_zero,
        smul_mul_assoc, mul_smul_comm, smul_sub, inr_mul, inr_smul]
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ 0 ≤ HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A)

Tactic:
simpa using ha01.2

Premises used: And.right
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
apply :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) ≤ 0
⊢ t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0

Tactic:
apply le_antisymm ?_ <| smul_nonneg h0t.le <| he.inr.isSelfAdjoint.conjugate_nonneg <| by
      simpa using ha01.2

Premises used: smul_nonneg, IsSelfAdjoint.conjugate_nonneg, LT.lt.le, le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) ≤
    t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      s • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A))

Tactic:
le_add_of_nonneg_right <| smul_nonneg h0s.le ?_

Premises used: smul_nonneg, LT.lt.le, le_add_of_nonneg_right
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
refine : 0 ≤ (↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A)
⊢ t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) ≤
    t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      s • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A))

Tactic:
refine le_add_of_nonneg_right <| smul_nonneg h0s.le ?_

Premises used: smul_nonneg, LT.lt.le, le_add_of_nonneg_right
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ norm (E := Unitization ℂ A) (↑b : Unitization ℂ A) ≤ 1

Tactic:
simpa [norm_inr]

Premises used: Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ 0 ≤ (↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A)

Tactic:
simpa [mul_one_sub_mul] using he.inr.isSelfAdjoint.conjugate_le_conjugate <|
          norm_le_one_iff_of_nonneg (b : A⁺¹) (by simpa) |>.mp (by simpa [norm_inr])

Premises used: Unitization.inr, IsSelfAdjoint.conjugate_le_conjugate, mul_one_sub_mul, Iff.mp, CStarAlgebra.norm_le_one_iff_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
simp :
  HSMul.hSMul (β := Unitization ℂ A) t (↑e : Unitization ℂ A) -
        t • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      (HSMul.hSMul (β := Unitization ℂ A) s (↑e : Unitization ℂ A) -
        s • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A))) =
    (↑e : Unitization ℂ A) -
      (t • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
        s • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A)))
⊢ t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      s •
        ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A)) =
    (↑e : Unitization ℂ A) -
      (↑e : Unitization ℂ A) *
          (HSMul.hSMul (β := Unitization ℂ A) t (↑a : Unitization ℂ A) +
            HSMul.hSMul (β := Unitization ℂ A) s (↑b : Unitization ℂ A)) *
        (↑e : Unitization ℂ A)

Tactic:
simp only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, mul_add,
          Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc]

Premises used: add_mul, Algebra.mul_smul_comm, IsStarProjection.isIdempotentElem, mul_one_sub_mul, IsStarProjection.inr, smul_sub, Algebra.smul_mul_assoc, mul_add, IsIdempotentElem.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
match_scalars : t * 1 + s * 1 = 1
match_scalars₁ : -(t * 1) = -(t * 1)
match_scalars₂ : -(s * 1) = -(s * 1)
⊢ HSMul.hSMul (β := Unitization ℂ A) t (↑e : Unitization ℂ A) -
        t • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      (HSMul.hSMul (β := Unitization ℂ A) s (↑e : Unitization ℂ A) -
        s • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A))) =
    (↑e : Unitization ℂ A) -
      (t • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
        s • (HMul.hMul (α := Unitization ℂ A) (↑e : Unitization ℂ A) (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A)))

Tactic:
match_scalars
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ t * 1 + s * 1 = 1

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ -(t * 1) = -(t * 1)

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ -(s * 1) = -(s * 1)

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
⊢ (↑e : Unitization ℂ A) -
      (↑e : Unitization ℂ A) *
          (HSMul.hSMul (β := Unitization ℂ A) t (↑a : Unitization ℂ A) +
            HSMul.hSMul (β := Unitization ℂ A) s (↑b : Unitization ℂ A)) *
        (↑e : Unitization ℂ A) =
    0

Tactic:
simp [← inr_smul, ← inr_add, hlin, ← inr_mul, he.isIdempotentElem.eq]

Premises used: IsStarProjection.isIdempotentElem, Unitization.inr_mul, Unitization.inr_smul, Unitization.inr_add, IsIdempotentElem.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
_ :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) ≤
    t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      s • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A))
_₁ :
  t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) +
      s •
        ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A) * (↑e : Unitization ℂ A)) =
    (↑e : Unitization ℂ A) -
      (↑e : Unitization ℂ A) *
          (HSMul.hSMul (β := Unitization ℂ A) t (↑a : Unitization ℂ A) +
            HSMul.hSMul (β := Unitization ℂ A) s (↑b : Unitization ℂ A)) *
        (↑e : Unitization ℂ A)
_₂ :
  (↑e : Unitization ℂ A) -
      (↑e : Unitization ℂ A) *
          (HSMul.hSMul (β := Unitization ℂ A) t (↑a : Unitization ℂ A) +
            HSMul.hSMul (β := Unitization ℂ A) s (↑b : Unitization ℂ A)) *
        (↑e : Unitization ℂ A) =
    0
⊢ t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) ≤ 0

Tactic:
calc
      _ ≤ t • (e * (1 - a : A⁺¹) * e) + s • (e * (1 - b) * e) := by
        refine le_add_of_nonneg_right <| smul_nonneg h0s.le ?_
        simpa [mul_one_sub_mul] using he.inr.isSelfAdjoint.conjugate_le_conjugate <|
          norm_le_one_iff_of_nonneg (b : A⁺¹) (by simpa) |>.mp (by simpa [norm_inr])
      _ = e - e * (t • a + s • b) * e := by
        simp only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, mul_add,
          Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc]
        match_scalars <;> grind
      _ = 0 := by simp [← inr_smul, ← inr_add, hlin, ← inr_mul, he.isIdempotentElem.eq]

Premises used: HMul.hMul, HSub.hSub, Unitization.inr, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ LE.le (α := Unitization ℂ A) 0 (↑e : Unitization ℂ A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ norm (E := Unitization ℂ A) (↑e : Unitization ℂ A) ≤ 1

Tactic:
simpa [norm_inr]

Premises used: Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 1

Tactic:
have : (e : A⁺¹) ≤ 1 := norm_le_one_iff_of_nonneg _ (by simpa) |>.mp (by simpa [norm_inr])
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 1
⊢ LE.le (α := Unitization ℂ A) 0 (↑e : Unitization ℂ A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 1
grw : LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 2
grw₁ : LE.le.{u_1} (α := Unitization ℂ A) 1 2
grw₂ grw₃ : LE.le.{u_1} (α := Unitization ℂ A) 2 2
⊢ 0 ≤ HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)

Tactic:
grw [sub_nonneg, this, one_le_two]

Premises used: one_le_two, sub_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 1
apply : Commute (↑e : Unitization ℂ A) (HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A))
⊢ 0 ≤ (↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)

Tactic:
apply Commute.mul_nonneg (by simpa) (by grw [sub_nonneg, this, one_le_two])

Premises used: Commute.mul_nonneg