awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ p⁻¹ • (a ^ p - 1)
have h : ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p - 1
Tactic: refine ConcaveOn.smul (by positivity) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p - 1
have h_convex : Convex ℝ s
Tactic: have h_convex : Convex ℝ s := by grind [convex_iff_forall_pos]
-- 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
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p - 1
have h : ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p
Tactic: refine ConcaveOn.sub ?_ (convexOn_const _ h_convex)
-- 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
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p
have h : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
Tactic: refine ConcaveOn.subset (t := Ici 0) ?_ (by grind) h_convex
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ a⁺ * a⁻ = 0
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
Tactic: rw [posPart_def, negPart_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
have pos : ∀ (ha : IsSelfAdjoint a),
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
pos :
  ∀ (ha : IsSelfAdjoint a),
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
have neg : ∀ (ha : ¬IsSelfAdjoint a),
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
have pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ * x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a
Tactic: rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ * x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a
have pos : ∀ x ∈ quasispectrum ℝ a, x⁺ * x⁻ = 0 x
Tactic: refine cfcₙ_congr (fun x _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ a⁻ * a⁺ = 0
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
Tactic: rw [posPart_def, negPart_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
have pos : ∀ (ha : IsSelfAdjoint a),
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
pos :
  ∀ (ha : IsSelfAdjoint a),
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
have neg : ∀ (ha : ¬IsSelfAdjoint a),
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
have pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻ * x⁺) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a
Tactic: rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻ * x⁺) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a
have pos : ∀ x ∈ quasispectrum ℝ a, x⁻ * x⁺ = 0 x
Tactic: refine cfcₙ_congr (fun x _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ a⁺ - a⁻ = a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a - cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = a
Tactic: rw [posPart_def, negPart_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a - cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = a
Tactic: rw [← cfcₙ_sub _ _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
| a
have rw : cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: rw [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = a
have conv_rhs : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: conv_rhs => rw [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
have h : ∀ (x : ℝ), x⁺ - x⁻ = id x
Tactic: congr! 2 with
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
⊢ (-a)⁺ = a⁻
have pos : ∀ (ha : IsSelfAdjoint a), (-a)⁺ = a⁻
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
pos : ∀ (ha : IsSelfAdjoint a), (-a)⁺ = a⁻
⊢ (-a)⁺ = a⁻
have neg : ∀ (ha : ¬IsSelfAdjoint a), (-a)⁺ = a⁻
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ (-a)⁺ = a⁻
have pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (-x)⁺) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a
Tactic: rw [posPart_def, negPart_def, ← cfcₙ_comp_neg _ _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
⊢ (-a)⁺ = a⁻
have ha' : ¬IsSelfAdjoint (-a)
Tactic: have ha' : ¬ IsSelfAdjoint (-a) := fun h ↦ ha (by simpa using h.neg)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
⊢ (-a)⁺ = a⁻
have neg : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = a⁻
Tactic: rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
neg : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = a⁻
⊢ (-a)⁺ = a⁻
have neg₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a
Tactic: rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
neg : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = a⁻
neg₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a
⊢ (-a)⁺ = a⁻
have neg₂ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = 0
Tactic: rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
neg : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = a⁻
neg₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a
neg₂ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = 0
⊢ (-a)⁺ = a⁻
have neg₃ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
⊢ (-a)⁻ = a⁺
have rw : a⁺ = (-a)⁻
Tactic: rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
rw : a⁺ = (-a)⁻
⊢ (-a)⁻ = a⁺
have rw₁ : a⁺ - (-a)⁻ = 0
Tactic: rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
rw : a⁺ = (-a)⁻
rw₁ : a⁺ - (-a)⁻ = 0
⊢ (-a)⁻ = a⁺
have rw₂ : a⁺ - (- -a)⁺ = 0
Tactic: rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
rw : a⁺ = (-a)⁻
rw₁ : a⁺ - (-a)⁻ = 0
rw₂ : a⁺ - (- -a)⁺ = 0
⊢ (-a)⁻ = a⁺
have rw₃ : a⁺ - a⁺ = 0
Tactic: rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
a : A
rw : a⁺ = (-a)⁻
rw₁ : a⁺ - (-a)⁻ = 0
rw₂ : a⁺ - (- -a)⁺ = 0
rw₃ : a⁺ - a⁺ = 0
⊢ (-a)⁻ = a⁺
have rw₄ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
⊢ (r • a)⁺ = r • a⁺
have pos : ∀ (ha : IsSelfAdjoint a), (r • a)⁺ = r • a⁺
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
pos : ∀ (ha : IsSelfAdjoint a), (r • a)⁺ = r • a⁺
⊢ (r • a)⁺ = r • a⁺
have neg : ∀ (ha : ¬IsSelfAdjoint a), (r • a)⁺ = r • a⁺
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
⊢ (r • a)⁺ = r • a⁺
have pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((↑r : ℝ) • a) = (↑r : ℝ) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a
Tactic: simp only [CFC.posPart_def, NNReal.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((↑r : ℝ) • a) =
    (↑r : ℝ) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a
have pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ((↑r : ℝ) • x)⁺) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑r : ℝ) • x⁺) a
Tactic: rw [← cfcₙ_comp_smul .., ← cfcₙ_smul ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ((↑r : ℝ) • x)⁺) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑r : ℝ) • x⁺) a
have pos : ∀ (x : ℝ) (hx : x ∈ quasispectrum ℝ a), ((↑r : ℝ) • x)⁺ = (↑r : ℝ) • x⁺
Tactic: refine cfcₙ_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
⊢ (r • a)⁺ = r • a⁺
have neg : (HSMul.hSMul (α := ℝ≥0) 0 a)⁺ = HSMul.hSMul (α := ℝ≥0) 0 a⁺
Tactic: obtain (rfl | hr) := eq_or_ne r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
neg : (HSMul.hSMul (α := ℝ≥0) 0 a)⁺ = HSMul.hSMul (α := ℝ≥0) 0 a⁺
⊢ (r • a)⁺ = r • a⁺
have neg₁ : ∀ (hr : r ≠ 0), (r • a)⁺ = r • a⁺
Tactic: obtain (rfl | hr) := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
hr : r ≠ 0
⊢ (r • a)⁺ = r • a⁺
have this : ¬IsSelfAdjoint (r • a)
Tactic: have := (not_iff_not.mpr <| (IsSelfAdjoint.all r).smul_iff hr.isUnit (x := a)) |>.mpr ha