awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
| HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2
have rw : ‖b * a * star b‖
Tactic: rw [← (CFC.sqrt_nonneg a).star_eq, ← star_star b, ← star_mul, norm_star,
    ← norm_star_mul_mul_self_of_nonneg _ ha, star_star]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
⊢ ‖b * a * star b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2
have conv_rhs : ‖b * a * star b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2
Tactic: conv_rhs => rw [← (CFC.sqrt_nonneg a).star_eq, ← star_star b, ← star_mul, norm_star,
    ← norm_star_mul_mul_self_of_nonneg _ ha, star_star]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
conv_rhs : ‖b * a * star b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2
⊢ ‖b * a * star b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2
have conv_rhs₁ : ‖b * a * star b‖ = ‖b * a * star b‖
Tactic: conv_rhs => rw [← (CFC.sqrt_nonneg a).star_eq, ← star_star b, ← star_mul, norm_star,
    ← norm_star_mul_mul_self_of_nonneg _ ha, star_star]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
⊢ MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)
have obtain : ∀ (μ : Measure ℝ)
  (hμ :
    ∀ (a : A),
      Membership.mem (γ := Set A) (Ici 0) a →
        IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
            μ ∧
          a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ),
  MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)
Tactic: obtain ⟨μ, hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ A hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
⊢ MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)
have h₃' : EqOn (β := A) (fun (a : A) ↦ a ^ p)
  (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
Tactic: have h₃' : (Ici 0).EqOn (fun a : A => a ^ p)
      (fun a : A => ∫ t in Ioi 0, cfcₙ (rpowIntegrand₀₁ p t) a ∂μ) :=
    fun a ha => (hμ a ha).2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)
have refine : MonotoneOn (β := A) (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ)
  (Ici 0)
Tactic: refine MonotoneOn.congr ?_ h₃'.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ)
    (Ici 0)
have refine : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x)) (Ici 0)
Tactic: refine integral_monotoneOn_of_integrand_ae ?_ fun a ha => (hμ a ha).1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x)) (Ici 0)
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t)) (Ici 0)
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have pos : ∀ (ha : 0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
pos : ∀ (ha : 0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have neg : ∀ (ha : ¬0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have hb : 0 ≤ b
Tactic: have hb : 0 ≤ b := ha.trans hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
have h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (Icc 0 1) x ↔ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
Tactic: have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have pos : ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p) ⦃a b : A⦄ (hab : a ≤ b) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})),
  LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
Tactic: rw [hIcc] at hp
Cleared hypotheses: hp, a, b, hab, ha, hb, hIcc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have pos : ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p),
  LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
Tactic: obtain (hp | hp) | hp := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
pos :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p),
    LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have pos₁ : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {0} p), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
Tactic: obtain (hp | hp) | hp := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
pos :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p),
    LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
pos₁ :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) {0} p), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have pos₂ : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {1} p), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
Tactic: obtain (hp | hp) | hp := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
have this : a ^ p = 0
Tactic: have : a ^ p = 0 := cfcₙ_apply_of_not_predicate a ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ sqrt a ≤ sqrt b
have rw : a ^ (1 / 2) ≤ b ^ (1 / 2)
Tactic: rw [CFC.sqrt_eq_nnrpow a, CFC.sqrt_eq_nnrpow b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ a ^ (1 / 2) ≤ b ^ (1 / 2)
have refine : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) (1 / 2)
Tactic: refine (monotone_nnrpow (A := A) ?_) hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ Membership.mem (γ := Set ℝ≥0) (Icc 0 1) (1 / 2)
have left : 0 ≤ 1 / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
left : 0 ≤ 1 / 2
⊢ Membership.mem (γ := Set ℝ≥0) (Icc 0 1) (1 / 2)
have right : 1 / 2 ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have obtain : ∀ (μ : Measure ℝ)
  (hμ :
    ∀ (a : A),
      Membership.mem (γ := Set A) (Ici 0) a →
        IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
            μ ∧
          a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ),
  ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
Tactic: obtain ⟨μ, hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ A hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have h₃' : EqOn (β := A) (fun (a : A) ↦ a ^ p)
  (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
Tactic: have h₃' : (Ici 0).EqOn (fun a : A => a ^ p)
      (fun a : A => ∫ t in Ioi 0, cfcₙ (rpowIntegrand₀₁ p t) a ∂μ) :=
    fun a ha => (hμ a ha).2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have refine : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦
  ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
Tactic: refine ConcaveOn.congr ?_ h₃'.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦
    ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
have refine : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x))
Tactic: refine integral_concaveOn_of_integrand_ae (convex_Ici _) ?_ fun a ha => (hμ a ha).1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x))
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t))
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
have h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (Icc 0 1) x ↔ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
Tactic: have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have hp₁ : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
Tactic: rw [hIcc] at hp
Cleared hypotheses: hp, hIcc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have inl : ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
Tactic: obtain (hp | hp) | hp := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
inl : ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have inl₁ : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {0} p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
Tactic: obtain (hp | hp) | hp := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
inl : ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
inl₁ : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {0} p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have inr : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {1} p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
Tactic: obtain (hp | hp) | hp := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) {0} p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have hp₁ : p = 0
Tactic: simp only [mem_singleton_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have inl : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ 0
Tactic: simp only [hp, nnrpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) {1} p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have hp₁ : p = 1
Tactic: simp only [mem_singleton_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 1
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have inr : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ≥0) a 1
Tactic: simp only [hp]