awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 1
⊢ cfc (p := p) f a ≤ 1
have apply : ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
  LE.le.{u_2} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    (1 : A)
Tactic: apply cfc_cases (· ≤ 1) _ _ (by simp) fun hf ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 1
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ LE.le.{u_2} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    (1 : A)
have rw : LE.le.{u_2} (α := A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) 1 : A)
Tactic: rw [← map_one (cfcHom ha (R := R))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 1
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ LE.le.{u_2} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) 1 : A)
have apply : { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
    C((↑(spectrum R a) : Type u_1), R) } ≤
  1
Tactic: apply cfcHom_mono ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f g : C((↑(spectrum R a) : Type u_1), R)
⊢ LE.le.{u_2} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A) ↔
    f ≤ g
have rw : 0 ≤
    HSub.hSub (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A)
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
  f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f g : C((↑(spectrum R a) : Type u_1), R)
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A) ↔
    f ≤ g
have rw₁ : LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (g - f) : A) ↔ f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f g : C((↑(spectrum R a) : Type u_1), R)
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    f ≤ g
rw₁ :
  LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (g - f) : A) ↔ f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A) ↔
    f ≤ g
have rw₂ : 0 ≤ g - f ↔ f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f g : C((↑(spectrum R a) : Type u_1), R)
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    f ≤ g
rw₁ :
  LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (g - f) : A) ↔ f ≤ g
rw₂ : 0 ≤ g - f ↔ f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A) ↔
    f ≤ g
have rw₃ : f ≤ g ↔ f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (p := p) f a ≤ cfc (p := p) g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x
have rw : (∀ (a_1 : (↑(spectrum R a) : Type u_1)),
    LE.le (α := R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          a_1 :
        R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          a_1 :
        R)) ↔
  ∀ x ∈ spectrum R a, f x ≤ g x
Tactic: rw [cfc_apply f a, cfc_apply g a, cfcHom_le_iff (show p a from ha), ContinuousMap.le_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0
have simp_rw : 0 ≤ cfc (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x
Tactic: simp_rw [← neg_nonneg, ← cfc_neg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) f a ≤ (algebraMap R A : (a : R) → A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r
have rw : cfc (p := p) f a ≤ cfc (p := p) (fun (x : R) ↦ r) a ↔ ∀ x ∈ spectrum R a, f x ≤ r
Tactic: rw [← cfc_const r a, cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : cfc (p := p) f a ≤ cfc (p := p) (fun (x : R) ↦ r) a ↔ ∀ x ∈ spectrum R a, f x ≤ r
⊢ cfc (p := p) f a ≤ (algebraMap R A : (a : R) → A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r
have rw₁ : (∀ x ∈ spectrum R a, f x ≤ r) ↔ ∀ x ∈ spectrum R a, f x ≤ r
Tactic: rw [← cfc_const r a, cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (algebraMap R A : (a : R) → A) r ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, r ≤ f x
have rw : cfc (p := p) (fun (x : R) ↦ r) a ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, r ≤ f x
Tactic: rw [← cfc_const r a, cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ r) a ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, r ≤ f x
⊢ (algebraMap R A : (a : R) → A) r ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, r ≤ f x
have rw₁ : (∀ x ∈ spectrum R a, r ≤ f x) ↔ ∀ x ∈ spectrum R a, r ≤ f x
Tactic: rw [← cfc_const r a, cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ a ≤ (algebraMap R A : (a : R) → A) r ↔ ∀ x ∈ spectrum R a, x ≤ r
have nth_rw : cfc.{u_1, u_2} (R := R) (p := p) id a ≤ (algebraMap R A : (a : R) → A) r ↔ ∀ x ∈ spectrum R a, x ≤ r
Tactic: nth_rw 1 [← cfc_id R a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ (algebraMap R A : (a : R) → A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x
have nth_rw : (algebraMap R A : (a : R) → A) r ≤ cfc.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ spectrum R a, r ≤ x
Tactic: nth_rw 1 [← cfc_id R a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = 1 ∧ cfc (p := p) f a * star (cfc (p := p) f a) = 1 ↔
    ∀ x ∈ spectrum R a, star (f x) * f x = 1
have rw : Set.EqOn (β := R) (fun (x : R) ↦ star (f x) * f x) 1 (spectrum R a) ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1
Tactic: rw [← IsStarNormal.cfc_map (p := p) f a |>.star_comm_self |>.eq, and_self, ← cfc_one R a,
    ← cfc_star, ← cfc_mul .., cfc_eq_cfc_iff_eqOn]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
⊢ Membership.mem (γ := Submonoid A) (unitary A) u ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
have rw : IsStarNormal u ∧ Membership.mem (γ := Submonoid A) (unitary A) u ↔
  IsStarNormal u ∧ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
Tactic: rw [← and_iff_right_of_imp isStarNormal_of_mem_unitary]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
⊢ IsStarNormal u ∧ Membership.mem (γ := Submonoid A) (unitary A) u ↔
    IsStarNormal u ∧ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
have refine : ∀ (hu : IsStarNormal u), Membership.mem (γ := Submonoid A) (unitary A) u ↔ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
Tactic: refine and_congr_right fun hu ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
hu : IsStarNormal u
⊢ Membership.mem (γ := Submonoid A) (unitary A) u ↔ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
have nth_rw : Membership.mem (γ := Submonoid A) (unitary A) (cfc (R := ℂ) (p := IsStarNormal) id u) ↔
  spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
Tactic: nth_rw 1 [← cfc_id ℂ u]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
hu : IsStarNormal u
⊢ Membership.mem (γ := Submonoid A) (unitary A) (cfc (R := ℂ) (p := IsStarNormal) id u) ↔
    spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
have rw : (∀ x ∈ spectrum ℂ u, star (id x) * id x = 1) ↔ ∀ x ∈ spectrum ℂ u, x ∈ (↑(unitary ℂ) : Set ℂ)
Tactic: rw [cfc_unitary_iff id u, Set.subset_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
⊢ Eq.{u_1 + 1} (α := ↥(unitary A)) (expUnitary 0) 1
have a : Eq.{u_1 + 1} (α := A) (↑(expUnitary 0) : A) (↑1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
⊢ Continuous.{u_1, u_1} (X := ↥(selfAdjoint A)) expUnitary
have simp : Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))
Tactic: simp only [continuous_induced_rng, Function.comp_def, selfAdjoint.expUnitary_coe]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
⊢ Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))
have let : ∀ (this : NormedAlgebra ℚ A), Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))
Tactic: let +nondep : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute (↑a : A) (↑b : A)
⊢ expUnitary (a + b) = expUnitary a * expUnitary b
have let : ∀ (this : NormedAlgebra ℚ A), expUnitary (a + b) = expUnitary a * expUnitary b
Tactic: let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute (↑a : A) (↑b : A)
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
have rw : SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)
Tactic: rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute (↑a : A) (↑b : A)
rw : SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
have rw₁ : selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
Tactic: rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute (↑a : A) (↑b : A)
rw : SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)
rw₁ : selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
have rw₂ : selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
Tactic: rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute (↑a : A) (↑b : A)
rw : SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)
rw₁ : selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
rw₂ : selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
have rw₃ : selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary (b + a)
Tactic: rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Exponential (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : StarRing A
inst_3 : ContinuousStar A
inst_4 : CompleteSpace A
inst_5 : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute (↑a : A) (↑b : A)
rw : SemiconjBy (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b) (selfAdjoint.expUnitary b)
rw₁ : selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
rw₂ : selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
rw₃ : selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary (b + a)
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
have rw₄ : selfAdjoint.expUnitary (b + a) = selfAdjoint.expUnitary (b + a)
Tactic: rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]