awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x_2 p x y : A
hx_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
hy_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : IsSelfAdjoint y ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (x + y) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr : ∀
  (hx :
    IsSelfAdjoint (R := Unitization ℂ A) (↑x : Unitization ℂ A) ∧
      SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑x : Unitization ℂ A)
        (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0))
  (hy :
    IsSelfAdjoint (R := Unitization ℂ A) (↑y : Unitization ℂ A) ∧
      SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑y : Unitization ℂ A)
        (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)),
  IsSelfAdjoint (R := Unitization ℂ A) (↑(x + y) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(x + y) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x_2 p x y : A
hx_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
hy_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx :
  IsSelfAdjoint (R := Unitization ℂ A) (↑x : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑x : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑y : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑y : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (R := Unitization ℂ A) (↑(x + y) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(x + y) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr : IsSelfAdjoint (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
  SpectrumRestricts (R := ℝ≥0) (S := ℝ) (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: rw [Unitization.inr_add]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
hp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p
⊢ IsSelfAdjoint p ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) p (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr : ∀ (x : A) (hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x),
  IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: induction hp using AddSubmonoid.closure_induction with
        | mem x hx =>
          obtain ⟨s, rfl⟩ := hx
          refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
            SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
          exact spectrum_star_mul_self_nonneg
        | zero =>
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
          simp
        | add x y _ _ hx hy =>
          simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
          rw [Unitization.inr_add]
          exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
hp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p
mpr :
  ∀ (x : A) (hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x),
    IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint p ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) p (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr₁ : IsSelfAdjoint.{u_1} (R := A) 0 ∧
  QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: induction hp using AddSubmonoid.closure_induction with
        | mem x hx =>
          obtain ⟨s, rfl⟩ := hx
          refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
            SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
          exact spectrum_star_mul_self_nonneg
        | zero =>
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
          simp
        | add x y _ _ hx hy =>
          simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
          rw [Unitization.inr_add]
          exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
hp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p
mpr :
  ∀ (x : A) (hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x),
    IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
mpr₁ :
  IsSelfAdjoint.{u_1} (R := A) 0 ∧
    QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint p ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) p (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr₂ : ∀ (x y : A),
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x →
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y →
      ∀
        (hx :
          IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0))
        (hy :
          IsSelfAdjoint y ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)),
        IsSelfAdjoint (x + y) ∧
          QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: induction hp using AddSubmonoid.closure_induction with
        | mem x hx =>
          obtain ⟨s, rfl⟩ := hx
          refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
            SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
          exact spectrum_star_mul_self_nonneg
        | zero =>
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
          simp
        | add x y _ _ hx hy =>
          simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
          rw [Unitization.inr_add]
          exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ ∀ x ∈ σₙ ℝ a, 0 ≤ x
have rw : ∀ x ∈ spectrum ℝ (A := Unitization ℂ A) (↑a : Unitization ℂ A), 0 ≤ x
Tactic: rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
⊢ ∀ x ∈ spectrum ℝ (A := Unitization ℂ A) (↑a : Unitization ℂ A), 0 ≤ x
have this : StarOrderedRing.{u_1} (Unitization ℂ A)
Tactic: have := CStarAlgebra.spectralOrderedRing A⁺¹
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this : StarOrderedRing.{u_1} (Unitization ℂ A)
⊢ ∀ x ∈ spectrum ℝ (A := Unitization ℂ A) (↑a : Unitization ℂ A), 0 ≤ x
have ha₁ : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: apply spectrum_nonneg_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this : StarOrderedRing.{u_1} (Unitization ℂ A)
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
have ha₁ : ∀ (ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a)
  (this : StarOrderedRing.{u_1} (Unitization ℂ A)),
  Membership.mem (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure (Set.range fun (s : Unitization ℂ A) ↦ star s * s)) (↑a : Unitization ℂ A)
Tactic: rw [StarOrderedRing.nonneg_iff] at ha ⊢
Cleared hypotheses: ha, x, this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this : StarOrderedRing.{u_1} (Unitization ℂ A)
⊢ Membership.mem (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure (Set.range fun (s : Unitization ℂ A) ↦ star s * s)) (↑a : Unitization ℂ A)
have this₁ : Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
  (AddSubmonoid.map (F := A →⋆ₙₐ[ℂ] Unitization ℂ A) (Unitization.inrNonUnitalStarAlgHom ℂ A)
    (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)))
  ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
Tactic: have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this_1 : StarOrderedRing.{u_1} (Unitization ℂ A)
this :
  Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.map (F := A →⋆ₙₐ[ℂ] Unitization ℂ A) (Unitization.inrNonUnitalStarAlgHom ℂ A)
      (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
⊢ Membership.mem (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure (Set.range fun (s : Unitization ℂ A) ↦ star s * s)) (↑a : Unitization ℂ A)
have this₁ : Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
  (AddSubmonoid.closure
    (Set.range (ι := A)
      (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
        star s * s)))
  ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
Tactic: rw [AddMonoidHom.map_mclosure, ← Set.range_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this_1 : StarOrderedRing.{u_1} (Unitization ℂ A)
this :
  Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure
      (Set.range (ι := A)
        (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
          star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
⊢ Membership.mem (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure (Set.range fun (s : Unitization ℂ A) ↦ star s * s)) (↑a : Unitization ℂ A)
have apply : Subset (α := Set (Unitization ℂ A))
  (Set.range (ι := A)
    (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
      star s * s))
  (Set.range fun (s : Unitization ℂ A) ↦ star s * s)
Tactic: apply AddSubmonoid.closure_mono ?_ this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have pos : ∀ (h : ContinuousOn f (σₙ R a) ∧ p a), (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: by_cases h : ContinuousOn f (σₙ R a) ∧ p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
pos :
  ∀ (h : ContinuousOn f (σₙ R a) ∧ p a),
    (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg : ∀ (h : ¬(ContinuousOn f (σₙ R a) ∧ p a)),
  (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: by_cases h : ContinuousOn f (σₙ R a) ∧ p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ContinuousOn f (σₙ R a) ∧ p a
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have hf : ContinuousOn f (σₙ R a)
Tactic: obtain ⟨hf, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ContinuousOn f (σₙ R a) ∧ p a
hf : ContinuousOn f (σₙ R a)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have ha : p a
Tactic: obtain ⟨hf, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
hf : ContinuousOn f (σₙ R a)
ha : p a
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have pos : (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfcₙ (p := p') f (↑a : Unitization ℂ A)
Tactic: rw [← cfcₙ_eq_cfc (quasispectrum_inr_eq R ℂ a ▸ hf)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: obtain (hf | ha) := not_and_or.mp h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
neg :
  ∀ (hf : ¬ContinuousOn f (σₙ R a)), (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg₁ : ∀ (ha : ¬p a), (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: obtain (hf | ha) := not_and_or.mp h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg : (↑0 : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
        cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
neg : (↑0 : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg₁ : 0 = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
        cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]