-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)
rw₁₀ 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)
⊢ 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

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' ..]

Premises used: cfc_pow, Real, cfc_const_one, cfc_sub, cfcₙ_eq_cfc, cfc_id', HSub.hSub, cfc_comp', HPow.hPow, Real.sqrt, cfc_real_eq_complex, OfNat.ofNat, cfc_const_mul, cfc_add