awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ (a • x + b • y)⁻¹ʳ =
    (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ
have rw : (a • x + b • y)⁻¹ʳ = (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) + b • y)⁻¹ʳ
Tactic: rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
rw : (a • x + b • y)⁻¹ʳ = (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) + b • y)⁻¹ʳ
⊢ (a • x + b • y)⁻¹ʳ =
    (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ
have rw₁ : (a • x + b • y)⁻¹ʳ = (a • x + b • y)⁻¹ʳ
Tactic: rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ Eq (α := A) (((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
have rw : Eq (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z)⁻¹ʳ : A)
  ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
Tactic: rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
rw :
  Eq (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z)⁻¹ʳ : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
⊢ Eq (α := A) (((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
have rw₁ : Eq (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z)⁻¹ʳ : A)
  ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z)⁻¹ʳ : A)
Tactic: rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ LE.le (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1)) : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1)) : A)
have h : HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) ≤ HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1)
Tactic: gcongr
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) ≤ HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1)
have h : cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z ≤
  cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
Tactic: rw [h₁, h₂]
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z ≤
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have h : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) (spectrum ℝ z)
Tactic: refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
h : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) (spectrum ℝ z)
⊢ cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z ≤
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have h₃ : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
Tactic: refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
h : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) (spectrum ℝ z)
h₃ : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
⊢ cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z ≤
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
have h₄ : ∀ x ∈ spectrum ℝ z, HPow.hPow (β := ℝ) (a + b * x) (-1) ≤ a + b * HPow.hPow (β := ℝ) x (-1)
Tactic: refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) (spectrum ℝ z)
have h : ∀ x ∈ spectrum ℝ z, a + b * x ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
Tactic: apply ContinuousOn.rpow_const (by fun_prop)
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
have this : 0 < r
Tactic: have := zpos.spectrum_pos 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this : 0 < r
⊢ a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
have this₁ : 0 ≤ b * r
Tactic: have : 0 ≤ b * r := by positivity
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this_1 : 0 < r
this : 0 ≤ b * r
⊢ a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
have h : 0 < a → a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
Tactic: cases lt_or_eq_of_le ha
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this_1 : 0 < r
this : 0 ≤ b * r
h : 0 < a → a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
⊢ a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
have h₃ : 0 = a → a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
Tactic: cases lt_or_eq_of_le ha
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
have h : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)
Tactic: refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this :
  HPow.hPow (β := ℤ) (HSMul.hSMul (β := ℝ) a 1 + b • r) (-1) ≤
    a • HPow.hPow (α := ℝ) (β := ℤ) 1 (-1) + b • HPow.hPow (β := ℤ) r (-1)
⊢ HPow.hPow (β := ℝ) (a + b * r) (-1) ≤ a + b * HPow.hPow (β := ℝ) r (-1)
have this₁ : HPow.hPow (β := ℝ) (HSMul.hSMul (β := ℝ) a 1 + b • r) (↑(-1) : ℝ) ≤
  a • HPow.hPow (α := ℝ) (β := ℝ) 1 (↑(-1) : ℝ) + b • HPow.hPow (β := ℝ) r (↑(-1) : ℝ)
Tactic: simp_rw [← Real.rpow_intCast] at this
Cleared hypotheses: this
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ HPow.hPow (β := ℝ) (a + b * r) (-1) ≤ a + b * HPow.hPow (β := ℝ) r (-1)
have h : HPow.hPow (β := ℤ) (HSMul.hSMul (β := ℝ) a 1 + b • r) (-1) ≤
  a • HPow.hPow (α := ℝ) (β := ℤ) 1 (-1) + b • HPow.hPow (β := ℤ) r (-1)
Tactic: suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ HPow.hPow (β := ℤ) (HSMul.hSMul (β := ℝ) a 1 + b • r) (-1) ≤
    a • HPow.hPow (α := ℝ) (β := ℤ) 1 (-1) + b • HPow.hPow (β := ℤ) r (-1)
have this : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (z : ℝ) ↦ HPow.hPow (β := ℤ) z (-1)
Tactic: have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ Eq (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1)) : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z⁻¹ʳ) : A)
have rw : Eq (α := A) ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z⁻¹ʳ) : A)
  ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z⁻¹ʳ) : A)
Tactic: rw [← inverse_eq_rpow_neg_one]
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
⊢ a • x⁻¹ʳ + HSMul.hSMul (β := A) b ((conjSqrt x⁻¹ʳ : (a : A) → A) z⁻¹ʳ : A) = a • x⁻¹ʳ + b • y⁻¹ʳ
have rw : a • x⁻¹ʳ + HSMul.hSMul (β := A) b (((conjSqrt x : (a : A) → A) z)⁻¹ʳ : A) = a • x⁻¹ʳ + b • y⁻¹ʳ
Tactic: rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]
-- 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
h₂ :
  HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z
rw : a • x⁻¹ʳ + HSMul.hSMul (β := A) b (((conjSqrt x : (a : A) → A) z)⁻¹ʳ : A) = a • x⁻¹ʳ + b • y⁻¹ʳ
⊢ a • x⁻¹ʳ + HSMul.hSMul (β := A) b ((conjSqrt x⁻¹ʳ : (a : A) → A) z⁻¹ʳ : A) = a • x⁻¹ʳ + b • y⁻¹ʳ
have rw₁ : a • x⁻¹ʳ + b • y⁻¹ʳ = a • x⁻¹ʳ + b • y⁻¹ʳ
Tactic: rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]