awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)
have ha' : q a
Tactic: obtain ⟨ha', haf⟩ := h a |>.mp ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)
have haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
Tactic: obtain ⟨ha', haf⟩ := h a |>.mp ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)
have rw : Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
  (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)
Tactic: rw [cfcₙHom_eq_restrict f ha ha' haf]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
⊢ Isometry.{u_1, u_3} (α := ContinuousMapZero (↑(σₙ R a) : Type u_1) R) (β := A)
    (⇑(nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf) : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A)
have refine : ∀ (g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R),
  dist.{u_3} (α := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₁ : A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₂ : A) =
    dist g₁ g₂
Tactic: refine .of_dist_eq fun g₁ g₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
⊢ dist.{u_3} (α := A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₁ : A)
      ((nonUnitalStarAlgHom (cfcₙHom (p := q) ha') haf : (a : ContinuousMapZero (↑(σₙ R a) : Type u_1) R) → A) g₂ : A) =
    dist g₁ g₂
have simp : dist (α := ContinuousMapZero (↑(σₙ S a) : Type u_2) S)
    (ContinuousMapZero.comp
      { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry : ContinuousMapZero R S }
      (g₁.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry, map_zero' := sorry :
          ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))
    (ContinuousMapZero.comp
      { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry, map_zero' := sorry : ContinuousMapZero R S }
      (g₂.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry, map_zero' := sorry :
          ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) =
  dist g₁ g₂
Tactic: simp only [nonUnitalStarAlgHom_apply, isometry_cfcₙHom a ha' |>.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
x : (↑(σₙ R a) : Type u_1)
x' : (↑(σₙ S a) : Type u_2) :=
  Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a) (⇑(algebraMap R S) : (a : R) → S) ⋯ x
⊢ dist (α := R) ((g₁ : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g₂ : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) =
    dist (α := R)
      ((g₁ : (a : (↑(σₙ R a) : Type u_1)) → R)
          (Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯
            (Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a)
              (⇑(algebraMap R S) : (a : R) → S) ⋯ x)) :
        R)
      ((g₂ : (a : (↑(σₙ R a) : Type u_1)) → R)
          (Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯
            (Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a)
              (⇑(algebraMap R S) : (a : R) → S) ⋯ x)) :
        R)
have h₁ : x =
  Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry
    (Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a) (⇑(algebraMap R S) : (a : R) → S) sorry x)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
x : (↑(σₙ R a) : Type u_1)
x' : (↑(σₙ S a) : Type u_2) :=
  Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a) (⇑(algebraMap R S) : (a : R) → S) ⋯ x
⊢ x =
    Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯
      (Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a) (⇑(algebraMap R S) : (a : R) → S) ⋯
        x)
have h₁ : (↑x : R) =
  (↑(Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) sorry
        (Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a) (⇑(algebraMap R S) : (a : R) → S) sorry
          x)) :
    R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
have rw : IsGreatest (f '' σ ℝ≥0 a) ‖cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
Tactic: rw [cfc_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: obtain ⟨-, ha'⟩ := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mp ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have ha'₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: rw [← SpectrumRestricts] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have h : f '' σ ℝ≥0 a = (fun (x : ℝ) ↦ ‖(↑(f x.toNNReal) : ℝ)‖₊) '' σ ℝ a
Tactic: convert! IsGreatest.nnnorm_cfc (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h : f '' σ ℝ≥0 a = (fun (x : ℝ) ↦ ‖(↑(f x.toNNReal) : ℝ)‖₊) '' σ ℝ a
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have convert! : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σ ℝ a)
Tactic: convert! IsGreatest.nnnorm_cfc (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ f x ≤ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
have revert : ∀ (hx : x ∈ σ ℝ≥0 a), f x ≤ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ∀ (hx : x ∈ σ ℝ≥0 a), f x ≤ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
have inl : Subsingleton A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
inl : Subsingleton A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
have inr : Nontrivial A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h_1 : Subsingleton A
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
have inl : nnnorm.{u_1} (E := A) 0 ≤ c
Tactic: rw [Subsingleton.elim (cfc f a) 0]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h_1 : Nontrivial A
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
have inr : ∀ (hf : ContinuousOn f (σ ℝ≥0 a)) (ha : 0 ≤ a),
  (fun (x : A) ↦ ‖x‖₊ ≤ c)
    ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
      { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := sorry : C((↑(σ ℝ≥0 a) : Type), ℝ≥0) })
Tactic: refine cfc_cases (‖·‖₊ ≤ c) a f (by simp) fun hf ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ (fun (x : A) ↦ ‖x‖₊ ≤ c)
    ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
      { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ : C((↑(σ ℝ≥0 a) : Type), ℝ≥0) })
have inr : c ∈ upperBounds (f '' σ ℝ≥0 a)
Tactic: simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.isLUB)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
have inl : Subsingleton A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
inl : Subsingleton A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
have inr : Nontrivial A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Subsingleton A
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
have inl : nnnorm.{u_1} (E := A) 0 < c
Tactic: rw [Subsingleton.elim (cfc f a) 0]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
have inr : ∀ (hf : ContinuousOn f (σ ℝ≥0 a)) (ha : 0 ≤ a),
  (fun (x : A) ↦ ‖x‖₊ < c)
    ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
      { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := sorry : C((↑(σ ℝ≥0 a) : Type), ℝ≥0) })
Tactic: refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_