awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
⊢ ¬0 ≤ a ∨ ¬IsUnit a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
neg : ∀ (H : ¬0 ≤ a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
neg₁ : ∀ (H : ¬IsUnit a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
obtain (H | H) : ¬0 ≤ a ∨ ¬IsUnit a := by grind

Premises used: IsUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
neg : sqrt a⁻¹ʳ = 0
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
rw [sqrt_of_not_nonneg H, inverse_zero]

Premises used: CFC.sqrt_of_not_nonneg, Ring.inverse_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
pos : ∀ (hunit : IsUnit a), sqrt a⁻¹ʳ = 0
neg : ∀ (hunit : ¬IsUnit a), sqrt a⁻¹ʳ = 0
⊢ sqrt a⁻¹ʳ = 0

Tactic:
by_cases hunit : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
⊢ ¬0 ≤ a⁻¹ʳ

Tactic:
grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]

Premises used: CFC.ringInverse_nonneg_iff_nonneg_of_isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
⊢ ¬0 ≤ a⁻¹ʳ

Tactic:
have h₂ : ¬0 ≤ inverse a := by grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
h₂ : ¬0 ≤ a⁻¹ʳ
pos pos₁ : Eq.{u_1 + 1} (α := A) 0 0
⊢ sqrt a⁻¹ʳ = 0

Tactic:
rw [sqrt_of_not_nonneg h₂]

Premises used: CFC.sqrt_of_not_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : ¬IsUnit a
⊢ sqrt a⁻¹ʳ = 0

Tactic:
simp [inverse_non_unit _ hunit]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬IsUnit a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
simp [inverse_non_unit _ ha', inverse_non_unit _ H]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 1

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ IsUnit (sqrt a) ∧ a = sqrt a * sqrt a

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 2

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ ∃ (b : A), IsStrictlyPositive b ∧ a = b * b

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 3

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ ∃ (b : A), IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 4

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ ∃ (b : A), IsUnit b ∧ a = star b * b

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 5

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ ∃ (b : A), IsUnit b ∧ a = b * star b

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 6

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
⊢ IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
CStarAlgebra.isStrictlyPositive_TFAE.out 0 8

Premises used: List.TFAE.out, CStarAlgebra.isStrictlyPositive_TFAE, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c : A
⊢ Eq (α := A →ₗ[ℝ] A) (↑(conjSqrt c) : A →ₗ[ℝ] A) (LinearMap.mulLeftRight ℝ (sqrt c, sqrt c))

Tactic:
rfl

Premises used: LinearMap.mulLeftRight, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a : A
⊢ (conjSqrt c : (a : A) → A) a = sqrt c * a * sqrt c

Tactic:
rfl

Premises used: CFC.sqrt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a : A
hc : ¬0 ≤ c
⊢ Eq (α := A) ((conjSqrt c : (a : A) → A) a : A) (0 : A)

Tactic:
simp [conjSqrt_apply, sqrt_of_not_nonneg hc]

Premises used: CFC.sqrt_of_not_nonneg, CFC.conjSqrt_apply
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
pos : ∀ (hc : 0 ≤ c), LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
neg : ∀ (hc : ¬0 ≤ c), LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
⊢ LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)

Tactic:
by_cases hc : 0 ≤ c
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
hc : 0 ≤ c
⊢ IsSelfAdjoint (sqrt c, sqrt c).1

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
hc : 0 ≤ c
⊢ LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)

Tactic:
exact IsSelfAdjoint.conjugate_le_conjugate hab (by cfc_tac)

Premises used: IsSelfAdjoint.conjugate_le_conjugate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
hc : ¬0 ≤ c
⊢ LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)

Tactic:
simp [conjSqrt_of_not_nonneg hc]

Premises used: CFC.conjSqrt_of_not_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
h : a ≤ b
⊢ LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)

Tactic:
conjSqrt_monotone h

Premises used: CFC.conjSqrt_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ IsSelfAdjoint (sqrt c)

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ IsSelfAdjoint (sqrt c)

Tactic:
have hc' : IsSelfAdjoint (sqrt c) := by cfc_tac
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
rw : IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
⊢ IsStrictlyPositive (A := A) ((conjSqrt c : (a : A) → A) a : A) ↔ IsStrictlyPositive a

Tactic:
rw [conjSqrt_apply]

Premises used: CFC.conjSqrt_apply
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
pos : ∀ (ha : IsSelfAdjoint a), IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
neg : ∀ (ha : ¬IsSelfAdjoint a), IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
ha : IsSelfAdjoint a
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
ha : ¬IsSelfAdjoint a
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
pos : ∀ (ha : IsUnit a), Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
neg : ∀ (ha : ¬IsUnit a), Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
⊢ Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : IsUnit a
⊢ Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)

Tactic:
grind [conjSqrt_apply]

Premises used: CFC.conjSqrt_apply
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : ¬IsUnit a
⊢ ¬IsUnit (M := A) ((conjSqrt c : (a : A) → A) a : A)

Tactic:
grind [conjSqrt_apply, IsUnit.mul_left_iff]

Premises used: CFC.conjSqrt_apply, IsUnit.mul_left_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : ¬IsUnit a
⊢ ¬IsUnit (M := A) ((conjSqrt c : (a : A) → A) a : A)

Tactic:
have : ¬IsUnit (conjSqrt c a) := by grind [conjSqrt_apply, IsUnit.mul_left_iff]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : ¬IsUnit a
this : ¬IsUnit (M := A) ((conjSqrt c : (a : A) → A) a : A)
⊢ Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)

Tactic:
simp [inverse_non_unit a ha, inverse_non_unit _ this]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ (conjSqrt c : (a : A) → A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a : A) = a

Tactic:
grind [conjSqrt_ringInverse_conjSqrt _ _ hc.ringInverse]

Premises used: IsStrictlyPositive.ringInverse, CFC.conjSqrt_ringInverse_conjSqrt
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c : A
hc : 0 ≤ c
rw : sqrt c * 1 * sqrt c = c
rw₁ : sqrt c * sqrt c = c
rw₂ rw₃ : c = c
⊢ (conjSqrt c : (a : A) → A) 1 = c

Tactic:
rw [conjSqrt_apply, mul_one, sqrt_mul_sqrt_self _]

Premises used: CFC.conjSqrt_apply, mul_one, CFC.sqrt_mul_sqrt_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c : A
hc : IsStrictlyPositive c
⊢ Eq (α := A) ((conjSqrt c⁻¹ʳ : (a : A) → A) c : A) (1 : A)

Tactic:
grind [conjSqrt_one c]

Premises used: CFC.conjSqrt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ≥0
hr : 0 < r
ha : 0 ≤ a
⊢ ‖a ^ r‖₊ = ‖a‖₊ ^ (↑r : ℝ)

Tactic:
NNReal.monotone_nnrpow_const r |>.monotoneOn _ |>.nnnorm_cfcₙ _ _

Premises used: CFC.nnrpow, NNReal.monotone_nnrpow_const, Monotone.monotoneOn, MonotoneOn.nnnorm_cfcₙ
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ≥0
hr : 0 < r
ha : 0 ≤ a
⊢ ‖a ^ r‖ = ‖a‖ ^ (↑r : ℝ)

Tactic:
congr(NNReal.toReal $(nnnorm_nnrpow a hr ha))

Premises used: congrArg, id, NNReal.toReal, CFC.nnnorm_nnrpow