awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
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
⊢ HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) z

Tactic:
rw [CFC.rpow_eq_cfc_real zpos.nonneg]

Premises used: IsStrictlyPositive.nonneg, CFC.rpow_eq_cfc_real
-- 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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ ContinuousOn id (spectrum ℝ z)

Tactic:
fun_prop
-- 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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, id x ≠ 0 ∨ LE.le (α := ℝ) 0 (-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)
h₁ :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) =
    cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z
⊢ 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)
-- 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)
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)
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
⊢ 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_smul b _ z hcont, ← Algebra.algebraMap_eq_smul_one, ← cfc_const_add a _ z]

Premises used: Algebra.algebraMap_eq_smul_one, cfc_smul, cfc_const_add
-- 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)
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

Tactic:
cfc_congr fun r hr => ?_

Premises used: cfc_congr
-- 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)
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)
refine : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ z), a + b • HPow.hPow (β := ℝ) r (-1) = a + b * HPow.hPow (β := ℝ) r (-1)
⊢ 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:
refine cfc_congr fun r hr => ?_

Premises used: cfc_congr
-- 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)
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)
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ a + b • HPow.hPow (β := ℝ) r (-1) = a + b * HPow.hPow (β := ℝ) r (-1)

Tactic:
simp
-- 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)
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

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
-- 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)
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)⁻¹ʳ
rw₁ rw₂ : (a • x + b • y)⁻¹ʳ = (a • x + 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))⁻¹ʳ

Tactic:
rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]

Premises used: CFC.conjSqrt_conjSqrt_ringInverse, CFC.conjSqrt_one, IsStrictlyPositive.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)
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
⊢ (HSMul.hSMul (β := A) a ((conjSqrt x : (a : A) → A) 1 : A) +
        HSMul.hSMul (β := A) b ((conjSqrt x : (a : A) → A) z : A))⁻¹ʳ =
    ((conjSqrt x : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z))⁻¹ʳ

Tactic:
simp
-- 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)
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)
rw₁ 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)
⊢ 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]

Premises used: CFC.ringInverse_conjSqrt, CFC.inverse_eq_rpow_neg_one
-- 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)
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 :
  HPow.hPow (β := ℝ) (HSMul.hSMul (β := A) a 1 + b • z) (-1) ≤ HSMul.hSMul (β := A) a 1 + b • HPow.hPow (β := ℝ) z (-1)
⊢ 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)

Tactic:
gcongr
-- 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)
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 :
  cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) z ≤
    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)

Tactic:
rw [h₁, h₂]
-- 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)
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

Tactic:
(cfc_le_iff _ _ _ ?_ ?_).mpr ?_

Premises used: Iff.mpr, cfc_le_iff
-- 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)
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)
h₄ : ∀ x ∈ spectrum ℝ z, HPow.hPow (β := ℝ) (a + b * x) (-1) ≤ a + b * HPow.hPow (β := ℝ) x (-1)
⊢ 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:
refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_

Premises used: Iff.mpr, cfc_le_iff
-- 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)
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 (x : ℝ) ↦ a + b * x) (spectrum ℝ z)

Tactic:
fun_prop
-- 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)
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 : ∀ x ∈ spectrum ℝ z, a + b * x ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
⊢ ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ HPow.hPow (β := ℝ) (a + b * r) (-1)) (spectrum ℝ z)

Tactic:
apply ContinuousOn.rpow_const (by fun_prop)

Premises used: ContinuousOn.rpow_const
-- 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)
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
⊢ 0 < r

Tactic:
have := zpos.spectrum_pos hr
-- 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)
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
⊢ 0 ≤ b * r

Tactic:
positivity
-- 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)
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
⊢ 0 ≤ b * r

Tactic:
have : 0 ≤ b * r := by positivity
-- 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)
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)
h₃ : 0 = a → a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)
⊢ a + b * r ≠ 0 ∨ LE.le (α := ℝ) 0 (-1)

Tactic:
cases lt_or_eq_of_le ha

Premises used: lt_or_eq_of_le
-- 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)
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)

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)
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)

Tactic:
grind