awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ 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
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r : R
a : A
⊢ abs (r • a) = r • abs a
have suffices : ∀ (r : ℝ≥0), abs (r • a) = r • abs a
Tactic: suffices ∀ r : ℝ≥0, abs (r • a) = r • abs a by simpa using this (r • 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ 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
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r_1 : R
a : A
r : ℝ≥0
⊢ abs (r • a) = r • abs a
have rw : r • abs a * r • abs a = star (r • a) * r • a
Tactic: rw [abs, sqrt_eq_iff _ _ (star_mul_self_nonneg _) (smul_nonneg (by positivity) (abs_nonneg _))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = ‖r‖ • abs a
have trans : abs (r • a) = abs (‖r‖ • a)
Tactic: trans abs (‖r‖ • a)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
trans : abs (r • a) = abs (‖r‖ • a)
⊢ abs (r • a) = ‖r‖ • abs a
have trans₁ : abs (‖r‖ • a) = ‖r‖ • abs a
Tactic: trans abs (‖r‖ • a)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = abs (‖r‖ • a)
have simp : sqrt ((r • star r) • (star a * a)) = sqrt (HSMul.hSMul (α := 𝕜) (β := 𝕜) (↑‖r‖ : 𝕜) (star (↑‖r‖ : 𝕜)) • (star a * a))
Tactic: simp only [abs, mul_smul_comm, smul_mul_assoc, star_smul, ← smul_assoc,
      RCLike.real_smul_eq_coe_smul (K := 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (‖r‖ • a) = ‖r‖ • abs a
have lift : ∀ (r : ℝ≥0), abs ((↑r : ℝ) • a) = (↑r : ℝ) • abs a
Tactic: lift ‖r‖ to ℝ≥0 using norm_nonneg _ with r
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
⊢ abs a = cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a
have rw : cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = star a * a
Tactic: rw [abs, sqrt_eq_iff _ _ (hb := cfcₙ_norm_nonneg _ _), ← cfcₙ_mul ..]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
| star a * a
have rw : cfcₙ (p := p) (fun (x : 𝕜) ↦ star x * x) a
Tactic: rw [← cfcₙ_id' 𝕜 a, ← cfcₙ_star, ← cfcₙ_mul ..]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = star a * a
have conv_rhs : cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) (fun (x : 𝕜) ↦ star x * x) a
Tactic: conv_rhs => rw [← cfcₙ_id' 𝕜 a, ← cfcₙ_star, ← cfcₙ_mul ..]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
have inl : ∀ (hf0 : f 0 = 0), cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
Tactic: obtain (hf0 | hf0) := em (f 0 = 0)
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
inl : ∀ (hf0 : f 0 = 0), cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
have inr : ∀ (hf0 : ¬f 0 = 0), cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
Tactic: obtain (hf0 | hf0) := em (f 0 = 0)
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
have inl : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : 𝕜) ↦ (↑‖x‖ : 𝕜)) a) = cfcₙ (p := p) f (abs a)
Tactic: rw [cfcₙ_comp' f (‖·‖) a, ← abs_eq_cfcₙ_coe_norm _ a]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
inl : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : 𝕜) ↦ (↑‖x‖ : 𝕜)) a) = cfcₙ (p := p) f (abs a)
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
have inl₁ : cfcₙ (p := p) f (abs a) = cfcₙ (p := p) f (abs a)
Tactic: rw [cfcₙ_comp' f (‖·‖) a, ← abs_eq_cfcₙ_coe_norm _ a]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
have inr : cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = 0
Tactic: rw [cfcₙ_apply_of_not_map_zero _ hf0,
      cfcₙ_apply_of_not_map_zero _ (fun h ↦ (hf0 <| by simpa using h).elim)]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
inr : cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = 0
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
have inr₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_apply_of_not_map_zero _ hf0,
      cfcₙ_apply_of_not_map_zero _ (fun h ↦ (hf0 <| by simpa using h).elim)]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
⊢ quasispectrum 𝕜 (abs a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a
have rw : quasispectrum 𝕜 (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a ha, cfcₙ_map_quasispectrum ..]
-- 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
rw : quasispectrum 𝕜 (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a
⊢ quasispectrum 𝕜 (abs a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a
have rw₁ : Eq (α := Set 𝕜) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a ha, cfcₙ_map_quasispectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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
a : A
ha : IsSelfAdjoint a
⊢ abs a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
Tactic: rw [abs_eq_cfcₙ_norm _, cfcₙ_eq_cfc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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
a : A
ha : IsSelfAdjoint a
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
⊢ abs a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
have rw₁ : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
Tactic: rw [abs_eq_cfcₙ_norm _, cfcₙ_eq_cfc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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 (↑(Int.negSucc n) : A)) (↑|Int.negSucc n| : A)
have negSucc : Eq.{u_2 + 1} (α := A) (↑(↑(n + 1) : ℤ) : A) (↑|Int.negSucc n| : A)
Tactic: rw [Int.cast_negSucc, abs_neg, abs_natCast, ← Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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)
have ofNat : ∀ (a : ℕ), Eq.{u_2 + 1} (α := A) (abs (↑(Int.ofNat a) : A)) (↑|Int.ofNat a| : A)
Tactic: cases n with
  | ofNat _ => simp
  | negSucc n =>
    rw [Int.cast_negSucc, abs_neg, abs_natCast, ← Int.cast_natCast]
    congr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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)
⊢ Eq.{u_2 + 1} (α := A) (abs (↑n : A)) (↑|n| : A)
have negSucc : ∀ (n : ℕ), Eq.{u_2 + 1} (α := A) (abs (↑(Int.negSucc n) : A)) (↑|Int.negSucc n| : A)
Tactic: cases n with
  | ofNat _ => simp
  | negSucc n =>
    rw [Int.cast_negSucc, abs_neg, abs_natCast, ← Int.cast_natCast]
    congr
Cleared hypotheses: n
-- 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
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' spectrum 𝕜 a)
⊢ cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (abs a)
have rw : cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a)
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, ← cfc_comp' ..]
-- 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
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)
⊢ cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (abs a)
have rw₁ : cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (cfc (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a)
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, ← cfc_comp' ..]
-- 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
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)
⊢ cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) f (abs a)
have rw₂ : cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfc (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a
Tactic: rw [abs_eq_cfcₙ_coe_norm 𝕜 a, cfcₙ_eq_cfc, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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
⊢ HPow.hPow (β := ℕ) (abs a) 2 = star a * a
have rw : abs a * abs a = star a * a
Tactic: rw [sq, abs_mul_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
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
⊢ HPow.hPow (β := ℕ) (abs a) 2 = star a * a
have rw₁ : star a * a = star a * a
Tactic: rw [sq, abs_mul_abs]
-- 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
⊢ 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 ..]