-- 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
calc :
  (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))⁻¹ʳ
calc₁ :
  (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))⁻¹ʳ
calc₂ :
  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)
calc₃ :
  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)
calc₄ :
  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)
calc₅ :
  (conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z⁻¹ʳ) =
    a • x⁻¹ʳ + HSMul.hSMul (β := A) b ((conjSqrt x⁻¹ʳ : (a : A) → A) z⁻¹ʳ : A)
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
have calc₆ : a • x⁻¹ʳ + HSMul.hSMul (β := A) b ((conjSqrt x⁻¹ʳ : (a : A) → A) z⁻¹ʳ : A) = a • x⁻¹ʳ + b • y⁻¹ʳ
Tactic: calc _ = (a • conjSqrt x 1 + b • conjSqrt x z)⁻¹ʳ := by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]
      _ = (conjSqrt x (a • 1 + b • z))⁻¹ʳ := by simp
      _ = conjSqrt x⁻¹ʳ ((a • 1 + b • z) ^ (-1 : ℝ)) := by
        rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
      _ ≤ conjSqrt x⁻¹ʳ (a • 1 + b • z ^ (-1 : ℝ)) := by
        gcongr
        rw [h₁, h₂]
        refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
        · apply ContinuousOn.rpow_const (by fun_prop)
          intro r hr
          have := zpos.spectrum_pos hr
          have : 0 ≤ b * r := by positivity
          cases lt_or_eq_of_le ha <;> grind
        · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by grind)
        · intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]
      _ = conjSqrt x⁻¹ʳ (a • 1 + b • z⁻¹ʳ) := by rw [← inverse_eq_rpow_neg_one]
      _ = a • inverse x + b • conjSqrt x⁻¹ʳ z⁻¹ʳ := by
        simp [conjSqrt_one x⁻¹ʳ (by grind)]
      _ = _ := by
        rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]