awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
⊢ IsStarProjection e ↔ Membership.mem (γ := Set A) (extremePoints ℝ ({x : A | 0 ≤ x} ∩ closedBall 0 1)) e
have simp : IsStarProjection e ↔
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
Tactic: simp only [mem_closedBall_zero_iff, mem_extremePoints_iff_left, mem_inter_iff,
    mem_setOf_eq, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
⊢ IsStarProjection e ↔
    (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
have refine_1 : ∀ (he : IsStarProjection e) (a : A) (ha : 0 ≤ a) (ha1 : ‖a‖ ≤ 1) (b : A) (hb : 0 ≤ b) (hb1 : ‖b‖ ≤ 1),
  e ∈ openSegment ℝ a b → ∀ (t s : ℝ) (h0t : 0 < t) (h0s : 0 < s) (hts : t + s = 1) (hlin : t • a + s • b = e), a = e
Tactic: refine ⟨fun he ↦ ⟨⟨he.nonneg, he.norm_le⟩,
    fun a ha ha1 b hb hb1 ⟨t, s, h0t, h0s, hts, hlin⟩ ↦ ?_⟩, fun ⟨⟨h1, h2⟩, h3⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
refine_1 :
  ∀ (he : IsStarProjection e) (a : A) (ha : 0 ≤ a) (ha1 : ‖a‖ ≤ 1) (b : A) (hb : 0 ≤ b) (hb1 : ‖b‖ ≤ 1),
    e ∈ openSegment ℝ a b → ∀ (t s : ℝ) (h0t : 0 < t) (h0s : 0 < s) (hts : t + s = 1) (hlin : t • a + s • b = e), a = e
⊢ IsStarProjection e ↔
    (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
have refine_2 : ((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),
    IsStarProjection e
Tactic: refine ⟨fun he ↦ ⟨⟨he.nonneg, he.norm_le⟩,
    fun a ha ha1 b hb hb1 ⟨t, s, h0t, h0s, hts, hlin⟩ ↦ ?_⟩, fun ⟨⟨h1, h2⟩, h3⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (hypothesis)
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
⊢ a = e
have ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
Tactic: have ⟨ha01, hb01⟩ : (a : A⁺¹) ∈ Icc 0 1 ∧ (b : A⁺¹) ∈ Icc 0 1 := by
      grind [inr_mem_Icc_iff_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (hypothesis)
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)
⊢ a = e
have hb01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)
Tactic: have ⟨ha01, hb01⟩ : (a : A⁺¹) ∈ Icc 0 1 ∧ (b : A⁺¹) ∈ Icc 0 1 := by
      grind [inr_mem_Icc_iff_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ a = e
have rw : e * t • a * e = t • e
Tactic: rw [← h0t.ne'.isUnit.smul_left_cancel, ← he.conjugate_of_nonneg_of_le
          (smul_nonneg h0t.le ha) ?hae]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ a = e
have rw₁ : t • a ≤ e
Tactic: rw [← h0t.ne'.isUnit.smul_left_cancel, ← he.conjugate_of_nonneg_of_le
          (smul_nonneg h0t.le ha) ?hae]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ e * t • a * e = t • e
have apply : Eq (α := Unitization ℂ A) (↑(t • e) : Unitization ℂ A) (↑(e * t • a * e) : Unitization ℂ A)
Tactic: apply inr_injective (R := ℂ) <| Eq.symm ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ a = e
have refine_1 : t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)) = 0
have apply : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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))
have refine : 0 ≤ (↑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 ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)) +
      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)
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ 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)))
have match_scalars : t * 1 + s * 1 = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ 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)))
have match_scalars₁ : -(t * 1) = -(t * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ 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)))
have match_scalars₂ : -(s * 1) = -(s * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)) ≤ 0
have _ : 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: 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)) ≤ 0
have _₁ : 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: 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ t • ((↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) * (↑e : Unitization ℂ A)) ≤ 0
have _₂ : (↑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: 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (hypothesis)
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
⊢ 0 ≤ (↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)
have this : 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])
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ 0 ≤ HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)
have grw : LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 2
Tactic: grw [sub_nonneg, this, one_le_two]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ 0 ≤ HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)
have grw₁ : LE.le.{u_1} (α := Unitization ℂ A) 1 2
Tactic: grw [sub_nonneg, this, one_le_two]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ 0 ≤ HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)
have grw₂ : LE.le.{u_1} (α := Unitization ℂ A) 2 2
Tactic: grw [sub_nonneg, this, one_le_two]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ 0 ≤ (↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A)
have apply : Commute (↑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])