awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
⊢ a = sqrt a * sqrt a

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
⊢ ∃ (b : A), 0 ≤ b ∧ a = b * b

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
⊢ ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
⊢ ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b

Tactic:
tfae_have 2 → 3 := fun h => ⟨sqrt a, sqrt_nonneg a, h⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
⊢ ∃ (b : A), 0 ≤ b ∧ a = b * b

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
⊢ ∃ (b : A), IsSelfAdjoint b ∧ a = b * b

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
⊢ ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
⊢ ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b

Tactic:
tfae_have 3 → 4 := fun ⟨b, hb⟩ => ⟨b, hb.1.isSelfAdjoint, hb.2⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
⊢ ∃ (b : A), IsSelfAdjoint b ∧ a = b * b

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
⊢ ∃ (b : A), a = star b * b

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
⊢ ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
⊢ ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b

Tactic:
tfae_have 4 → 5 := fun ⟨b, hb⟩ => ⟨b, hb.1.symm ▸ hb.2⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
⊢ ∃ (b : A), a = star b * b

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
⊢ ∃ (b : A), a = b * star b

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
⊢ ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b

Tactic:
5 → 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
⊢ ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b

Tactic:
tfae_have 5 → 6 := fun ⟨b, hb⟩ => ⟨star b, star_star b |>.symm ▸ hb⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
tfae_5_to_6 : ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b
⊢ ∃ (b : A), a = b * star b

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
tfae_5_to_6 : ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b
⊢ 0 ≤ a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
tfae_5_to_6 : ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b
⊢ ∀ (a_1 : ∃ (b : A), a = b * star b), 0 ≤ a

Tactic:
6 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
tfae_5_to_6 : ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b
⊢ ∀ (a_1 : ∃ (b : A), a = b * star b), 0 ≤ a

Tactic:
tfae_have 6 → 1 := fun ⟨b, hb⟩ => hb ▸ mul_star_self_nonneg _
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
tfae_1_iff_9 :
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
tfae_1_iff_8 : 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
tfae_2_to_3 : ∀ (a_1 : a = sqrt a * sqrt a), ∃ (b : A), 0 ≤ b ∧ a = b * b
tfae_3_to_4 : ∀ (a_1 : ∃ (b : A), 0 ≤ b ∧ a = b * b), ∃ (b : A), IsSelfAdjoint b ∧ a = b * b
tfae_4_to_5 : ∀ (a_1 : ∃ (b : A), IsSelfAdjoint b ∧ a = b * b), ∃ (b : A), a = star b * b
tfae_5_to_6 : ∀ (a_1 : ∃ (b : A), a = star b * b), ∃ (b : A), a = b * star b
tfae_6_to_1 : ∀ (a_1 : ∃ (b : A), a = b * star b), 0 ≤ a
⊢ [0 ≤ a, a = sqrt a * sqrt a, ∃ (b : A), 0 ≤ b ∧ a = b * b, ∃ (b : A), IsSelfAdjoint b ∧ a = b * b,
      ∃ (b : A), a = star b * b, ∃ (b : A), a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
⊢ 0 ≤ a ↔ a = sqrt a * sqrt a

Tactic:
CStarAlgebra.nonneg_TFAE.out 0 1

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

Tactic:
CStarAlgebra.nonneg_TFAE.out 0 2

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

Tactic:
CStarAlgebra.nonneg_TFAE.out 0 3

Premises used: List.TFAE.out, CStarAlgebra.nonneg_TFAE, OfNat.ofNat