awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ sqrt (a, b) = (sqrt a, sqrt b)
have simp : (a, b) ^ (1 / 2) = (a ^ (1 / 2), b ^ (1 / 2))
Tactic: simp only [sqrt_eq_nnrpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ sqrt c = fun (i : ι) ↦ sqrt (c i)
have simp : c ^ (1 / 2) = fun (i : ι) ↦ c i ^ (1 / 2)
Tactic: simp only [sqrt_eq_nnrpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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, ∃ (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
have tfae_1_iff_9 : 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: tfae_have 1 ↔ 9 := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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 = 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
have tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
Tactic: tfae_have 1 ↔ 7 := eq_comm.eq ▸ (CFC.posPart_eq_self a).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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, 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
have tfae_1_iff_8 : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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, 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
have tfae_1_to_2 : ∀ (a_1 : 0 ≤ a), a = sqrt a * sqrt a
Tactic: tfae_have 1 → 2 := fun h => sqrt_mul_sqrt_self a |>.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ [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
have tfae_2_to_3 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ [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
have tfae_3_to_4 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ [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
have tfae_4_to_5 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ [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
have tfae_5_to_6 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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, 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
have tfae_6_to_1 : ∀ (a_1 : ∃ (b : A), a = b * star b), 0 ≤ a
Tactic: tfae_have 6 → 1 := fun ⟨b, hb⟩ => hb ▸ mul_star_self_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
y : ℝ
ha : 0 ≤ a
⊢ a ^ y = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ y) a
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal ^ y) : ℝ)) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ y) a
Tactic: rw [CFC.rpow_def, cfc_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
y : ℝ
ha : 0 ≤ a
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal ^ y) : ℝ)) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ y) a
have refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(x.toNNReal ^ y) : ℝ)) (fun (x : ℝ) ↦ x ^ y) (spectrum ℝ a)
Tactic: refine cfc_congr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ cfc (p := IsSelfAdjoint) f a ^ y = cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ f r ^ y) a
have hg : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ r ^ y) (f '' spectrum ℝ a)
Tactic: have hg : ContinuousOn (fun r => r ^ y) (f '' spectrum ℝ a) :=
    ContinuousOn.rpow_const (f := id) (by fun_prop) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
hg : ContinuousOn (Y := ℝ) (fun (r : ℝ) ↦ r ^ y) (f '' spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) f a ^ y = cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ f r ^ y) a
have rw : cfc (p := IsSelfAdjoint) ((fun (x : ℝ) ↦ x ^ y) ∘ f) a = cfc (p := IsSelfAdjoint) (fun (r : ℝ) ↦ f r ^ y) a
Tactic: rw [CFC.rpow_eq_cfc_real (by grind [cfc_nonneg]), ← cfc_comp _ _ a ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
a : A
n : ℕ
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ) a (↑n : ℝ) = a ^ n
have rw : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) a
Tactic: rw [← cfc_pow_id (R := ℝ≥0) a n, rpow_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
a : A
n : ℕ
ha : 0 ≤ a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) a
have e_f : Eq (α := ℝ≥0 → ℝ≥0) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) fun (x : ℝ≥0) ↦ x ^ n
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
x : ℝ≥0
y : ℝ
⊢ HPow.hPow (α := A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) x : A) y = (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (x ^ y)
have rw : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) x) =
  (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (x ^ y)
Tactic: rw [rpow_def, cfc_algebraMap ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
x : ℝ≥0
y : ℝ
rw :
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) x) =
    (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (x ^ y)
⊢ HPow.hPow (α := A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) x : A) y = (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (x ^ y)
have rw₁ : Eq (α := A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (x ^ y) : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (x ^ y) : A)
Tactic: rw [rpow_def, cfc_algebraMap ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
a : A
x y : ℝ
ha : IsUnit a
⊢ a ^ (x + y) = a ^ x * a ^ y
have ha' : 0 ∉ spectrum ℝ≥0 a
Tactic: have ha' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
a : A
x y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
⊢ a ^ (x + y) = a ^ x * a ^ y
have simp : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x + y)) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a *
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a
Tactic: simp only [rpow_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
a : A
x y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x + y)) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a *
      cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a
have rw : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x + y)) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x * x_1 ^ y) a
Tactic: rw [← cfc_mul _ _ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
a : A
x y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x + y)) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x * x_1 ^ y) a
have refine : Set.EqOn (β := ℝ≥0) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x + y)) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x * x_1 ^ y) (spectrum ℝ≥0 a)
Tactic: refine cfc_congr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
a : A
x y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
⊢ Eq (α := ℝ≥0) ((fun (x_1 : ℝ≥0) ↦ x_1 ^ (x + y)) z) ((fun (x_1 : ℝ≥0) ↦ x_1 ^ x * x_1 ^ y) z)
have this : z ≠ 0
Tactic: have : z ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x) ^ y = a ^ (x * y)
have ha₁' : 0 ∉ spectrum ℝ≥0 a
Tactic: have ha₁' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha.isUnit
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
ha₁' : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y)
      (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
have rw : cfc (R := ℝ≥0) (p := LE.le 0) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
Tactic: rw [← cfc_comp _ _ a ha.nonneg]