awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
rw :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      cfc (p := IsStarNormal) (fun (x : ℂ) ↦ I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₁ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₂ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₃ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₄ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₅ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₆ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2) a)
⊢ a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
have rw₇ : a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
  a +
    I •
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
        (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) a)
Tactic: rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
rw :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      cfc (p := IsStarNormal) (fun (x : ℂ) ↦ I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₁ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₂ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₃ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₄ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₅ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₆ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2) a)
rw₇ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
            cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) a)
⊢ a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
have rw₈ : a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
  a +
    I •
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
        (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
          HPow.hPow (β := ℕ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a) 2)
Tactic: rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
rw :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      cfc (p := IsStarNormal) (fun (x : ℂ) ↦ I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₁ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₂ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₃ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₄ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₅ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₆ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2) a)
rw₇ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
            cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) a)
rw₈ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
            HPow.hPow (β := ℕ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a) 2)
⊢ a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
have rw₉ : a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
  a +
    I •
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
        (1 - HPow.hPow (β := ℕ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a) 2)
Tactic: rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
rw :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      cfc (p := IsStarNormal) (fun (x : ℂ) ↦ I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₁ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₂ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a +
      I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₃ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₄ :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₅ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)) a
rw₆ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2) a)
rw₇ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
            cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) a)
rw₈ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a -
            HPow.hPow (β := ℕ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a) 2)
rw₉ :
  a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    a +
      I •
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x)
          (1 - HPow.hPow (β := ℕ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a) 2)
⊢ a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
have rw₁₀ : a + I • cfc (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
  a + I • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) (1 - HPow.hPow (β := ℕ) a 2)
Tactic: rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
have key : a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
Tactic: have key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x : ℂ ↦ x.re + I * √(1 - x.re ^ 2)) a := by
    rw [CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg]
    case nonneg =>
      rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
    rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
key :
  a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
have inr : ∀ x ∈ spectrum ℂ a,
  star ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) *
      ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) =
    1
Tactic: rw [key, cfc_unitary_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
key :
  a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ star ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) *
      ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) =
    1
have inr : ‖x.re‖ ≤ 1
Tactic: rw [← starRingEnd_apply, ← Complex.normSq_eq_conj_mul_self,
    Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
⊢ x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
have rw : x =
  ‖x‖ •
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑u₁ : A)) : A) +
      HSMul.hSMul (β := A) I (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑u₂ : A)) : A))
Tactic: rw [smul_add, smul_comm _ I, Unitary.coe_star, Unitary.coe_star,
    ← realPart_apply_coe (u₁ : A), ← realPart_apply_coe (u₂ : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
have inl : ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ),
  Eq.{u_1 + 1} (α := A) 0 (∑ i : Fin 4, c i • (↑(u i) : A)) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ norm.{u_1} (E := A) 0 / 2
Tactic: obtain (rfl | hx) := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
inl :
  ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ),
    Eq.{u_1 + 1} (α := A) 0 (∑ i : Fin 4, c i • (↑(u i) : A)) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ norm.{u_1} (E := A) 0 / 2
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
have inr : ∀ (hx : x ≠ 0),
  ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
Tactic: obtain (rfl | hx) := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
have this : have u₁ :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) sorry;
have u₂ :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) sorry;
x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
Tactic: have := norm_smul_two_inv_smul_add_four_unitary x hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
have h : x =
    ∑ i : Fin 4,
      ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A) ∧
  ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
Tactic: use ![u₁, star u₁, u₂, star u₂], ![‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹ * I, ‖x‖ * 2⁻¹ * I]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
⊢ x =
      ∑ i : Fin 4,
        ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
          (↑(![u₁, star u₁, u₂, star u₂] i) : A) ∧
    ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
have h : x =
  ∑ i : Fin 4,
    ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
      (↑(![u₁, star u₁, u₂, star u₂] i) : A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h_1 : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
h :
  x =
    ∑ i : Fin 4,
      ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)
⊢ x =
      ∑ i : Fin 4,
        ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
          (↑(![u₁, star u₁, u₂, star u₂] i) : A) ∧
    ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
have h₁ : ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
| x
have rw : ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
⊢ x =
    ∑ i : Fin 4,
      ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)
have h : ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A))) =
  ∑ i : Fin 4,
    ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
      (↑(![u₁, star u₁, u₂, star u₂] i) : A)
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
⊢ ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A))) =
    ∑ i : Fin 4,
      ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)
have h : (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (↑u₁ : A) + (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (star (↑u₁ : A)) +
    ((↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (I • (↑u₂ : A)) +
      (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (I • star (↑u₂ : A))) =
  ((↑‖x‖ : ℂ) * 2⁻¹) • (↑u₁ : A) + ((↑‖x‖ : ℂ) * 2⁻¹) • star (↑u₁ : A) + ((↑‖x‖ : ℂ) * 2⁻¹ * I) • (↑u₂ : A) +
    ((↑‖x‖ : ℂ) * 2⁻¹ * I) • star (↑u₂ : A)
Tactic: simp [Fin.sum_univ_four, ← Complex.coe_smul]