awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ConcaveOn ℝ (β := A) (fun (a : A) ↦ Ici 0 a) fun (a : A) ↦ sqrt a
have simp_rw : ConcaveOn ℝ (β := A) (fun (a : A) ↦ Ici 0 a) fun (a : A) ↦ a ^ (1 / 2)
Tactic: simp_rw [sqrt_eq_nnrpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 ⋯
⊢ Monotone (β := A) fun (a : A) ↦ a ^ p
have change : Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
Tactic: change Monotone (fun a : A => a ^ (q : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 ⋯
⊢ Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
have inl : ∀ (hq : q = 0), Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
Tactic: obtain hq | hq := eq_zero_or_pos q
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 : ℝ)
⊢ Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
have inr : ∀ (hq : 0 < q), Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
Tactic: obtain hq | hq := eq_zero_or_pos q
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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
⊢ Monotone (β := A) fun (a : A) ↦ a ^ (↑q : ℝ)
have inl : Monotone (β := A) fun (a : A) ↦ a ^ (↑0 : ℝ)
Tactic: rw [hq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)
have pos : ∀ (ha : 0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) 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 : 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)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)
have neg : ∀ (ha : ¬0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) 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 : 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
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)
have hb : 0 ≤ b
Tactic: have hb : 0 ≤ b := ha.trans hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (hypothesis)
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
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) a) ((fun (a : A) ↦ a ^ (↑0 : ℝ)) b)
have this : HPow.hPow (β := ℝ) a 0 = 0
Tactic: have : a ^ (0 : ℝ) = 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 : 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 : ℝ)
have inr : Monotone (β := A) fun (a : A) ↦ a ^ q
Tactic: simp_rw [← CFC.nnrpow_eq_rpow hq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 ⋯
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
have change : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
Tactic: change ConcaveOn ℝ (Ici (0 : A)) (fun a : A => a ^ (q : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 ⋯
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
have inl : ∀ (hq : q = 0), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
Tactic: obtain hq | hq := eq_zero_or_pos q
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 : ℝ)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
have inr : ∀ (hq : 0 < q), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ (↑q : ℝ)
Tactic: obtain hq | hq := eq_zero_or_pos q
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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) ↦ a ^ (↑q : ℝ)
have inl : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ) a 0
Tactic: simp only [hq, NNReal.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order (goal)
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 : ℝ)
have inr : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ q
Tactic: simp_rw [← CFC.nnrpow_eq_rpow hq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ ConvexOn.{0, u_1, u_1} ℝ (E := A) {a : A | IsStrictlyPositive a} inverse
have 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⁻¹ʳ
Tactic: refine ⟨by grind [convex_iff_forall_pos], ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
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⁻¹ʳ
have IsStrictlyPositive : ∀ (xpos : IsStrictlyPositive 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⁻¹ʳ
Tactic: (xpos : IsStrictlyPositive x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
xpos : IsStrictlyPositive 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⁻¹ʳ
have IsStrictlyPositive : ∀ (ypos : IsStrictlyPositive y) ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
Tactic: (ypos : IsStrictlyPositive y)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have zpos : IsStrictlyPositive z
Tactic: have zpos : IsStrictlyPositive z := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have xinvpos : IsStrictlyPositive x⁻¹ʳ
Tactic: have xinvpos : IsStrictlyPositive x⁻¹ʳ := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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)
have pos : ∀ (ha' : 0 < a), IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
Tactic: by_cases ha' : 0 < a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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)
⊢ IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
have neg : ∀ (ha' : ¬0 < a), IsStrictlyPositive (HSMul.hSMul (β := A) a 1 + b • z)
Tactic: by_cases ha' : 0 < a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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⁻¹ʳ
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have hsp : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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
have 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
Tactic: rw [← cfc_smul_id (R := ℝ) (S := ℝ) b z, ← Algebra.algebraMap_eq_smul_one,
        ← cfc_const_add a (fun r => b • r) z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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
have 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
Tactic: simp only [smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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
have refine : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ z), 0 < a + b * r
Tactic: refine cfc_rpow fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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
⊢ 0 < a + b * r
have pos : ∀ (ha' : a = 0), 0 < a + b * r
Tactic: by_cases ha' : a = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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
⊢ 0 < a + b * r
have neg : ∀ (ha' : ¬a = 0), 0 < a + b * r
Tactic: by_cases ha' : a = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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
have hb' : b = 1
Tactic: have hb' : b = 1 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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 < a + b * r
have pos : 0 < r
Tactic: simp only [ha', hb', one_mul, zero_add, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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)
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have h₁ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have rw : HSMul.hSMul (β := A) a 1 + b • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-1)) z =
  cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
Tactic: rw [CFC.rpow_eq_cfc_real zpos.nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ HSMul.hSMul (β := A) a 1 + b • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-1)) z =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have hcont : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
Tactic: have hcont : ContinuousOn (fun r : ℝ => (r ^ (-1 : ℝ))) (spectrum ℝ z) :=
      ContinuousOn.rpow_const (f := id) (by fun_prop) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
hcont : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
⊢ HSMul.hSMul (β := A) a 1 + b • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-1)) z =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b • HPow.hPow (β := ℝ) x (-1)) z =
  cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
Tactic: rw [← cfc_smul b _ z hcont, ← Algebra.algebraMap_eq_smul_one, ← cfc_const_add a _ z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (goal)
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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
hcont : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ a + b • HPow.hPow (β := ℝ) x (-1)) z =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have refine : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ z), a + b • HPow.hPow (β := ℝ) r (-1) = a + b * HPow.hPow (β := ℝ) r (-1)
Tactic: refine cfc_congr fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder (hypothesis)
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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have h₂ : HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
  cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
Tactic: have h₂ : (a • 1 + b • z ^ (-1 : ℝ)) = cfc (fun r => (a + b * r ^ (-1 : ℝ))) z := by
    rw [CFC.rpow_eq_cfc_real zpos.nonneg]
    have hcont : ContinuousOn (fun r : ℝ => (r ^ (-1 : ℝ))) (spectrum ℝ z) :=
      ContinuousOn.rpow_const (f := id) (by fun_prop) (by grind)
    rw [← cfc_smul b _ z hcont, ← Algebra.algebraMap_eq_smul_one, ← cfc_const_add a _ z]
    refine cfc_congr fun r hr => ?_
    simp