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

Tactic:
ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _

Premises used: ContinuousOn.const_add, ContinuousOn.const_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)
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 (β := ℝ) r (-1)) (spectrum ℝ z)
⊢ ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ a + b * HPow.hPow (β := ℝ) r (-1)) (spectrum ℝ z)

Tactic:
refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _

Premises used: ContinuousOn.const_add, ContinuousOn.const_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)
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 : ℝ) ↦ r) (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
⊢ ∀ x ∈ spectrum ℝ z, 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
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 (β := ℝ) r (-1)) (spectrum ℝ z)

Tactic:
exact ContinuousOn.rpow_const (by fun_prop) (by grind)

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
this :
  HPow.hPow (β := ℤ) (HSMul.hSMul (β := ℝ) a 1 + b • r) (-1) ≤
    a • HPow.hPow (α := ℝ) (β := ℤ) 1 (-1) + b • HPow.hPow (β := ℤ) r (-1)
⊢ 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

Premises used: Real.rpow_intCast
-- 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 :
  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)

Tactic:
simpa using this
-- 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
h :
  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)

Tactic:
suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
-- 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
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (z : ℝ) ↦ HPow.hPow (β := ℤ) z (-1)

Tactic:
have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
-- 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 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (z : ℝ) ↦ HPow.hPow (β := ℤ) z (-1)
⊢ HPow.hPow (β := ℤ) (HSMul.hSMul (β := ℝ) a 1 + b • r) (-1) ≤
    a • HPow.hPow (α := ℝ) (β := ℤ) 1 (-1) + b • HPow.hPow (β := ℤ) r (-1)

Tactic:
grind [ConvexOn, IsStrictlyPositive.spectrum_pos]

Premises used: IsStrictlyPositive.spectrum_pos, ConvexOn
-- 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 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 • HPow.hPow (β := ℝ) z (-1)) : A)
    ((conjSqrt x⁻¹ʳ : (a : A) → A) (HSMul.hSMul (β := A) a 1 + b • z⁻¹ʳ) : A)

Tactic:
rw [← inverse_eq_rpow_neg_one]

Premises used: 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
⊢ 0 ≤ 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
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
⊢ (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)

Tactic:
simp [conjSqrt_one x⁻¹ʳ (by grind)]

Premises used: Ring.inverse, CFC.conjSqrt_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
rw : a • x⁻¹ʳ + HSMul.hSMul (β := A) b (((conjSqrt x : (a : A) → A) z)⁻¹ʳ : A) = a • x⁻¹ʳ + b • y⁻¹ʳ
rw₁ rw₂ : a • x⁻¹ʳ + b • y⁻¹ʳ = a • x⁻¹ʳ + b • y⁻¹ʳ
⊢ 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]

Premises used: CFC.conjSqrt_conjSqrt_ringInverse, CFC.ringInverse_conjSqrt
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
⊢ ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) 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
t : ℝ
ht : 0 < t
⊢ ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)

Tactic:
have : ∀ x ∈ Ici (0 : A), IsStrictlyPositive (algebraMap ℝ A t + 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
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
a₁ : A
_ : ∀ ⦃a₂ : A⦄, Eq (α := A) ((addl : (a : A) → A) a₁ : A) ((addl : (a : A) → A) a₂ : A) → a₁ = a₂
⊢ ∀ ⦃a₂ : A⦄, Eq (α := A) ((addl : (a : A) → A) a₁ : A) ((addl : (a : A) → A) a₂ : A) → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
a₁ a₂ : A
⊢ Eq (α := A) ((addl : (a : A) → A) a₁ : A) ((addl : (a : A) → A) a₂ : A) → a₁ = a₂

Tactic:
simp [addl]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
⊢ Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)

Tactic:
have haddl : Function.Injective addl := by intro _ _; simp [addl]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
rw rw₁ : Eq.{u_1 + 1} (α := Set A) (Ici 0) (Ici 0)
⊢ Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))

Tactic:
rw [Set.preimage_image_eq _ haddl]

Premises used: Set.preimage_image_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
⊢ Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))

Tactic:
have hici : Ici (0 : A) = addl ⁻¹' addl '' Ici 0 := by
    rw [Set.preimage_image_eq _ haddl]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
simp_rw :
  ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (β := A) x ((algebraMap ℝ A : (a : ℝ) → A) t : A))
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)

Tactic:
simp_rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
change : ConvexOn ℝ (E := A) (β := A) (Ici 0) (Ring.inverse ∘ (⇑addl : (a : A) → A))
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦ Ring.inverse (HAdd.hAdd (β := A) x ((algebraMap ℝ A : (a : ℝ) → A) t : A))

Tactic:
change ConvexOn ℝ (Ici 0) (Ring.inverse ∘ addl)

Premises used: Real, Set.Ici, Function.comp, Ring.inverse, OfNat.ofNat, DFunLike.coe, ConvexOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
rw :
  ConvexOn ℝ (E := A) (β := A) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
    (Ring.inverse ∘ (⇑addl : (a : A) → A))
⊢ ConvexOn ℝ (E := A) (β := A) (Ici 0) (Ring.inverse ∘ (⇑addl : (a : A) → A))

Tactic:
rw [hici]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
hf : ConvexOn ℝ (E := A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) Ring.inverse
⊢ ConvexOn ℝ (E := A) (β := A) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
    (Ring.inverse ∘ (⇑addl : (a : A) → A))

Tactic:
apply ConvexOn.comp_affineMap

Premises used: ConvexOn.comp_affineMap
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
t : ℝ
ht : 0 < t
this :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Ici 0) x →
      IsStrictlyPositive (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
addl : A →ᵃ[ℝ] A :=
  (LinearEquiv.symm (AffineMap.toConstProdLinearMap ℝ) : (a : A × (A →ₗ[ℝ] A)) → A →ᵃ[ℝ] A)
    ((algebraMap ℝ A : (a : ℝ) → A) t, LinearMap.id)
haddl : Function.Injective (α := A) (β := A) (⇑addl : (a : A) → A)
hici : Eq (α := Set A) (Ici 0) (preimage (β := A) (⇑addl : (a : A) → A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)))
⊢ ConvexOn ℝ (E := A) (image (α := A) (⇑addl : (a : A) → A) (Ici 0)) Ring.inverse

Tactic:
ConvexOn.subset CStarAlgebra.convexOn_ringInverse ?_ (Convex.affine_image _ (convex_Ici _))

Premises used: Convex.affine_image, CStarAlgebra.convexOn_ringInverse, convex_Ici, ConvexOn.subset