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 : 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)⁻¹) a * cfc (p := p) f a = 1
have rw : cfc (p := p) (fun (x : R) ↦ (f x)⁻¹ * f x) a = cfc.{u_1, u_2} (R := R) (p := p) 1 a
Tactic: rw [← cfc_mul .., ← cfc_one 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 : 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
⊢ cfcUnits (p := p) f a hf' hf ha ^ n = cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a ⋯ ⋯ ha
have huv : (↑(cfcUnits (p := p) f a hf' hf ha ^ n) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a sorry sorry ha) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ (↑(cfcUnits (p := p) f a hf' hf ha ^ n) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a ⋯ ⋯ ha) : A)
have 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 sorry sorry ha) : A)
Tactic: cases n with
  | zero => simp [cfc_const_one R a]
  | succ n => simp [cfc_pow f _ a]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ (↑(cfcUnits (p := p) f a hf' hf ha ^ n) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ n) a ⋯ ⋯ ha) : A)
have huv₁ : ∀ (n : ℕ),
  (↑(cfcUnits (p := p) f a hf' hf ha ^ (n + 1)) : A) = (↑(cfcUnits (p := p) (fun (x : R) ↦ f x ^ (n + 1)) a sorry sorry ha) : A)
Tactic: cases n with
  | zero => simp [cfc_const_one R a]
  | succ n => simp [cfc_pow f _ a]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)⁻¹) a = (cfc (p := p) f a)⁻¹ʳ
have rw : (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A) = (cfc (p := p) f a)⁻¹ʳ
Tactic: rw [← val_inv_cfcUnits f a hf', ← val_cfcUnits f a hf', Ring.inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)⁻¹ʳ
⊢ cfc (p := p) (fun (x : R) ↦ (f x)⁻¹) a = (cfc (p := p) f a)⁻¹ʳ
have rw₁ : (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A) = (↑(cfcUnits (p := p) f a hf' hf ha) : A)⁻¹ʳ
Tactic: rw [← val_inv_cfcUnits f a hf', ← val_cfcUnits f a hf', Ring.inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)⁻¹ʳ
⊢ cfc (p := p) (fun (x : R) ↦ (f x)⁻¹) a = (cfc (p := p) f a)⁻¹ʳ
have rw₂ : (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A) = (↑(cfcUnits (p := p) f a hf' hf ha)⁻¹ : A)
Tactic: rw [← val_inv_cfcUnits f a hf', ← val_cfcUnits f a hf', Ring.inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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) ↦ x⁻¹) (↑a : A) = (↑a⁻¹ : A)
have rw : cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) = (↑a : A)⁻¹ʳ
Tactic: rw [← Ring.inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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) ↦ x⁻¹) (↑a : A) = (↑a : A)⁻¹ʳ
have h : (↑a : A) = cfc.{u_1, u_2} (R := R) (p := p) id (↑a : A)
Tactic: convert! cfc_inv (id : R → R) (a : 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 : 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)
⊢ cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑a : A) = (↑a : A)⁻¹ʳ
have convert! : ∀ x ∈ spectrum R (↑a : A), id x ≠ 0
Tactic: convert! cfc_inv (id : R → R) (a : 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 : 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⁻¹) a = a⁻¹ʳ
have rw : cfc (p := p) (fun (x : R) ↦ x⁻¹) a = (↑ha_unit.unit⁻¹ : A)
Tactic: rw [Ring.inverse_of_isUnit ha_unit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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⁻¹) a = (↑ha_unit.unit⁻¹ : A)
have change : cfc (p := p) (fun (x : R) ↦ x⁻¹) (↑ha_unit.unit : A) = (↑ha_unit.unit⁻¹ : A)
Tactic: change cfc (fun x ↦ x⁻¹ : R → R) (ha_unit.unit : A) = ha_unit.unit⁻¹
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ cfc (p := p) (fun (x : R) ↦ f x / g x) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
have simp : 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ cfc (p := p) (fun (x : R) ↦ f x * (g x)⁻¹) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
have 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)⁻¹ʳ
Tactic: rw [cfc_mul .., cfc_inv g a hg']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)⁻¹ʳ
⊢ cfc (p := p) (fun (x : R) ↦ f x * (g x)⁻¹) a = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
have rw₁ : cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ = cfc (p := p) f a * (cfc (p := p) g a)⁻¹ʳ
Tactic: rw [cfc_mul .., cfc_inv g a hg']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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 ^ Int.negSucc n = cfcUnits (p := p) (f ^ Int.negSucc n) a ⋯ ⋯ ha
have negSucc : (cfcUnits (p := p) f a hf' hf ha)⁻¹ ^ (n + 1) = cfcUnits (p := p) (f⁻¹ ^ (n + 1)) a sorry sorry ha
Tactic: simp only [zpow_negSucc, ← inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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) = cfcUnits (p := p) (f⁻¹ ^ (n + 1)) a ⋯ ⋯ ha
have negSucc : (↑((cfcUnits (p := p) f a hf' hf ha)⁻¹ ^ (n + 1)) : A) = (↑(cfcUnits (p := p) (f⁻¹ ^ (n + 1)) a sorry sorry ha) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ cfcUnits (p := p) f a hf' hf ha ^ n = cfcUnits (p := p) (f ^ n) a ⋯ ⋯ ha
have ofNat : ∀ (a_1 : ℕ), cfcUnits (p := p) f a hf' hf ha ^ Int.ofNat a_1 = cfcUnits (p := p) (f ^ Int.ofNat a_1) a sorry sorry 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ cfcUnits (p := p) f a hf' hf ha ^ n = cfcUnits (p := p) (f ^ n) a ⋯ ⋯ ha
have negSucc : ∀ (n : ℕ), cfcUnits (p := p) f a hf' hf ha ^ Int.negSucc n = cfcUnits (p := p) (f ^ Int.negSucc n) a sorry sorry 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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.negSucc n) (↑a : A) = (↑(a ^ Int.negSucc n) : A)
have negSucc : cfc (p := p) (fun (x : R) ↦ x⁻¹ ^ (n + 1)) (↑a : A) = (↑a⁻¹ : A) ^ (n + 1)
Tactic: simp only [zpow_negSucc, ← inv_pow, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
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) = (↑a⁻¹ : A) ^ (n + 1)
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ x ^ n) (↑a : A) = (↑(a ^ n) : A)
have ofNat : ∀ (n : ℕ), cfc (p := p) (fun (x : R) ↦ x ^ Int.ofNat n) (↑a : A) = (↑(a ^ Int.ofNat 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))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ x ^ n) (↑a : A) = (↑(a ^ n) : A)
have negSucc : ∀ (n : ℕ), cfc (p := p) (fun (x : R) ↦ x ^ Int.negSucc n) (↑a : A) = (↑(a ^ Int.negSucc 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))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ f x⁻¹) (↑a : A) = cfc (p := p) f (↑a⁻¹ : A)
have rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) Inv.inv (↑a : A)) = cfc (p := p) f (↑a⁻¹ : A)
Tactic: rw [cfc_comp' .., cfc_inv_id _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ f x⁻¹) (↑a : A) = cfc (p := p) f (↑a⁻¹ : A)
have rw₁ : cfc (p := p) f (↑a⁻¹ : A) = cfc (p := p) f (↑a⁻¹ : A)
Tactic: rw [cfc_comp' .., cfc_inv_id _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ f (x ^ n)) (↑a : A) = cfc (p := p) f (↑(a ^ n) : A)
have rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ x ^ n) (↑a : A)) = cfc (p := p) f (↑(a ^ n) : A)
Tactic: rw [cfc_comp' .., cfc_zpow 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 : 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)
⊢ cfc (p := p) (fun (x : R) ↦ f (x ^ n)) (↑a : A) = cfc (p := p) f (↑(a ^ n) : A)
have rw₁ : cfc (p := p) f (↑(a ^ n) : A) = cfc (p := p) f (↑(a ^ n) : A)
Tactic: rw [cfc_comp' .., cfc_zpow 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 : 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)
⊢ cfc (p := p) (fun (x : R) ↦ f x - g x) a = cfc (p := p) f a - cfc (p := p) g a
have 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
Tactic: by_cases ha : p 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 : 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
⊢ cfc (p := p) (fun (x : R) ↦ f x - g x) a = cfc (p := p) f a - cfc (p := p) g a
have 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
Tactic: by_cases ha : p 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 : 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
have 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 := sorry :
        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 := sorry :
          C((↑(spectrum R a) : Type u_1), R) } -
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) }) :
    A)
Tactic: rw [cfc_apply f a, cfc_apply g a, ← map_sub, cfc_apply ..]