awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
change : Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
⊢ Monotone (β := A) fun (a : A) ↦ a ^ p

Tactic:
change Monotone (fun a : A => a ^ (q : ℝ))

Premises used: Monotone, HPow.hPow, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
inl : ∀ (hq : q = 0), Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
inr : ∀ (hq : 0 < q), Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
⊢ Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)

Tactic:
obtain hq | hq := eq_zero_or_pos q

Premises used: eq_zero_or_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
inl : Monotone (β := A) fun (a : A) ↦ a ^ (↑0 : ℝ)
⊢ Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)

Tactic:
rw [hq]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
a b : A
hab : a ≤ b
pos : ∀ (ha : 0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)
neg : ∀ (ha : ¬0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)

Tactic:
by_cases ha : 0 ≤ a
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
a b : A
hab : a ≤ b
ha : 0 ≤ a
⊢ 0 ≤ b

Tactic:
have hb : 0 ≤ b := ha.trans hab
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)

Tactic:
simp [CFC.rpow_zero a, CFC.rpow_zero b]

Premises used: CFC.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
⊢ HPow.hPow (β := ℝ) a 0 = 0

Tactic:
have : a ^ (0 : ℝ) = 0 := cfc_apply_of_not_predicate a ha
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
this : HPow.hPow (β := ℝ) a 0 = 0
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : 0 < q
inr : Monotone (β := A) fun (a : A) ↦ a ^ q
⊢ Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)

Tactic:
simp_rw [← CFC.nnrpow_eq_rpow hq]

Premises used: CFC.nnrpow_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : 0 < q
⊢ Monotone (β := A) fun (a : A) ↦ a ^ q

Tactic:
monotone_nnrpow hp

Premises used: CFC.monotone_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : 0 < q
⊢ Monotone (β := A) fun (a : A) ↦ a ^ q

Tactic:
exact monotone_nnrpow hp

Premises used: CFC.monotone_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
a b : A
hab : a ≤ b
⊢ a ^ p ≤ b ^ p

Tactic:
monotone_rpow hp hab

Premises used: CFC.monotone_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
change : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
change ConcaveOn ℝ (Ici (0 : A)) (fun a : A => a ^ (q : ℝ))

Premises used: Real, Set.Ici, HPow.hPow, ConcaveOn, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
inl : ∀ (hq : q = 0), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
inr : ∀ (hq : 0 < q), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)

Tactic:
obtain hq | hq := eq_zero_or_pos q

Premises used: eq_zero_or_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
inl : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ) a 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)

Tactic:
simp only [hq, NNReal.coe_zero]

Premises used: NNReal.coe_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ) a 0

Tactic:
ConcaveOn.congr (concaveOn_const _ (convex_Ici _)) rpow_zero_eqOn.symm

Premises used: ConcaveOn.congr, convex_Ici, Set.EqOn.symm, CFC.rpow_zero_eqOn, concaveOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : q = 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ) a 0

Tactic:
exact ConcaveOn.congr (concaveOn_const _ (convex_Ici _)) rpow_zero_eqOn.symm

Premises used: ConcaveOn.congr, convex_Ici, Set.EqOn.symm, CFC.rpow_zero_eqOn, concaveOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : 0 < q
inr : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ q
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)

Tactic:
simp_rw [← CFC.nnrpow_eq_rpow hq]

Premises used: CFC.nnrpow_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : 0 < q
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ q

Tactic:
concaveOn_nnrpow hp

Premises used: CFC.concaveOn_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Icc 0 1) p
q : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) p ⋯
hq : 0 < q
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ q

Tactic:
exact concaveOn_nnrpow hp

Premises used: CFC.concaveOn_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Convex.{0, u_1} ℝ (E := A) {a : A | IsStrictlyPositive a}

Tactic:
grind [convex_iff_forall_pos]

Premises used: convex_iff_forall_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
refine :
  ∀ ⦃x : A⦄,
    Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} x →
      ∀ ⦃y : A⦄,
        Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} y →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
⊢ ConvexOn.{0, u_1, u_1} ℝ (E := A) {a : A | IsStrictlyPositive a} inverse

Tactic:
refine ⟨by grind [convex_iff_forall_pos], ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
IsStrictlyPositive :
  ∀ (xpos : _root_.IsStrictlyPositive x) ⦃y : A⦄,
    Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} y →
      ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
⊢ Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} x →
    ∀ ⦃y : A⦄,
      Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} y →
        ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
(xpos : IsStrictlyPositive x)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : _root_.IsStrictlyPositive x
y : A
IsStrictlyPositive :
  ∀ (ypos : _root_.IsStrictlyPositive y) ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
⊢ Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} y →
    ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
(ypos : IsStrictlyPositive y)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
⊢ IsStrictlyPositive z

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
⊢ IsStrictlyPositive z

Tactic:
have zpos : IsStrictlyPositive z := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
⊢ IsStrictlyPositive x⁻¹ʳ

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
⊢ IsStrictlyPositive x⁻¹ʳ

Tactic:
have xinvpos : IsStrictlyPositive x⁻¹ʳ := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
pos : ∀ (ha' : 0 < a), IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
neg : ∀ (ha' : ¬0 < a), IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)

Tactic:
by_cases ha' : 0 < a
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
ha' : 0 < a
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)

Tactic:
grind [smul_nonneg]

Premises used: smul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
ha' : ¬0 < a
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)

Tactic:
grind [smul_nonneg]

Premises used: smul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)

Tactic:
have hsp : IsStrictlyPositive (a • 1 + b • z) := by
    by_cases ha' : 0 < a <;> grind [smul_nonneg]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
rw :
  HPow.hPow (β := ℝ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b • x) z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z

Tactic:
rw [← cfc_smul_id (R := ℝ) (S := ℝ) b z, ← Algebra.algebraMap_eq_smul_one,
        ← cfc_const_add a (fun r => b • r) z]

Premises used: Algebra.algebraMap_eq_smul_one, cfc_const_add, cfc_smul_id, HSMul.hSMul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
simp :
  HPow.hPow (β := ℝ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b * x) z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ HPow.hPow (β := ℝ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b • x) z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z

Tactic:
simp only [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
⊢ HPow.hPow (β := ℝ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b * x) z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z

Tactic:
cfc_rpow fun r hr => ?_

Premises used: CFC.cfc_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
refine : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ z), 0 < a + b * r
⊢ HPow.hPow (β := ℝ) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b * x) z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z

Tactic:
refine cfc_rpow fun r hr => ?_

Premises used: CFC.cfc_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
pos : ∀ (ha' : a = 0), 0 < a + b * r
neg : ∀ (ha' : ¬a = 0), 0 < a + b * r
⊢ 0 < a + b * r

Tactic:
by_cases ha' : a = 0
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
⊢ b = 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
⊢ b = 1

Tactic:
have hb' : b = 1 := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
hb' : b = 1
pos : 0 < r
⊢ 0 < a + b * r

Tactic:
simp only [ha', hb', one_mul, zero_add, gt_iff_lt]

Premises used: zero_add, gt_iff_lt, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
hb' : b = 1
⊢ 0 < r

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : ¬a = 0
⊢ 0 < a + b * r

Tactic:
grind [add_pos_of_pos_of_nonneg, mul_nonneg]

Premises used: mul_nonneg, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ : (a : A) → A) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
⊢ HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z

Tactic:
have h₁ : (a • 1 + b • z) ^ (-1 : ℝ) = cfc (fun r => (a + b * r) ^ (-1 : ℝ)) z := by
    rw [← cfc_smul_id (R := ℝ) (S := ℝ) b z, ← Algebra.algebraMap_eq_smul_one,
        ← cfc_const_add a (fun r => b • r) z]
    simp only [smul_eq_mul]
    refine cfc_rpow fun r hr => ?_
    by_cases ha' : a = 0
    · have hb' : b = 1 := by grind
      simp only [ha', hb', one_mul, zero_add, gt_iff_lt]
      grind
    · grind [add_pos_of_pos_of_nonneg, mul_nonneg]