awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : Algebra 𝕜 A
inst_7 : ContinuousFunctionalCalculus 𝕜 A p
inst_8 : Algebra ℝ A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
inst_12 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
rw : spectrum 𝕜 (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a
⊢ spectrum 𝕜 (abs a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a
have rw₁ : spectrum 𝕜 (cfc (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : Algebra 𝕜 A
inst_7 : ContinuousFunctionalCalculus 𝕜 A p
inst_8 : Algebra ℝ A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
inst_12 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
rw : spectrum 𝕜 (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a
rw₁ : spectrum 𝕜 (cfc (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a
⊢ spectrum 𝕜 (abs a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a
have rw₂ : Eq (α := Set 𝕜) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a)
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ abs a = 0 ↔ a = 0
have rw : sqrt (star a * a) = 0 ↔ a = 0
Tactic: rw [CFC.abs, sqrt_eq_zero_iff _, CStarRing.star_mul_self_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : sqrt (star a * a) = 0 ↔ a = 0
⊢ abs a = 0 ↔ a = 0
have rw₁ : star a * a = 0 ↔ a = 0
Tactic: rw [CFC.abs, sqrt_eq_zero_iff _, CStarRing.star_mul_self_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : sqrt (star a * a) = 0 ↔ a = 0
rw₁ : star a * a = 0 ↔ a = 0
⊢ abs a = 0 ↔ a = 0
have rw₂ : a = 0 ↔ a = 0
Tactic: rw [CFC.abs, sqrt_eq_zero_iff _, CStarRing.star_mul_self_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ ‖abs a‖ = ‖a‖
have rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
⊢ ‖abs a‖ = ‖a‖
have rw₁ : ‖abs a‖ * ‖abs a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖abs a‖ * ‖abs a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
⊢ ‖abs a‖ = ‖a‖
have rw₂ : ‖abs a‖ * ‖abs a‖ = ‖a‖ * ‖a‖
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖abs a‖ * ‖abs a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₂ : ‖abs a‖ * ‖abs a‖ = ‖a‖ * ‖a‖
⊢ ‖abs a‖ = ‖a‖
have rw₃ : ‖star (abs a) * abs a‖ = ‖a‖ * ‖a‖
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖abs a‖ * ‖abs a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₂ : ‖abs a‖ * ‖abs a‖ = ‖a‖ * ‖a‖
rw₃ : ‖star (abs a) * abs a‖ = ‖a‖ * ‖a‖
⊢ ‖abs a‖ = ‖a‖
have rw₄ : ‖abs a * abs a‖ = ‖a‖ * ‖a‖
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖abs a‖ * ‖abs a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₂ : ‖abs a‖ * ‖abs a‖ = ‖a‖ * ‖a‖
rw₃ : ‖star (abs a) * abs a‖ = ‖a‖ * ‖a‖
rw₄ : ‖abs a * abs a‖ = ‖a‖ * ‖a‖
⊢ ‖abs a‖ = ‖a‖
have rw₅ : ‖star a * a‖ = ‖a‖ * ‖a‖
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
rw : HPow.hPow (β := ℕ) ‖abs a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖abs a‖ * ‖abs a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₂ : ‖abs a‖ * ‖abs a‖ = ‖a‖ * ‖a‖
rw₃ : ‖star (abs a) * abs a‖ = ‖a‖ * ‖a‖
rw₄ : ‖abs a * abs a‖ = ‖a‖ * ‖a‖
rw₅ : ‖star a * a‖ = ‖a‖ * ‖a‖
⊢ ‖abs a‖ = ‖a‖
have rw₆ : ‖a‖ * ‖a‖ = ‖a‖ * ‖a‖
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
⊢ exp f = { toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ }
have h : ∀ (a : α),
  Eq.{u_1 + 1} (α := 𝕜) ((exp f : (a : α) → 𝕜) a : 𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := sorry : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ Eq.{u_1 + 1} (α := 𝕜) ((exp f : (a : α) → 𝕜) a : 𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
have h : Eq.{u_1 + 1} (α := 𝕜)
  ((∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n : (a : (i : Fin n) → C(α, 𝕜)) → C(α, 𝕜)) fun (x : Fin n) ↦ f : (a : α) → 𝕜) a :
    𝕜)
  (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := sorry : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
Tactic: simp_rw [NormedSpace.exp_eq_expSeries_sum (𝔸 := C(α, 𝕜)) 𝕜, FormalMultilinearSeries.sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n : (a : (i : Fin n) → C(α, 𝕜)) → C(α, 𝕜)) fun (x : Fin n) ↦ f : (a : α) → 𝕜) a :
      𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
have h_sum : Summable (α := C(α, 𝕜)) fun (n : ℕ) ↦
  (expSeries 𝕜 C(α, 𝕜) n : (a : (i : Fin n) → C(α, 𝕜)) → C(α, 𝕜)) fun (x : Fin n) ↦ f
Tactic: have h_sum := NormedSpace.expSeries_summable (𝕂 := 𝕜) f
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum :
  Summable (α := C(α, 𝕜)) fun (n : ℕ) ↦
    (expSeries 𝕜 C(α, 𝕜) n : (a : (i : Fin n) → C(α, 𝕜)) → C(α, 𝕜)) fun (x : Fin n) ↦ f
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n : (a : (i : Fin n) → C(α, 𝕜)) → C(α, 𝕜)) fun (x : Fin n) ↦ f : (a : α) → 𝕜) a :
      𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
have h : Eq.{u_1 + 1} (α := 𝕜) (∑' (i : ℕ), (HSMul.hSMul (α := 𝕜) (↑i.factorial : 𝕜)⁻¹ (f ^ i) : (a : α) → 𝕜) a : 𝕜)
  (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := sorry : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
Tactic: simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ exp a
have rw : 0 ≤ cfc (p := IsSelfAdjoint) Real.exp a
Tactic: rw [← real_exp_eq_normedSpace_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ log (r • a) = HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (log a)
have rw : cfc (p := IsSelfAdjoint) (Real.log ∘ fun (x : ℝ) ↦ r • x) a =
  HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (cfc (p := IsSelfAdjoint) Real.log a)
Tactic: rw [log, ← cfc_smul_id (R := ℝ) r a, ← cfc_comp Real.log (r • ·) a, log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ Real.log r + Real.log z) a =
    HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (cfc (p := IsSelfAdjoint) Real.log a)
have rw : HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (cfc (p := IsSelfAdjoint) Real.log a) =
  HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (cfc (p := IsSelfAdjoint) Real.log a)
Tactic: rw [cfc_const_add _ _ _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ cfc (p := IsSelfAdjoint) (Real.log ∘ fun (x : ℝ) ↦ r • x) a =
    HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (cfc (p := IsSelfAdjoint) Real.log a)
have _ : cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ Real.log r + Real.log z) a =
  HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (cfc (p := IsSelfAdjoint) Real.log a)
Tactic: calc
    _ = cfc (fun z => Real.log r + Real.log z) a :=
      cfc_congr (Real.log_mul hr <| ha₂ · ·)
    _ = _ := by rw [cfc_const_add _ _ _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
⊢ log (a ^ n) = n • log a
have ha₂' : ContinuousOn Real.log (spectrum ℝ a)
Tactic: have ha₂' : ContinuousOn Real.log (spectrum ℝ a) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
⊢ ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
have funProp : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a) x → x ≠ 0
Tactic: fun_prop (disch := aesop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
⊢ log (a ^ n) = n • log a
have ha₂'' : ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
Tactic: have ha₂'' : ContinuousOn Real.log ((· ^ n) '' spectrum ℝ a) := by fun_prop (disch := aesop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
⊢ log (a ^ n) = n • log a
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (x ^ n)) a = n • cfc (p := IsSelfAdjoint) Real.log a
Tactic: rw [log, ← cfc_pow_id (R := ℝ) a n ha₁, ← cfc_comp' Real.log (· ^ n) a ha₂'', log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (x ^ n)) a = n • cfc (p := IsSelfAdjoint) Real.log a
have simp_rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑n : ℝ) * Real.log x) a = n • cfc (p := IsSelfAdjoint) Real.log a
Tactic: simp_rw [Real.log_pow, ← Nat.cast_smul_eq_nsmul ℝ n, cfc_const_mul (n : ℝ) Real.log a ha₂']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)
simp_rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑n : ℝ) * Real.log x) a = n • cfc (p := IsSelfAdjoint) Real.log a
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (x ^ n)) a = n • cfc (p := IsSelfAdjoint) Real.log a
have simp_rw₁ : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑n : ℝ) * Real.log x) a =
  HSMul.hSMul (α := ℝ) (↑n : ℝ) (cfc (p := IsSelfAdjoint) Real.log a)
Tactic: simp_rw [Real.log_pow, ← Nat.cast_smul_eq_nsmul ℝ n, cfc_const_mul (n : ℝ) Real.log a ha₂']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
have funProp : ∀ x ∈ Real.exp '' spectrum ℝ a, x ≠ 0
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ log (exp a) = a
have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
Tactic: have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ log (exp a) = a
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.log (Real.exp x)) a = a
Tactic: rw [log, ← real_exp_eq_normedSpace_exp, ← cfc_comp' Real.log Real.exp a hcont]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
⊢ exp (log a) = a
have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
Tactic: have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
| a
have rw : cfc (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: rw [← cfc_id (R := ℝ) a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = a
have conv_rhs : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = cfc (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: conv_rhs => rw [← cfc_id (R := ℝ) a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
inst_6 : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ Real.exp (Real.log x)) a = cfc (R := ℝ) (p := IsSelfAdjoint) id a
have refine : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a), Real.exp (Real.log x) = id x
Tactic: refine cfc_congr fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ Tendsto (fun (p : ℝ) ↦ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a) (𝓝[>] 0) (𝓝 (log a))
have refine : TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
Tactic: refine tendsto_cfc_fun ?tendsto ?cont
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
refine : TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
⊢ Tendsto (fun (p : ℝ) ↦ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a) (𝓝[>] 0) (𝓝 (log a))
have refine₁ : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)
Tactic: refine tendsto_cfc_fun ?tendsto ?cont
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) (spectrum ℝ a)
have funProp : 0 ≤ p
Tactic: fun_prop (disch := grind -abstractProof)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
funProp : 0 ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) (spectrum ℝ a)
have funProp₁ : (↑0 : ℝ) ≤ p
Tactic: fun_prop (disch := grind -abstractProof)