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 : 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 : ℕ
negSucc : (cfcUnits (p := p) f a hf' hf ha)⁻¹ ^ (n + 1) = cfcUnits (p := p) (f⁻¹ ^ (n + 1)) a ⋯ ⋯ ha
⊢ cfcUnits (p := p) f a hf' hf ha ^ Int.negSucc n = cfcUnits (p := p) (f ^ Int.negSucc n) a ⋯ ⋯ ha

Tactic:
simp only [zpow_negSucc, ← inv_pow]

Premises used: zpow_negSucc, inv_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
hf : ContinuousOn f (spectrum R a)
ha : p a
n : ℕ
negSucc : (↑((cfcUnits (p := p) f a hf' hf ha)⁻¹ ^ (n + 1)) : A) = (↑(cfcUnits (p := p) (f⁻¹ ^ (n + 1)) a ⋯ ⋯ ha) : A)
⊢ (cfcUnits (p := p) f a hf' hf ha)⁻¹ ^ (n + 1) = cfcUnits (p := p) (f⁻¹ ^ (n + 1)) 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
n : ℕ
⊢ (↑((cfcUnits (p := p) f a hf' hf ha)⁻¹ ^ (n + 1)) : A) = (↑(cfcUnits (p := p) (f⁻¹ ^ (n + 1)) a ⋯ ⋯ ha) : A)

Tactic:
cfc_pow (hf := hf.inv₀ hf') .. |>.symm

Premises used: cfc_pow, ContinuousOn.inv₀, 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
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) (f⁻¹ ^ (n + 1)) a ⋯ ⋯ ha) : A)

Tactic:
exact cfc_pow (hf := hf.inv₀ hf') .. |>.symm

Premises used: cfc_pow, ContinuousOn.inv₀, 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
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℤ
hf : ContinuousOn f (spectrum R a)
ha : p a
ofNat : ∀ (a_1 : ℕ), cfcUnits (p := p) f a hf' hf ha ^ Int.ofNat a_1 = cfcUnits (p := p) (f ^ Int.ofNat a_1) a ⋯ ⋯ ha
negSucc : ∀ (n : ℕ), cfcUnits (p := p) f a hf' hf ha ^ Int.negSucc n = cfcUnits (p := p) (f ^ Int.negSucc n) a ⋯ ⋯ ha
⊢ cfcUnits (p := p) f a hf' hf ha ^ n = cfcUnits (p := p) (f ^ n) a ⋯ ⋯ ha

Tactic:
cases n with
  | ofNat _ => simpa using cfcUnits_pow f a hf' _
  | negSucc n =>
    simp only [zpow_negSucc, ← inv_pow]
    ext
    exact cfc_pow (hf := hf.inv₀ hf') .. |>.symm

Premises used: cfc_pow, zpow_negSucc, inv_pow, cfcUnits_pow, ContinuousOn.inv₀, 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)
n : ℕ
⊢ cfc (p := p) (fun (x : R) ↦ x ^ Int.ofNat n) (↑a : A) = (↑(a ^ Int.ofNat n) : A)

Tactic:
simpa using cfc_pow_id (a : A) n

Premises used: Units.val, cfc_pow_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 : p (↑a : A)
n : ℕ
negSucc : cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = (↑a⁻¹ : A) ^ (n + 1)
⊢ cfc (p := p) (fun (x : R) ↦ x ^ Int.negSucc n) (↑a : A) = (↑(a ^ Int.negSucc n) : A)

Tactic:
simp only [zpow_negSucc, ← inv_pow, Units.val_pow_eq_pow_val]

Premises used: zpow_negSucc, inv_pow, Units.val_pow_eq_pow_val
-- 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)
n : ℕ
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) ^ (n + 1)

Tactic:
have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)
-- 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)
n : ℕ
this : cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) ^ (n + 1)
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = (↑a⁻¹ : A) ^ (n + 1)

Tactic:
this.trans <| congr($(cfc_inv_id a) ^ (n + 1))

Premises used: congrArg, id, cfc_inv_id, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Eq.trans
-- 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)
n : ℕ
this : cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) ^ (n + 1)
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = (↑a⁻¹ : A) ^ (n + 1)

Tactic:
exact this.trans <| congr($(cfc_inv_id a) ^ (n + 1))

Premises used: cfc_inv_id, HAdd.hAdd, OfNat.ofNat, Eq.trans
-- 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ˣ
n : ℤ
ha : p (↑a : A)
ofNat : ∀ (n : ℕ), cfc (p := p) (fun (x : R) ↦ x ^ Int.ofNat n) (↑a : A) = (↑(a ^ Int.ofNat n) : A)
negSucc : ∀ (n : ℕ), cfc (p := p) (fun (x : R) ↦ x ^ Int.negSucc n) (↑a : A) = (↑(a ^ Int.negSucc n) : A)
⊢ cfc (p := p) (fun (x : R) ↦ x ^ n) (↑a : A) = (↑(a ^ n) : A)

Tactic:
cases n with
  | ofNat n => simpa using cfc_pow_id (a : A) n
  | negSucc n =>
    simp only [zpow_negSucc, ← inv_pow, Units.val_pow_eq_pow_val]
    have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)
    exact this.trans <| congr($(cfc_inv_id a) ^ (n + 1))

Premises used: zpow_negSucc, inv_pow, cfc_inv_id, HAdd.hAdd, Units.val_pow_eq_pow_val, OfNat.ofNat
-- 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
inst_11 : UniqueHom R A
f : R → R
a : Aˣ
hf : ContinuousOn f ((fun (x : R) ↦ x⁻¹) '' spectrum R (↑a : A))
ha : p (↑a : A)
rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) Inv.inv (↑a : A)) = cfc (p := p) f (↑a⁻¹ : A)
rw₁ rw₂ : cfc (p := p) f (↑a⁻¹ : A) = cfc (p := p) f (↑a⁻¹ : A)
⊢ cfc (p := p) (fun (x : R) ↦ f x⁻¹) (↑a : A) = cfc (p := p) f (↑a⁻¹ : A)

Tactic:
rw [cfc_comp' .., cfc_inv_id _]

Premises used: cfc_comp', 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
inst_11 : UniqueHom R A
f : R → R
n : ℤ
a : Aˣ
hf : ContinuousOn f ((fun (x : R) ↦ x ^ n) '' spectrum R (↑a : A))
ha : p (↑a : A)
rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ x ^ n) (↑a : A)) = cfc (p := p) f (↑(a ^ n) : A)
rw₁ rw₂ : cfc (p := p) f (↑(a ^ n) : A) = cfc (p := p) f (↑(a ^ n) : A)
⊢ cfc (p := p) (fun (x : R) ↦ f (x ^ n)) (↑a : A) = cfc (p := p) f (↑(a ^ n) : A)

Tactic:
rw [cfc_comp' .., cfc_zpow a]

Premises used: cfc_comp', cfc_zpow
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ f x - g x) a = cfc (p := p) f a - cfc (p := p) g a
neg : ∀ (ha : ¬p a), 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:
by_cases ha : p a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x - g x, 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)
        ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } -
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      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_apply f a, cfc_apply g a, ← map_sub, cfc_apply ..]

Premises used: map_sub, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x - g x, 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)
        ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } -
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (p := p) (fun (x : R) ↦ f x - g x) a = cfc (p := p) f a - cfc (p := p) g a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Premises used: cfc_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
neg : ∀ (h : ¬(p a ∧ ContinuousOn f (spectrum R a))), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a

Tactic:
by_cases h : p a ∧ ContinuousOn f (spectrum R a)

Premises used: spectrum, ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ p a

Tactic:
obtain ⟨ha, hf⟩ := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : p a ∧ ContinuousOn f (spectrum R a)
ha : p a
⊢ ContinuousOn f (spectrum R a)

Tactic:
obtain ⟨ha, hf⟩ := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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)
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ -f x, 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)
        (-{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      A)
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a

Tactic:
rw [cfc_apply f a, ← map_neg, cfc_apply ..]

Premises used: map_neg, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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)
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ -f x, 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)
        (-{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
neg₁ : ∀ (hf : ¬ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a

Tactic:
obtain (ha | hf) := not_and_or.mp h

Premises used: not_and_or, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
ha : ¬p a
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Premises used: cfc_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a

Tactic:
rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, neg_zero]

Premises used: cfc_apply_of_not_continuousOn, neg_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
hf_neg : ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (spectrum R a)
⊢ ContinuousOn f (spectrum R a)

Tactic:
simpa using hf_neg.neg

Premises used: ContinuousOn.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (spectrum R a)

Tactic:
exact fun hf_neg ↦ hf <| by simpa using hf_neg.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
h : ∀ (a : A), cfc (p := p) (-f) a = (-cfc (p := p) f) a
⊢ cfc (p := p) (-f) = -cfc (p := p) f

Tactic:
ext1 a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ cfc (p := p) (-f) a = (-cfc (p := p) f) a

Tactic:
cfc_neg f a

Premises used: cfc_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
⊢ cfc (p := p) (-f) a = (-cfc (p := p) f) a

Tactic:
exact cfc_neg f a

Premises used: cfc_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
a : A
ha : p a
rw : -cfc (p := p) (fun (x : R) ↦ x) a = -a
rw₁ rw₂ : -a = -a
⊢ cfc (p := p) (fun (x : R) ↦ -x) a = -a

Tactic:
rw [cfc_neg _ a, cfc_id' R a]

Premises used: cfc_id', cfc_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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
inst_10 : UniqueHom R A
hf : ContinuousOn f ((fun (x : R) ↦ -x) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) Neg.neg a) = cfc (p := p) f (-a)
rw₁ rw₂ : cfc (p := p) f (-a) = cfc (p := p) f (-a)
⊢ cfc (p := p) (fun (x : R) ↦ f (-x)) a = cfc (p := p) f (-a)

Tactic:
rw [cfc_comp' .., cfc_neg_id _]

Premises used: cfc_comp', cfc_neg_id