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 : 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 : ContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ContinuousOn f (spectrum R a)
pos : cfc (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfc (p := p) (fun (x : R) ↦ f x * star (f x)) a
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)

Tactic:
rw [← cfc_star, ← cfc_mul .., ← cfc_mul ..]

Premises used: cfc_mul, cfc_star
-- 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 : ContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ContinuousOn f (spectrum R a)
pos : ∀ (x : R), star (f x) * f x = f x * star (f x)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfc (p := p) (fun (x : R) ↦ f x * star (f x)) a

Tactic:
congr! 2
-- 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 : ContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ContinuousOn f (spectrum R a)
x : R
⊢ star (f x) * f x = f x * star (f x)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- 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 : ContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ContinuousOn f (spectrum R a)
x : R
⊢ star (f x) * f x = f x * star (f x)

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- 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 : ContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ¬ContinuousOn f (spectrum R a)
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)

Tactic:
simp [cfc_apply_of_not_continuousOn a h]

Premises used: cfc_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
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
inst_9 : ContinuousFunctionalCalculus R A IsSelfAdjoint
f : R → R
a : A
⊢ IsSelfAdjoint (cfc (p := IsSelfAdjoint) f a)

Tactic:
cfc_predicate _ _

Premises used: cfc_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
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
inst_9 : LE A
inst_10 : ContinuousFunctionalCalculus R A fun (x : A) ↦ 0 ≤ x
f : R → R
a : A
⊢ 0 ≤ cfc (p := fun (x : A) ↦ 0 ≤ x) f a

Tactic:
cfc_predicate _ _

Premises used: cfc_predicate
-- 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 : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
a : A
ha : p a
⊢ (spectrum R a).Nonempty

Tactic:
ContinuousFunctionalCalculus.spectrum_nonempty a ha

Premises used: ContinuousFunctionalCalculus.spectrum_nonempty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : 0 ∉ f '' spectrum R a ↔ ∀ x ∈ spectrum R a, f x ≠ 0
⊢ IsUnit (cfc (p := p) f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0

Tactic:
rw [← spectrum.zero_notMem_iff R, cfc_map_spectrum ..]

Premises used: spectrum.zero_notMem_iff, cfc_map_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 0 ∉ f '' spectrum R a ↔ ∀ x ∈ spectrum R a, f x ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ f x * (f x)⁻¹) a = cfc.{u_1, u_2} (R := R) (p := p) 1 a
⊢ cfc (p := p) f a * cfc (p := p) (fun (x : R) ↦ (f x)⁻¹) a = 1

Tactic:
rw [← cfc_mul .., ← cfc_one R a]

Premises used: cfc_one, cfc_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
x : R
h : x ∈ spectrum R a
⊢ f x * (f x)⁻¹ = 1 x

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f x * (f x)⁻¹) a = cfc.{u_1, u_2} (R := R) (p := p) 1 a

Tactic:
exact cfc_congr fun _ _ ↦ by aesop

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ (f x)⁻¹ * f x) a = cfc.{u_1, u_2} (R := R) (p := p) 1 a
⊢ cfc (p := p) (fun (x : R) ↦ (f x)⁻¹) a * cfc (p := p) f a = 1

Tactic:
rw [← cfc_mul .., ← cfc_one R a]

Premises used: cfc_one, cfc_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
x : R
h : x ∈ spectrum R a
⊢ (f x)⁻¹ * f x = 1 x

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ (f x)⁻¹ * f x) a = cfc.{u_1, u_2} (R := R) (p := p) 1 a

Tactic:
exact cfc_congr fun _ _ ↦ by aesop

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : ContinuousOn f (spectrum R a)
ha : p a
huv : (↑(cfcUnits (p := p) f a hf' hf ha ^ n) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a ⋯ ⋯ ha) : A)
⊢ cfcUnits (p := p) f a hf' hf ha ^ n = cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a ⋯ ⋯ ha

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (↑(HPow.hPow (β := ℕ) (cfcUnits (p := p) f a hf' hf ha) 0) : A) =
    (↑(cfcUnits (p := p) (fun (x : R) ↦ HPow.hPow (β := ℕ) (f x) 0) a ⋯ ⋯ ha) : A)

Tactic:
simp [cfc_const_one R a]

Premises used: cfc_const_one
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
n : ℕ
⊢ (↑(cfcUnits (p := p) f a hf' hf ha ^ (n + 1)) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ (n + 1)) a ⋯ ⋯ ha) : A)

Tactic:
simp [cfc_pow f _ a]

Premises used: cfc_pow
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : ContinuousOn f (spectrum R a)
ha : p a
huv :
  (↑(HPow.hPow (β := ℕ) (cfcUnits (p := p) f a hf' hf ha) 0) : A) =
    (↑(cfcUnits (p := p) (fun (x : R) ↦ HPow.hPow (β := ℕ) (f x) 0) a ⋯ ⋯ ha) : A)
huv₁ :
  ∀ (n : ℕ),
    (↑(cfcUnits (p := p) f a hf' hf ha ^ (n + 1)) : A) =
      (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ (n + 1)) a ⋯ ⋯ ha) : A)
⊢ (↑(cfcUnits (p := p) f a hf' hf ha ^ n) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a ⋯ ⋯ ha) : A)

Tactic:
cases n with
  | zero => simp [cfc_const_one R a]
  | succ n => simp [cfc_pow f _ a]

Premises used: cfc_pow, cfc_const_one
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A) = (cfc (p := p) f a)⁻¹ʳ
rw₁ : (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A) = (↑(cfcUnits (p := p) f a hf' hf ha) : A)⁻¹ʳ
rw₂ rw₃ : (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A) = (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A)
⊢ cfc (p := p) (fun (x : R) ↦ (f x)⁻¹) a = (cfc (p := p) f a)⁻¹ʳ

Tactic:
rw [← val_inv_cfcUnits f a hf', ← val_cfcUnits f a hf', Ring.inverse_unit]

Premises used: val_cfcUnits, Ring.inverse_unit, val_inv_cfcUnits
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
rw : cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) = (↑a : A)⁻¹ʳ
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) = (↑a⁻¹ : A)

Tactic:
rw [← Ring.inverse_unit]

Premises used: Ring.inverse_unit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
⊢ cfc (p := p) (fun (x : R) ↦ (id x)⁻¹) (↑a : A) = (cfc.{u_1, u_2} (R := R) (p := p) id (↑a : A))⁻¹ʳ

Tactic:
cfc_inv (id : R → R) (a : A) ?_

Premises used: Units.val, id, cfc_inv
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
h : (↑a : A) = cfc.{u_1, u_2} (R := R) (p := p) id (↑a : A)
convert! : ∀ x ∈ spectrum R (↑a : A), id x ≠ 0
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) = (↑a : A)⁻¹ʳ

Tactic:
convert! cfc_inv (id : R → R) (a : A) ?_

Premises used: Units.val, id, cfc_inv
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
⊢ (↑a : A) = cfc.{u_1, u_2} (R := R) (p := p) id (↑a : A)

Tactic:
(cfc_id R (a : A)).symm

Premises used: Units.val, cfc_id, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
⊢ (↑a : A) = cfc.{u_1, u_2} (R := R) (p := p) id (↑a : A)

Tactic:
exact (cfc_id R (a : A)).symm

Premises used: Units.val, cfc_id, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
hx : 0 ∈ spectrum R (↑a : A)
⊢ False

Tactic:
spectrum.zero_notMem R a.isUnit hx

Premises used: spectrum.zero_notMem, Units.isUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : Aˣ
ha : p (↑a : A)
hx : 0 ∈ spectrum R (↑a : A)
⊢ False

Tactic:
exact spectrum.zero_notMem R a.isUnit hx

Premises used: spectrum.zero_notMem, Units.isUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : A
ha_unit : IsUnit a
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ x⁻¹) a = (↑ha_unit.unit⁻¹ : A)
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) a = a⁻¹ʳ

Tactic:
rw [Ring.inverse_of_isUnit ha_unit]

Premises used: Ring.inverse_of_isUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : A
ha_unit : IsUnit a
ha : p a
change : cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑ha_unit.unit : A) = (↑ha_unit.unit⁻¹ : A)
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) a = (↑ha_unit.unit⁻¹ : A)

Tactic:
change cfc (fun x ↦ x⁻¹ : R → R) (ha_unit.unit : A) = ha_unit.unit⁻¹

Premises used: Units.val, cfc, Inv.inv, IsUnit.unit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : A
ha_unit : IsUnit a
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑ha_unit.unit : A) = (↑ha_unit.unit⁻¹ : A)

Tactic:
cfc_inv_id _ ha

Premises used: cfc_inv_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
a : A
ha_unit : IsUnit a
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑ha_unit.unit : A) = (↑ha_unit.unit⁻¹ : A)

Tactic:
exact cfc_inv_id _ ha

Premises used: cfc_inv_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
simp : cfc (p := p) (fun (x : R) ↦ f x * (g x)⁻¹) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
⊢ cfc (p := p) (fun (x : R) ↦ f x / g x) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
rw : cfc (p := p) f a * cfc (p := p) (fun (x : R) ↦ (g x)⁻¹) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
rw₁ rw₂ : cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
⊢ cfc (p := p) (fun (x : R) ↦ f x * (g x)⁻¹) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ

Tactic:
rw [cfc_mul .., cfc_inv g a hg']

Premises used: cfc_inv, cfc_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Ring A
inst_2 : TopologicalSpace R
inst_3 : ContinuousInv₀ R
inst_4 : Algebra R A
a : Aˣ
⊢ spectrum R (↑a : A) ⊆ {0}ᶜ

Tactic:
simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_notMem R a.isUnit

Premises used: Set.subset_compl_singleton_iff, spectrum.zero_notMem, Units.isUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Ring A
inst_2 : TopologicalSpace R
inst_3 : ContinuousInv₀ R
inst_4 : Algebra R A
inst_5 : ContinuousMul R
a : Aˣ
n : ℤ
⊢ spectrum R (↑a : A) ⊆ {0}ᶜ

Tactic:
simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_notMem R a.isUnit

Premises used: Set.subset_compl_singleton_iff, spectrum.zero_notMem, Units.isUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield 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
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
a_1 : ℕ
⊢ cfcUnits (p := p) f a hf' hf ha ^ Int.ofNat a_1 = cfcUnits (p := p) (f ^ Int.ofNat a_1) a ⋯ ⋯ ha

Tactic:
simpa using cfcUnits_pow f a hf' _

Premises used: cfcUnits_pow