awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
U : ↥(unitary A)
⊢ abs (↑U : A) = 1

Tactic:
simp [abs]

Premises used: CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
U : A
hU : Membership.mem (γ := Submonoid A) (unitary A) U
⊢ abs U = 1

Tactic:
abs_coe_unitary ⟨U, hU⟩

Premises used: CFC.abs_coe_unitary, Subtype.mk
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
⊢ Eq.{u_2 + 1} (α := A) (abs 1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
x : ℝ≥0
⊢ Eq (α := A) (abs ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) x) : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) x : A)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
n : ℕ
⊢ Eq.{u_2 + 1} (α := A) (abs (↑n : A)) (↑n : A)

Tactic:
simpa only [map_natCast, Nat.abs_cast] using abs_algebraMap_nnreal (n : ℝ≥0)

Premises used: Nat.abs_cast, Nat.cast, map_natCast, CFC.abs_algebraMap_nnreal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
n : ℕ
inst_11 : n.AtLeastTwo
⊢ Eq.{u_2 + 1} (α := A) (abs (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
simpa using abs_natCast n

Premises used: CFC.abs_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
a : ℕ
⊢ Eq.{u_2 + 1} (α := A) (abs (↑(Int.ofNat a) : A)) (↑|Int.ofNat a| : A)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
n : ℕ
negSucc : Eq.{u_2 + 1} (α := A) (↑(↑(n + 1) : ℤ) : A) (↑|Int.negSucc n| : A)
⊢ Eq.{u_2 + 1} (α := A) (abs (↑(Int.negSucc n) : A)) (↑|Int.negSucc n| : A)

Tactic:
rw [Int.cast_negSucc, abs_neg, abs_natCast, ← Int.cast_natCast]

Premises used: Int.cast_natCast, CFC.abs_neg, CFC.abs_natCast, Int.cast_negSucc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
n : ℕ
⊢ Eq.{u_2 + 1} (α := A) (↑(↑(n + 1) : ℤ) : A) (↑|Int.negSucc n| : A)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : StarModule ℝ A
n : ℤ
ofNat : ∀ (a : ℕ), Eq.{u_2 + 1} (α := A) (abs (↑(Int.ofNat a) : A)) (↑|Int.ofNat a| : A)
negSucc : ∀ (n : ℕ), Eq.{u_2 + 1} (α := A) (abs (↑(Int.negSucc n) : A)) (↑|Int.negSucc n| : A)
⊢ Eq.{u_2 + 1} (α := A) (abs (↑n : A)) (↑|n| : A)

Tactic:
cases n with
  | ofNat _ => simp
  | negSucc n =>
    rw [Int.cast_negSucc, abs_neg, abs_natCast, ← Int.cast_natCast]
    congr

Premises used: Int.cast_natCast, CFC.abs_neg, CFC.abs_natCast, Int.cast_negSucc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
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 : Algebra ℝ A
inst_8 : NonnegSpectrumClass ℝ A
inst_9 : IsTopologicalRing A
inst_10 : T2Space A
inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_12 : StarModule 𝕜 A
inst_13 : StarModule ℝ A
inst_14 : IsScalarTower ℝ 𝕜 A
c : 𝕜
⊢ Eq.{u_2 + 1} (α := A) (abs ((algebraMap 𝕜 A : (a : 𝕜) → A) c) : A) ((algebraMap ℝ A : (a : ℝ) → A) ‖c‖ : A)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a)
rw : cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a)
rw₁ : cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (cfc (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a)
rw₂ rw₃ : cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a
⊢ cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (abs a)

Tactic:
rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, ← cfc_comp' ..]

Premises used: CFC.abs_eq_cfcₙ_coe_norm, cfcₙ_eq_cfc, cfc_comp'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : TopologicalSpace A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
rw : abs a * abs a = star a * a
rw₁ rw₂ : star a * a = star a * a
⊢ HPow.hPow (β := ℕ) (abs a) 2 = star a * a

Tactic:
rw [sq, abs_mul_abs]

Premises used: sq, CFC.abs_mul_abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
rw₂ rw₃ : Eq (α := Set 𝕜) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a)
⊢ spectrum 𝕜 (abs a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a

Tactic:
rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, cfc_map_spectrum ..]

Premises used: CFC.abs_eq_cfcₙ_coe_norm, cfcₙ_eq_cfc, cfc_map_spectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : ContinuousStar A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : CompleteSpace A
⊢ Continuous (Y := A) fun (a : A) ↦ star a * a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : ContinuousStar A
inst_3 : NormedSpace ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : CompleteSpace A
⊢ ∀ (x : A), Membership.mem (γ := Set A) {a : A | 0 ≤ a} (star x * x)

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
rw₂ rw₃ : a = 0 ↔ a = 0
⊢ abs a = 0 ↔ a = 0

Tactic:
rw [CFC.abs, sqrt_eq_zero_iff _, CStarRing.star_mul_self_eq_zero_iff]

Premises used: CStarRing.star_mul_self_eq_zero_iff, CFC.sqrt_eq_zero_iff, CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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‖
rw₆ rw₇ : ‖a‖ * ‖a‖ = ‖a‖ * ‖a‖
⊢ ‖abs 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]

Premises used: LE.le.star_eq, sq, CStarRing.norm_star_mul_self, sq_eq_sq₀, CFC.abs_mul_abs, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
h :
  ∀ (a : α),
    Eq.{u_1 + 1} (α := 𝕜) ((exp f : (a : α) → 𝕜) a : 𝕜)
      (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
⊢ exp f = { toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ }

Tactic:
ext a
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
a : α
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 := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((exp f : (a : α) → 𝕜) a : 𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)

Tactic:
simp_rw [NormedSpace.exp_eq_expSeries_sum (𝔸 := C(α, 𝕜)) 𝕜, FormalMultilinearSeries.sum]

Premises used: FormalMultilinearSeries.sum, NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
𝕜 : Type u_1
α : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
h :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (i : ℕ), (HSMul.hSMul (α := 𝕜) (↑i.factorial : 𝕜)⁻¹ (f ^ i) : (a : α) → 𝕜) a : 𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) 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 : 𝕜)

Tactic:
simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]

Premises used: ContinuousMap.tsum_apply, NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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} (α := 𝕜) (∑' (i : ℕ), (HSMul.hSMul (α := 𝕜) (↑i.factorial : 𝕜)⁻¹ (f ^ i) : (a : α) → 𝕜) a : 𝕜)
    (({ toFun := exp ∘ (⇑f : (a : α) → 𝕜), continuous_toFun := ⋯ : C(α, 𝕜) } : (a : α) → 𝕜) a : 𝕜)

Tactic:
simp [NormedSpace.exp_eq_tsum 𝕜]

Premises used: NormedSpace.exp_eq_tsum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
⊢ cfc (p := IsSelfAdjoint) Real.exp a = exp a

Tactic:
Real.exp_eq_exp_ℝ ▸ exp_eq_normedSpace_exp ha

Premises used: Eq.rec, CFC.exp_eq_normedSpace_exp, Real.exp_eq_exp_ℝ, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
rw : 0 ≤ cfc (p := IsSelfAdjoint) Real.exp a
⊢ 0 ≤ exp a

Tactic:
rw [← real_exp_eq_normedSpace_exp]

Premises used: CFC.real_exp_eq_normedSpace_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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 ≤ cfc (p := IsSelfAdjoint) Real.exp a

Tactic:
cfc_nonneg fun x _ => Real.exp_nonneg x

Premises used: cfc_nonneg, Real.exp_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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 ≤ cfc (p := IsSelfAdjoint) Real.exp a

Tactic:
exact cfc_nonneg fun x _ => Real.exp_nonneg x

Premises used: cfc_nonneg, Real.exp_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
p : A → Prop
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℂ A
inst_3 : ContinuousFunctionalCalculus ℂ A p
a : A
ha : p a
⊢ cfc (p := p) Complex.exp a = exp a

Tactic:
Complex.exp_eq_exp_ℂ ▸ exp_eq_normedSpace_exp ha

Premises used: Complex.exp_eq_exp_ℂ, Eq.rec, CFC.exp_eq_normedSpace_exp, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ IsSelfAdjoint (log a)

Tactic:
cfc_predicate _ a

Premises used: CFC.log, cfc_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ log 0 = 0

Tactic:
simp [log]

Premises used: CFC.log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ log 1 = 0

Tactic:
simp [log]

Premises used: CFC.log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
⊢ log ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) (Real.log r)

Tactic:
simp [log]

Premises used: CFC.log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
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)
⊢ log (r • a) = HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (log a)

Tactic:
rw [log, ← cfc_smul_id (R := ℝ) r a, ← cfc_comp Real.log (r • ·) a, log]

Premises used: Real.log, cfc_comp, CFC.log, cfc_smul_id, HSMul.hSMul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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 (x1 : ℝ) ↦ Real.log (r * x1)) a =
    cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ Real.log r + Real.log z) a

Tactic:
cfc_congr (Real.log_mul hr <| ha₂ · ·)

Premises used: cfc_congr, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
rw 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)
⊢ 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:
rw [cfc_const_add _ _ _]

Premises used: cfc_const_add
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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)
⊢ 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:
calc
    _ = cfc (fun z => Real.log r + Real.log z) a :=
      cfc_congr (Real.log_mul hr <| ha₂ · ·)
    _ = _ := by rw [cfc_const_add _ _ _]

Premises used: cfc, Real.log, HAdd.hAdd, cfc_congr, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
r : ℝ
a : A
hr : 0 < r
ha : IsStrictlyPositive a
⊢ log (r • a) = HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (Real.log r) : A) (log a)

Tactic:
grind [log_smul]

Premises used: CFC.log_smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
funProp : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn Real.log (spectrum ℝ a)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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
⊢ ContinuousOn Real.log (spectrum ℝ a)

Tactic:
have ha₂' : ContinuousOn Real.log (spectrum ℝ a) := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a) x → x ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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)
funProp : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a) x → x ≠ 0
⊢ ContinuousOn Real.log ((fun (x : ℝ) ↦ x ^ n) '' spectrum ℝ a)

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
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)

Tactic:
have ha₂'' : ContinuousOn Real.log ((· ^ n) '' spectrum ℝ a) := by fun_prop (disch := aesop)