awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
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
⊢ a ≤ (algebraMap R A : (a : R) → A) r ↔ ∀ x ∈ spectrum R a, x ≤ r

Tactic:
nth_rw 1 [← cfc_id R a]

Premises used: cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ 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:
cfc_le_algebraMap_iff id r a

Premises used: cfc_le_algebraMap_iff, id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ 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:
exact cfc_le_algebraMap_iff id r a

Premises used: cfc_le_algebraMap_iff, id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
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
⊢ (algebraMap R A : (a : R) → A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
nth_rw 1 [← cfc_id R a]

Premises used: cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 ≤ cfc.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
algebraMap_le_cfc_iff id r a

Premises used: id, algebraMap_le_cfc_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 ≤ cfc.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
exact algebraMap_le_cfc_iff id r a

Premises used: id, algebraMap_le_cfc_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 ≤ 1 ↔ ∀ x ∈ spectrum R a, f x ≤ 1

Tactic:
simpa using cfc_le_algebraMap_iff f 1 a

Premises used: cfc_le_algebraMap_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ 1 ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, 1 ≤ f x

Tactic:
simpa using algebraMap_le_cfc_iff f 1 a

Premises used: OfNat.ofNat, algebraMap_le_cfc_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ a ≤ 1 ↔ ∀ x ∈ spectrum R a, x ≤ 1

Tactic:
simpa using le_algebraMap_iff_spectrum_le (r := (1 : R)) (a := a)

Premises used: le_algebraMap_iff_spectrum_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ 1 ≤ a ↔ ∀ x ∈ spectrum R a, 1 ≤ x

Tactic:
simpa using algebraMap_le_iff_le_spectrum (r := (1 : R)) (a := a)

Premises used: algebraMap_le_iff_le_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
s : Set R
hs : spectrum R a ⊆ s
⊢ Continuous[_, inst_7] (⇑(cfcHomSuperset (p := p) ha (s := s) hs) : (a : C((↑s : Type u_1), R)) → A)

Tactic:
(cfcHom_continuous ha).comp <| ContinuousMap.continuous_precomp _

Premises used: cfcHom_continuous, Continuous.comp, ContinuousMap.continuous_precomp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
s : Set R
hs : spectrum R a ⊆ s
⊢ (cfcHomSuperset (p := p) ha (s := s) hs : (a : C((↑s : Type u_1), R)) → A) (restrict s (ContinuousMap.id R)) = a

Tactic:
cfcHom_id ha

Premises used: spectrum, Set.Mem, cfcHom_id, setOf, ContinuousMap.comp, Not, ContinuousMap.restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ClosedEmbeddingContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(spectrum R a) : Type u_1), R)) (Y := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
ClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding a ha

Premises used: ClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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)
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
⊢ 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

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]

Premises used: and_self, IsStarNormal.star_comm_self, cfc_eq_cfc_iff_eqOn, cfc_one, cfc_mul, cfc_star, Commute.eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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)
⊢ 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:
Iff.rfl

Premises used: Iff.rfl, Set.EqOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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)
⊢ 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:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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
rw :
  IsStarNormal u ∧ Membership.mem (γ := Submonoid A) (unitary A) u ↔
    IsStarNormal u ∧ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
⊢ Membership.mem (γ := Submonoid A) (unitary A) u ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)

Tactic:
rw [← and_iff_right_of_imp isStarNormal_of_mem_unitary]

Premises used: isStarNormal_of_mem_unitary, and_iff_right_of_imp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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 ℂ)

Tactic:
and_congr_right fun hu ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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
refine :
  ∀ (hu : IsStarNormal u), Membership.mem (γ := Submonoid A) (unitary A) u ↔ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
⊢ IsStarNormal u ∧ Membership.mem (γ := Submonoid A) (unitary A) u ↔
    IsStarNormal u ∧ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)

Tactic:
refine and_congr_right fun hu ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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
nth_rw :
  Membership.mem (γ := Submonoid A) (unitary A) (cfc (R := ℂ) (p := IsStarNormal) id u) ↔
    spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
⊢ Membership.mem (γ := Submonoid A) (unitary A) u ↔ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)

Tactic:
nth_rw 1 [← cfc_id ℂ u]

Premises used: cfc_id, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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
rw : (∀ x ∈ spectrum ℂ u, star (id x) * id x = 1) ↔ ∀ x ∈ spectrum ℂ u, x ∈ (↑(unitary ℂ) : Set ℂ)
⊢ Membership.mem (γ := Submonoid A) (unitary A) (cfc (R := ℂ) (p := IsStarNormal) id u) ↔
    spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)

Tactic:
rw [cfc_unitary_iff id u, Set.subset_def]

Premises used: Set.subset_def, id, cfc_unitary_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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
⊢ (∀ x ∈ spectrum ℂ u, star (id x) * id x = 1) ↔ ∀ x ∈ spectrum ℂ u, x ∈ (↑(unitary ℂ) : Set ℂ)

Tactic:
simp only [id_eq, RCLike.star_def, SetLike.mem_coe, Unitary.mem_iff_star_mul_self]

Premises used: RCLike.star_def, Unitary.mem_iff_star_mul_self, SetLike.mem_coe, id_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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
inst_5 : IsStarNormal u
hu : spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)
⊢ Membership.mem (γ := Submonoid A) (unitary A) u

Tactic:
unitary_iff_isStarNormal_and_spectrum_subset_unitary.mpr ⟨‹_›, hu⟩

Premises used: Iff.mpr, And.intro, unitary_iff_isStarNormal_and_spectrum_subset_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
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 : Membership.mem (γ := Submonoid A) (unitary A) u
⊢ spectrum ℂ u ⊆ (↑(unitary ℂ) : Set ℂ)

Tactic:
unitary_iff_isStarNormal_and_spectrum_subset_unitary.mp hu |>.right

Premises used: And.right, unitary_iff_isStarNormal_and_spectrum_subset_unitary, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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 : Eq.{u_1 + 1} (α := A) (↑(expUnitary 0) : A) (↑1 : A)
⊢ Eq.{u_1 + 1} (α := ↥(unitary A)) (expUnitary 0) 1

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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} (α := A) (↑(expUnitary 0) : A) (↑1 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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
simp : Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))
⊢ Continuous.{u_1, u_1} (X := ↥(selfAdjoint A)) expUnitary

Tactic:
simp only [continuous_induced_rng, Function.comp_def, selfAdjoint.expUnitary_coe]

Premises used: Function.comp_def, selfAdjoint.expUnitary_coe, continuous_induced_rng
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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
let : ∀ (this : NormedAlgebra ℚ A), Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))
⊢ Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))

Tactic:
let +nondep : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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
this : NormedAlgebra ℚ A
⊢ Continuous (Y := A) fun (x : ↥(selfAdjoint A)) ↦ exp (I • (↑x : A))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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)
let : ∀ (this : NormedAlgebra ℚ A), expUnitary (a + b) = expUnitary a * expUnitary b
⊢ expUnitary (a + b) = expUnitary a * expUnitary b

Tactic:
let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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)
this : NormedAlgebra ℚ A
⊢ expUnitary (a + b) = expUnitary a * expUnitary b

Tactic:
simpa only [Subtype.ext_iff, expUnitary_coe, AddSubgroup.coe_add, smul_add] using
    exp_add_of_commute ((h.smul_left I).smul_right I)

Premises used: Commute.smul_left, Subtype.ext_iff, AddSubgroup.coe_add, Commute.smul_right, NormedSpace.exp_add_of_commute, smul_add, selfAdjoint.expUnitary_coe, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Exponential
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)
rw₄ rw₅ : selfAdjoint.expUnitary (b + a) = selfAdjoint.expUnitary (b + a)
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)

Tactic:
rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]

Premises used: SemiconjBy, Commute, add_comm, Commute.symm, Commute.expUnitary_add
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
simp :
  IsStarProjection e ↔
    (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ IsStarProjection e ↔ Membership.mem (γ := Set A) (extremePoints ℝ ({x : A | 0 ≤ x} ∩ closedBall 0 1)) e

Tactic:
simp only [mem_closedBall_zero_iff, mem_extremePoints_iff_left, mem_inter_iff,
    mem_setOf_eq, and_imp]

Premises used: mem_extremePoints_iff_left, and_imp, Set.mem_inter_iff, Set.mem_setOf_eq, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
⊢ IsStarProjection e ↔
    (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e

Tactic:
⟨fun he ↦ ⟨⟨he.nonneg, he.norm_le⟩,
    fun a ha ha1 b hb hb1 ⟨t, s, h0t, h0s, hts, hlin⟩ ↦ ?_⟩, fun ⟨⟨h1, h2⟩, h3⟩ ↦ ?_⟩

Premises used: IsStarProjection.norm_le, _private.0.isStarProjection_iff_mem_extremePoints_setOf_nonneg_inter_unitClosedBall.match_4, And.intro, Iff.intro, _private.0.isStarProjection_iff_mem_extremePoints_setOf_nonneg_inter_unitClosedBall.match_5, Eq, IsStarProjection, IsStarProjection.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
refine_1 :
  ∀ (he : IsStarProjection e) (a : A) (ha : 0 ≤ a) (ha1 : ‖a‖ ≤ 1) (b : A) (hb : 0 ≤ b) (hb1 : ‖b‖ ≤ 1),
    e ∈ openSegment ℝ a b → ∀ (t s : ℝ) (h0t : 0 < t) (h0s : 0 < s) (hts : t + s = 1) (hlin : t • a + s • b = e), a = e
refine_2 :
  ((0 ≤ e ∧ ‖e‖ ≤ 1) ∧
      ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e) →
    ∀ (h1 : 0 ≤ e) (h2 : ‖e‖ ≤ 1)
      (h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e),
      IsStarProjection e
⊢ IsStarProjection e ↔
    (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e

Tactic:
refine ⟨fun he ↦ ⟨⟨he.nonneg, he.norm_le⟩,
    fun a ha ha1 b hb hb1 ⟨t, s, h0t, h0s, hts, hlin⟩ ↦ ?_⟩, fun ⟨⟨h1, h2⟩, h3⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A) ∧
    Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)

Tactic:
grind [inr_mem_Icc_iff_norm_le]

Premises used: CStarAlgebra.inr_mem_Icc_iff_norm_le
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)

Tactic:
have ⟨ha01, hb01⟩ : (a : A⁺¹) ∈ Icc 0 1 ∧ (b : A⁺¹) ∈ Icc 0 1 := by
      grind [inr_mem_Icc_iff_norm_le]
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
h : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑a : Unitization ℂ A)
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑b : Unitization ℂ A)

Tactic:
have ⟨ha01, hb01⟩ : (a : A⁺¹) ∈ Icc 0 1 ∧ (b : A⁺¹) ∈ Icc 0 1 := by
      grind [inr_mem_Icc_iff_norm_le]