awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu :
  Membership.mem (γ := Set ↥(unitary A))
    (thickening 2 (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)) u
⊢ Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u
have hu₁ : ∃ (z : ↥(unitary A)),
  Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) z ∧
    dist u z < 2
Tactic: rw [mem_thickening_iff] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu :
  ∃ (z : ↥(unitary A)),
    Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
        z ∧
      dist u z < 2
⊢ Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u
have mp : ∀ (v : ↥(unitary A)) (huv : dist u v < 2) (l : List ↥(selfAdjoint A)) (hlv : (List.map expUnitary l).prod = v),
  Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u
Tactic: obtain ⟨v, ⟨⟨l, (hlv : (l.map expUnitary).prod = v)⟩, huv⟩⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : dist u v < 2
l : List ↥(selfAdjoint A)
hlv : (List.map expUnitary l).prod = v
⊢ Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u
have mp : (fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) (argSelfAdjoint (u * star v) :: l) = u
Tactic: refine ⟨argSelfAdjoint (u * star v) :: l, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
l : List ↥(selfAdjoint A)
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary l).prod
have mpr : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.prod (List.map expUnitary []))
Tactic: induction l with
    | nil => simp
    | cons x xs ih => simpa using (joined_one_expUnitary x).mul ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
l : List ↥(selfAdjoint A)
mpr : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.prod (List.map expUnitary []))
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary l).prod
have mpr₁ : ∀ (x : ↥(selfAdjoint A)) (xs : List ↥(selfAdjoint A))
  (ih : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary xs).prod),
  Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary (x :: xs)).prod
Tactic: induction l with
    | nil => simp
    | cons x xs ih => simpa using (joined_one_expUnitary x).mul ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
⊢ Eq.{u_2 + 1} (α := A ≃ₗᵢ[R] A)
    (let __spread.0 : A ≃ₗ[R] A :=
      (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) 1);
    { toLinearEquiv := __spread.0, norm_map' := ⋯ })
    1
have h : ∀ (x : A),
  Eq (α := A)
    ((let __spread.0 : A ≃ₗ[R] A :=
            (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) 1);
          { toLinearEquiv := __spread.0, norm_map' := sorry } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
x x_1 : ↥(unitary A)
⊢ (let __spread.0 : A ≃ₗ[R] A :=
      (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) (x * x_1) : Aˣ);
    { toLinearEquiv := __spread.0, norm_map' := ⋯ }) =
    HMul.hMul (α := A ≃ₗᵢ[R] A)
      (let __spread.0 : A ≃ₗ[R] A :=
        (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x : Aˣ);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A })
      (let __spread.0 : A ≃ₗ[R] A :=
        (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x_1 : Aˣ);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A })
have h : ∀ (x_2 : A),
  Eq (α := A)
    ((let __spread.0 : A ≃ₗ[R] A :=
            (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) (x * x_1) : Aˣ);
          { toLinearEquiv := __spread.0, norm_map' := sorry } :
          (a : A) → A)
        x_2 :
      A)
    ((HMul.hMul (α := A ≃ₗᵢ[R] A)
            (let __spread.0 : A ≃ₗ[R] A :=
              (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x : Aˣ);
            { toLinearEquiv := __spread.0, norm_map' := sorry : A ≃ₗᵢ[R] A })
            (let __spread.0 : A ≃ₗ[R] A :=
              (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x_1 : Aˣ);
            { toLinearEquiv := __spread.0, norm_map' := sorry : A ≃ₗᵢ[R] A }) :
          (a : A) → A)
        x_2 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u : ↥(unitary A)
⊢ Eq.{u_2 + 1} (α := A ≃ₗᵢ[R] A) (LinearIsometryEquiv.symm ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u))
    ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (star u))
have h : ∀ (x : A),
  Eq (α := A) ((LinearIsometryEquiv.symm ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u) : (a : A) → A) x : A)
    ((((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (star u) : A ≃ₗᵢ[R] A) : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
⊢ Eq (α := A ≃ₗᵢ[R] A) (LinearIsometryEquiv.symm (mulRight R u)) (mulRight R (star u))
have h : ∀ (x : A),
  Eq (α := A) ((LinearIsometryEquiv.symm (mulRight R u) : (a : A) → A) x : A)
    ((mulRight R (star u) : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u v : ↥(unitary A)
⊢ Eq (α := A ≃ₗᵢ[R] A) (LinearIsometryEquiv.trans (mulRight R u) (mulRight R v)) (mulRight R (u * v))
have h : ∀ (x : A),
  Eq (α := A) ((LinearIsometryEquiv.trans (mulRight R u) (mulRight R v) : (a : A) → A) x : A)
    ((mulRight R (u * v) : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
⊢ Eq (α := A ≃ₗᵢ[R] A) (mulRight R 1) (LinearIsometryEquiv.refl R A)
have h : ∀ (x : A), Eq (α := A) ((mulRight R 1 : (a : A) → A) x : A) ((LinearIsometryEquiv.refl R A : (a : A) → A) x : A)
Tactic: ext
-- 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
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
have inl : Subsingleton A → Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- 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
inl : Subsingleton A → Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
have inr : Nontrivial A → Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- 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
⊢ a + I • CFC.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) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
Tactic: rw [CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg]
-- 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 : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
⊢ a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
have rw₁ : 0 ≤ 1 - HPow.hPow (β := ℕ) a 2
Tactic: rw [CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg]
-- 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
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) a 2
have rwa : HPow.hPow (β := ℕ) a 2 ≤ 1
Tactic: rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
-- 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
rwa : HPow.hPow (β := ℕ) a 2 ≤ 1
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) a 2
have rwa₁ : ‖HPow.hPow (β := ℕ) a 2‖ ≤ 1
Tactic: rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
-- 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
rwa : HPow.hPow (β := ℕ) a 2 ≤ 1
rwa₁ : ‖HPow.hPow (β := ℕ) a 2‖ ≤ 1
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) a 2
have rwa₂ : ‖a * a‖ ≤ 1
Tactic: rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
-- 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
rwa : HPow.hPow (β := ℕ) a 2 ≤ 1
rwa₁ : ‖HPow.hPow (β := ℕ) a 2‖ ≤ 1
rwa₂ : ‖a * a‖ ≤ 1
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) a 2
have rwa₃ : HPow.hPow (β := ℕ) ‖a‖ 2 ≤ 1
Tactic: rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
-- 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
⊢ 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) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ 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' ..]
-- 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
⊢ 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) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a +
    I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(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' ..]
-- 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
⊢ 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) =
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a +
    I • cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑√(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' ..]
-- 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
⊢ 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 := IsStarNormal) (fun (x : ℂ) ↦ (↑√(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' ..]
-- 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
⊢ 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 : ℝ) ↦ √(1 - 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
⊢ 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 : ℝ) ↦ √(1 - 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
⊢ 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 - 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' ..]