awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})).Nonempty
have this : (ofReal ⁻¹' (σ ℂ a)ᶜ).Nonempty
Tactic: have := Filter.NeBot.nonempty_of_mem inferInstance <| Filter.mem_map.mp <|
      Complex.isometry_ofReal.antilipschitz.tendsto_cobounded (spectrum.isBounded a |>.compl)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})
have upper : {z : ℂ | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im}
Tactic: apply Complex.isConnected_of_upperHalfPlane ?_ <| Set.inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})
have upper : {z : ℂ | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im}
Tactic: case' upper => apply Complex.isConnected_of_upperHalfPlane ?_ <| Set.inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
have lower : {z : ℂ | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0}
Tactic: apply Complex.isConnected_of_lowerHalfPlane ?_ <| Set.inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
have lower : {z : ℂ | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0}
Tactic: case' lower => apply Complex.isConnected_of_lowerHalfPlane ?_ <| Set.inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z : ℂ | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0}
have lower : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.im < 0} z) (hz' : z ∈ σ ℂ a), False
Tactic: refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.im < 0} z
hz' : z ∈ σ ℂ a
⊢ False
have hz₁ : LT.lt (α := ℝ) 0 0
Tactic: rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z : ℂ | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im}
have upper : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z) (hz' : z ∈ σ ℂ a), False
Tactic: refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
hz' : z ∈ σ ℂ a
⊢ False
have hz₁ : LT.lt (α := ℝ) 0 0
Tactic: rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
⊢ IsUnit (↑a : A) ↔ IsUnit a
have refine : ∀ (ha : IsUnit (↑a : A)), IsUnit a
Tactic: refine ⟨fun ha ↦ ?_, IsUnit.map S.subtype⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
⊢ IsUnit a
have ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
Tactic: have ha₁ := ha.star.mul ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
⊢ IsUnit a
have ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
Tactic: have ha₂ := ha.mul ha.star
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
⊢ IsUnit a
have spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
Tactic: have spec_eq {x : S} (hx : IsSelfAdjoint x) : spectrum ℂ x = spectrum ℂ (x : A) :=
    Subalgebra.spectrum_eq_of_isPreconnected_compl S _ <|
      (hx.map S.subtype).isConnected_spectrum_compl.isPreconnected
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ IsUnit a
have rw : ∀ (ha₁ : IsUnit (a⋆ * a)) (ha₂ : IsUnit (a * a⋆)) (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)),
  IsUnit a
Tactic: rw [← StarMemClass.coe_star, ← MulMemClass.coe_mul, ← spectrum.zero_notMem_iff ℂ, ← spec_eq,
    spectrum.zero_notMem_iff] at ha₁ ha₂
Cleared hypotheses: ha₁, ha₂, spec_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
rw :
  ∀ (ha₁ : IsUnit (a⋆ * a)) (ha₂ : IsUnit (a * a⋆)) (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)),
    IsUnit a
⊢ IsUnit a
have rw₁ : ∀ (ha₁ : 0 ∉ σ ℂ (a⋆ * a)) (ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A))
  (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)), IsSelfAdjoint (a * a⋆)
Tactic: rw [← StarMemClass.coe_star, ← MulMemClass.coe_mul, ← spectrum.zero_notMem_iff ℂ, ← spec_eq,
    spectrum.zero_notMem_iff] at ha₁ ha₂
Cleared hypotheses: ha₁, ha₂, spec_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
rw :
  ∀ (ha₁ : IsUnit (a⋆ * a)) (ha₂ : IsUnit (a * a⋆)) (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)),
    IsUnit a
rw₁ :
  ∀ (ha₁ : 0 ∉ σ ℂ (a⋆ * a)) (ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A))
    (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)), IsSelfAdjoint (a * a⋆)
⊢ IsUnit a
have rw₂ : ∀ (ha₁ : 0 ∉ σ ℂ (↑(a⋆ * a) : A)) (ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A))
  (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)), IsSelfAdjoint (a⋆ * a)
Tactic: rw [← StarMemClass.coe_star, ← MulMemClass.coe_mul, ← spectrum.zero_notMem_iff ℂ, ← spec_eq,
    spectrum.zero_notMem_iff] at ha₁ ha₂
Cleared hypotheses: ha₁, ha₂, spec_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ IsUnit a
have h₁ : (↑ha₁.unit⁻¹ : ↥S) * a⋆ * a = 1
Tactic: have h₁ : ha₁.unit⁻¹ * star a * a = 1 := mul_assoc _ _ a ▸ ha₁.val_inv_mul
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
h₁ : (↑ha₁.unit⁻¹ : ↥S) * a⋆ * a = 1
⊢ IsUnit a
have h₂ : a * (a⋆ * (↑ha₂.unit⁻¹ : ↥S)) = 1
Tactic: have h₂ : a * (star a * ha₂.unit⁻¹) = 1 := (mul_assoc a _ _).symm ▸ ha₂.mul_val_inv
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤ ‖x‖₊
have refine : nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) *
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤
  ‖x‖₊ * ‖x‖₊
Tactic: refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) *
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤
    ‖x‖₊ * ‖x‖₊
have simp_rw : nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (x⋆ * x) : Unitization ℂ B) ≤
  ‖x⋆ * x‖₊
Tactic: simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤ ‖x‖₊
have suffices : ∀ {s : Unitization ℂ A},
  IsSelfAdjoint s →
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
Tactic: suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
      refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
      simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
      exact this <| .star_mul_self x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
this :
  spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
have rwa : ∀
  (this :
    (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
        ℝ≥0∞) ≤
      spectralRadius ℂ s),
  nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
Tactic: rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
this :
  spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s
rwa :
  ∀
    (this :
      (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
          ℝ≥0∞) ≤
        spectralRadius ℂ s),
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
have rwa₁ : ∀
  (this :
    (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
        ℝ≥0∞) ≤
      (↑‖s‖₊ : ℝ≥0∞)),
  nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
Tactic: rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
this :
  spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s
rwa :
  ∀
    (this :
      (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
          ℝ≥0∞) ≤
        spectralRadius ℂ s),
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
rwa₁ :
  ∀
    (this :
      (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
          ℝ≥0∞) ≤
        (↑‖s‖₊ : ℝ≥0∞)),
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
have rwa₂ : ∀
  (this :
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊),
  nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
Tactic: rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
have suffices : spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
  spectralRadius ℂ s
Tactic: suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
⊢ nnnorm.{u_3} (E := B) ((φ : (a : A) → B) a : B) ≤ ‖a‖₊
have h : ∀ (ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)) (x : Unitization ℂ A),
  nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤ ‖x‖₊
Tactic: have h (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A) :
      ‖ψ x‖₊ ≤ ‖x‖₊ := by
    suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
      refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
      simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
      exact this <| .star_mul_self x
    intro s hs
    suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
    exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
inst : CStarAlgebra A
inst_1 : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : ↥(selfAdjoint A)), Eq (α := ℂ) (((φ : (a : A) → ℂ) (↑s : A))⋆ : ℂ) ((φ : (a : A) → ℂ) (↑s : A) : ℂ)
⊢ Eq (α := ℂ) ((φ : (a : A) → ℂ) a⋆ : ℂ) (((φ : (a : A) → ℂ) a)⋆ : ℂ)
have rw : Eq (α := ℂ)
  ((φ : (a : A) → ℂ)
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))⋆ :
    ℂ)
  (((φ : (a : A) → ℂ)
        ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
          HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)))⋆ :
    ℂ)
Tactic: rw [← realPart_add_I_smul_imaginaryPart a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
inst : CStarAlgebra A
inst_1 : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ Eq (α := ℂ) ((φ : (a : A) → ℂ) a⋆ : ℂ) (((φ : (a : A) → ℂ) a)⋆ : ℂ)
have suffices : ∀ (s : ↥(selfAdjoint A)), Eq (α := ℂ) (((φ : (a : A) → ℂ) (↑s : A))⋆ : ℂ) ((φ : (a : A) → ℂ) (↑s : A) : ℂ)
Tactic: suffices hsa : ∀ s : selfAdjoint A, (φ s)⋆ = φ s by
      rw [← realPart_add_I_smul_imaginaryPart a]
      simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
F : Type u_1
A : Type u_2
inst : CStarAlgebra A
inst_1 : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : ↥(selfAdjoint A)
⊢ Eq (α := ℂ) (((φ : (a : A) → ℂ) (↑s : A))⋆ : ℂ) ((φ : (a : A) → ℂ) (↑s : A) : ℂ)
have rw : (↑(re ((φ : (a : A) → ℂ) (↑s : A))) : ℂ)⋆ = (↑(re ((φ : (a : A) → ℂ) (↑s : A))) : ℂ)
Tactic: rw [selfAdjoint.mem_spectrum_eq_re s (AlgHom.apply_mem_spectrum φ (s : A))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ 2 * (1 - z.re) ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2
have rw : √(2 * (1 - z.re)) ≤ ‖u - 1‖
Tactic: rw [← Real.sqrt_le_left (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ √(2 * (1 - z.re)) ≤ ‖u - 1‖
have this : Membership.mem (γ := Set ℂ) (sphere 0 1) z
Tactic: have := spectrum.subset_circle_of_unitary hu hz
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
this : Membership.mem (γ := Set ℂ) (sphere 0 1) z
⊢ √(2 * (1 - z.re)) ≤ ‖u - 1‖
have this₁ : ‖z‖ = 1
Tactic: simp only [mem_sphere_iff_norm, sub_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
this : ‖z‖ = 1
⊢ √(2 * (1 - z.re)) ≤ ‖u - 1‖
have rw : √(2 * (1 - z.re)) ≤ ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖
Tactic: rw [← cfc_id' ℂ u, ← cfc_one ℂ u, ← cfc_sub ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
this : ‖z‖ = 1
⊢ √(2 * (1 - z.re)) ≤ ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖
have h : √(2 * (1 - z.re)) = ‖z - 1‖
Tactic: convert! norm_apply_le_norm_cfc (fun z ↦ z - 1) u hz
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
have inl : Subsingleton A → HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
inl : Subsingleton A → HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
have inr : Nontrivial A → HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h : Subsingleton A
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h : Subsingleton A
⊢ False
have inl : spectrum ℂ u = ∅
Tactic: apply hz.nonempty.of_image.ne_empty
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h : Nontrivial A
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
have inr : HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)
Tactic: rw [← cfc_id' ℂ u, ← cfc_one ℂ u, ← cfc_sub ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h : Nontrivial A
⊢ HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)
have h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
Tactic: have h_eqOn : (spectrum ℂ u).EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) :=
    Complex.norm_sub_one_sq_eqOn_sphere.mono <| spectrum.subset_circle_of_unitary (𝕜 := ℂ) hu