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 b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ sqrt a = b ↔ b * b = a

Tactic:
⟨(mul_self_eq ·), (sqrt_unique ·)⟩

Premises used: CFC.sqrt_unique, Iff.intro, CFC.mul_self_eq
-- 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
ha : 0 ≤ a
rw : HMul.hMul (α := A) 0 0 = a ↔ a = 0
rw₁ : 0 = a ↔ a = 0
rw₂ rw₃ : a = 0 ↔ a = 0
⊢ sqrt a = 0 ↔ a = 0

Tactic:
rw [sqrt_eq_iff a _, mul_zero, eq_comm]

Premises used: CFC.sqrt_eq_iff, eq_comm, MulZeroClass.mul_zero
-- 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 b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * a = b * b ↔ a = b

Tactic:
⟨fun h => sqrt_mul_self a ▸ sqrt_unique h.symm, fun h => h ▸ rfl⟩

Premises used: CFC.sqrt_unique, Eq.rec, Iff.intro, Eq.symm, rfl, CFC.sqrt_mul_self
-- 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
ha : 0 ≤ a
this : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a
rwa :
  ∀
    (this :
      cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a =
        cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a),
    sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
rwa₁ :
  ∀ (this : cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a = a),
    sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a), sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
⊢ sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a

Tactic:
rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] at this

Premises used: CFC.sqrt_eq_iff, cfcₙ_id', cfcₙ_mul, Real.sqrt_nonneg, cfcₙ_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
ha : 0 ≤ a
suffices : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a
⊢ sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a

Tactic:
suffices cfcₙ (fun x : ℝ ↦ √x * √x) a = cfcₙ (fun x : ℝ ↦ x) a by
    rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] at this
-- 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
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a

Tactic:
cfcₙ_congr fun x hx ↦ Real.mul_self_sqrt <| quasispectrum_nonneg_of_nonneg a ha x hx

Premises used: Real.mul_self_sqrt, cfcₙ_congr, NonnegSpectrumClass.quasispectrum_nonneg_of_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
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a

Tactic:
exact cfcₙ_congr fun x hx ↦ Real.mul_self_sqrt <| quasispectrum_nonneg_of_nonneg a ha x hx

Premises used: Real.mul_self_sqrt, cfcₙ_congr, NonnegSpectrumClass.quasispectrum_nonneg_of_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
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : StarOrderedRing B
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_21 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_22 : IsSemitopologicalRing B
inst_23 : T2Space B
inst_24 : NonnegSpectrumClass ℝ B
inst_25 : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
ha : 0 ≤ a
hb : 0 ≤ b
simp : (a, b) ^ (1 / 2) = (a ^ (1 / 2), b ^ (1 / 2))
⊢ sqrt (a, b) = (sqrt a, sqrt b)

Tactic:
simp only [sqrt_eq_nnrpow]

Premises used: CFC.sqrt_eq_nnrpow
-- 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
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : StarOrderedRing B
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_21 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_22 : IsSemitopologicalRing B
inst_23 : T2Space B
inst_24 : NonnegSpectrumClass ℝ B
inst_25 : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a, b) ^ (1 / 2) = (a ^ (1 / 2), b ^ (1 / 2))

Tactic:
nnrpow_map_prod

Premises used: CFC.nnrpow_map_prod
-- 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
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : StarOrderedRing B
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_21 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_22 : IsSemitopologicalRing B
inst_23 : T2Space B
inst_24 : NonnegSpectrumClass ℝ B
inst_25 : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a, b) ^ (1 / 2) = (a ^ (1 / 2), b ^ (1 / 2))

Tactic:
exact nnrpow_map_prod

Premises used: CFC.nnrpow_map_prod
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → NonUnitalRing (C i)
inst_2 : (i : ι) → TopologicalSpace (C i)
inst_3 : (i : ι) → StarRing (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Module ℝ (C i)
inst_7 : ∀ (i : ι), SMulCommClass.{0, u_3, u_3} ℝ (C i) (C i)
inst_8 : ∀ (i : ι), IsScalarTower.{0, u_3, u_3} ℝ (C i) (C i)
inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_11 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_12 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_14 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
hc : ∀ (i : ι), 0 ≤ c i
simp : c ^ (1 / 2) = fun (i : ι) ↦ c i ^ (1 / 2)
⊢ sqrt c = fun (i : ι) ↦ sqrt (c i)

Tactic:
simp only [sqrt_eq_nnrpow]

Premises used: CFC.sqrt_eq_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → NonUnitalRing (C i)
inst_2 : (i : ι) → TopologicalSpace (C i)
inst_3 : (i : ι) → StarRing (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Module ℝ (C i)
inst_7 : ∀ (i : ι), SMulCommClass.{0, u_3, u_3} ℝ (C i) (C i)
inst_8 : ∀ (i : ι), IsScalarTower.{0, u_3, u_3} ℝ (C i) (C i)
inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_11 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_12 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_14 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
hc : ∀ (i : ι), 0 ≤ c i
⊢ c ^ (1 / 2) = fun (i : ι) ↦ c i ^ (1 / 2)

Tactic:
nnrpow_map_pi

Premises used: CFC.nnrpow_map_pi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → NonUnitalRing (C i)
inst_2 : (i : ι) → TopologicalSpace (C i)
inst_3 : (i : ι) → StarRing (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Module ℝ (C i)
inst_7 : ∀ (i : ι), SMulCommClass.{0, u_3, u_3} ℝ (C i) (C i)
inst_8 : ∀ (i : ι), IsScalarTower.{0, u_3, u_3} ℝ (C i) (C i)
inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_11 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_12 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_14 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
hc : ∀ (i : ι), 0 ≤ c i
⊢ c ^ (1 / 2) = fun (i : ι) ↦ c i ^ (1 / 2)

Tactic:
exact nnrpow_map_pi

Premises used: CFC.nnrpow_map_pi
-- 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

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
⊢ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
9

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
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
1 ↔ 9

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
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
tfae_have 1 ↔ 9 := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts

Premises used: nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- 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)
⊢ 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)
⊢ a = a⁺

Tactic:
7

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)
⊢ 0 ≤ a ↔ a = a⁺

Tactic:
1 ↔ 7

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)
⊢ 0 ≤ a ↔ a = a⁺

Tactic:
tfae_have 1 ↔ 7 := eq_comm.eq ▸ (CFC.posPart_eq_self a).symm
-- 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⁺
⊢ 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⁺
⊢ IsSelfAdjoint a ∧ a⁻ = 0

Tactic:
8

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⁺
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0

Tactic:
1 ↔ 8

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⁺
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0

Tactic:
tfae_have 1 ↔ 8 := ⟨fun h => ⟨h.isSelfAdjoint, negPart_eq_zero_iff a |>.mpr h⟩,
    fun h => negPart_eq_zero_iff a |>.mp h.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
⊢ 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
⊢ 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
⊢ ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a

Tactic:
1 → 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
⊢ ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a

Tactic:
tfae_have 1 → 2 := fun h => sqrt_mul_sqrt_self a |>.symm

Premises used: Eq.symm, CFC.sqrt_mul_sqrt_self