awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
Tactic: have (m : ℕ) : 0 ≤ ((2 : ℝ) ^ (-(m : ℤ)) • x m) := smul_nonneg (by positivity) (hx_nonneg m)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have refine : LE.le.{u_2} (α := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
  ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg (this n)) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
⊢ LE.le.{u_2} (α := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
    ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have a : HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n ≤ ∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
⊢ ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖
have obtain : ∀ (C : ℝ≥0)
  (h :
    ∀ (a : A₁),
      norm.{u_2} (E := A₂) ((PositiveLinearMapClass.toPositiveLinearMap f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖),
  ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖
Tactic: obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
⊢ Continuous.{u_1, u_2} (X := A₁) (Y := A₂) (⇑f : (a : A₁) → A₂)
have hbound : ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖
Tactic: have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by
      obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)
      exact ⟨C, h⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
⊢ Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)
have obtain : ∀ (y : Fin 4 → A₁) (hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i) (hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖)
  (hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i),
  Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)
Tactic: obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
x : Fin 4
⊢ star (y x) = y x
have rw : y x = y x
Tactic: rw [IsSelfAdjoint.star_eq (hy_nonneg x).isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
⊢ Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)
have hy' : ∀ (x : Fin 4), star (y x) = y x
Tactic: have hy' : ∀ x : Fin 4, star (y x) = y x := fun x => by
      rw [IsSelfAdjoint.star_eq (hy_nonneg x).isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
hy' : ∀ (x : Fin 4), star (y x) = y x
x : Fin 4
⊢ Eq.{u_2 + 1} (α := A₂) (star ((f : (a : A₁) → A₂) (y x)) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)
have rw : Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (y x) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)
Tactic: rw [IsSelfAdjoint.star_eq (map_nonneg f (hy_nonneg x)).isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
hy' : ∀ (x : Fin 4), star (y x) = y x
⊢ Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)
have hy'' : ∀ (x : Fin 4), Eq.{u_2 + 1} (α := A₂) (star ((f : (a : A₁) → A₂) (y x)) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)
Tactic: have hy'' : ∀ x : Fin 4, star (f (y x)) = f (y x) := fun x => by
      rw [IsSelfAdjoint.star_eq (map_nonneg f (hy_nonneg x)).isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
⊢ IsSelfAdjoint p ↔ IsStarNormal p
have simp : IsStarNormal p → ∀ x ∈ quasispectrum ℂ p, x = (↑x.re : ℂ)
Tactic: simp only [isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts,
    QuasispectrumRestricts.real_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx : x ∈ quasispectrum ℂ p
⊢ x = (↑x.re : ℂ)
have inl : ∀ (hx : x = 0), x = (↑x.re : ℂ)
Tactic: rcases hp.quasispectrum_subset _ hx with (hx | hx)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx : x ∈ quasispectrum ℂ p
inl : ∀ (hx : x = 0), x = (↑x.re : ℂ)
⊢ x = (↑x.re : ℂ)
have inr : ∀ (hx : Membership.mem (γ := Set ℂ) {1} x), x = (↑x.re : ℂ)
Tactic: rcases hp.quasispectrum_subset _ hx with (hx | hx)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (hypothesis)
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, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
have tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
Tactic: tfae_have 1 → 2 := fun h ↦ (hq.mul_right_and_mul_left_of_nonneg_of_le hp.nonneg h).2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (hypothesis)
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
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
have tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
Tactic: tfae_have 2 → 3 := fun h ↦ by
    simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $h)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (hypothesis)
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
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
have tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
Tactic: tfae_have 3 → 4 := hp.sub_of_mul_eq_left hq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (hypothesis)
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)
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
have tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
Tactic: tfae_have 4 → 1 := fun h ↦ by simpa using h.nonneg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (hypothesis)
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
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
have tfae_4_iff_5 : IsStarProjection (q - p) ↔ IsIdempotentElem (q - p)
Tactic: tfae_have 4 ↔ 5 := by simp [isStarProjection_iff, hq.isSelfAdjoint.sub hp.isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (goal)
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
⊢ Commute p q
have rw : p * q = q * p
Tactic: rw [commute_iff_eq, hp.le_iff_mul_eq_right hq |>.mp h, hp.le_iff_mul_eq_left hq |>.mp h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (goal)
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
⊢ Commute p q
have rw₁ : p * q = p
Tactic: rw [commute_iff_eq, hp.le_iff_mul_eq_right hq |>.mp h, hp.le_iff_mul_eq_left hq |>.mp h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Projection (goal)
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
⊢ Commute p q
have rw₂ : p = p
Tactic: rw [commute_iff_eq, hp.le_iff_mul_eq_right hq |>.mp h, hp.le_iff_mul_eq_left hq |>.mp h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) ⊤
have rw : {a : A | 0 ≤ a} ⊆ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
Tactic: rw [eq_top_iff, ← span_nonneg, span_le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
have inl : ∀ (hx : Membership.mem (γ := Set A) {a : A | 0 ≤ a} 0),
  0 ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
Tactic: obtain (rfl | hx_pos) := eq_zero_or_norm_pos x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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)
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
have inr : ∀ (hx_pos : 0 < ‖x‖), x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
Tactic: obtain (rfl | hx_pos) := eq_zero_or_norm_pos x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
have rw : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x ∈
  (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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)
have refine_1 : Membership.mem (γ := Set A) {x : A | 0 ≤ x} (((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x)
Tactic: refine smul_mem _ _ (subset_span <| Set.mem_inter ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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)
⊢ ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x ∈
    (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
have refine_2 : Membership.mem (γ := Set A) (Metric.closedBall 0 r) (((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x)
Tactic: refine smul_mem _ _ (subset_span <| Set.mem_inter ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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)
have refine_1 : Membership.mem (γ := Set A) {x : A | 0 ≤ x} ((r * ‖x‖⁻¹) • x)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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‖
⊢ x ∈ (↑(span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r)) : Set A)
have inr : ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
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']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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‖⁻¹ : ℂ))⁻¹ • ((↑r : ℂ) * (↑‖x‖⁻¹ : ℂ)) • x = x
have inr : (↑r : ℂ) * (↑‖x‖⁻¹ : ℂ) ≠ 0
Tactic: apply inv_smul_smul₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
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
have inr : ¬r * ‖x‖⁻¹ = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r)) ⊤
have 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))
Tactic: rw [eq_top_iff, ← span_nonneg_inter_closedBall (half_pos hr)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
r : ℝ
hr : 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))
have h : Subset.{u_1} (α := Set A) (Metric.closedBall 0 (r / 2)) (Metric.ball 0 r)
Tactic: gcongr