awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s

Tactic:
exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)

Premises used: AlgHom.spectrum_apply_subset, iSup_le_iSup_of_subset
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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‖₊

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)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
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‖₊
⊢ nnnorm.{u_3} (E := B) ((φ : (a : A) → B) a : B) ≤ ‖a‖₊

Tactic:
simpa [nnnorm_inr] using h (starLift (inrNonUnitalStarAlgHom ℂ B |>.comp (φ : A →⋆ₙₐ[ℂ] B))) a

Premises used: Unitization.inr, Unitization.inrNonUnitalStarAlgHom, NonUnitalStarAlgHom.comp, Unitization.starLift, NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom, Complex, DFunLike.coe, Unitization.nnnorm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ norm.{u_3} (E := B) ((φ : (a : A) → B) a : B) ≤ ‖a‖

Tactic:
exact_mod_cast nnnorm_apply_le φ a

Premises used: NonUnitalStarAlgHom.nnnorm_apply_le
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ ∀ (x : A), norm.{u_3} (E := B) ((φ : (a : A) → B) x : B) ≤ 1 * ‖x‖

Tactic:
simpa only [one_mul] using nnnorm_apply_le φ

Premises used: NonUnitalStarAlgHom.nnnorm_apply_le, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : EquivLike F A B
inst_3 : NonUnitalAlgEquivClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
⊢ ‖a‖₊ ≤ nnnorm.{u_3} (E := B) ((φ : (a : A) → B) a : B)

Tactic:
simpa using NonUnitalStarAlgHom.nnnorm_apply_le (symm (φ : A ≃⋆ₐ[ℂ] B)) ((φ : A ≃⋆ₐ[ℂ] B) a)

Premises used: NonUnitalStarAlgHom.nnnorm_apply_le, StarAlgEquivClass.toStarAlgEquiv, StarAlgEquiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : EquivLike F A B
inst_3 : NonUnitalAlgEquivClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
⊢ norm.{u_3} (E := B) ((φ : (a : A) → B) a : B) = ‖a‖

Tactic:
congr_arg NNReal.toReal (nnnorm_map φ a)

Premises used: congr_arg, StarAlgEquiv.nnnorm_map, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : EquivLike F A B
inst_3 : NonUnitalAlgEquivClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
⊢ Isometry.{u_2, u_3} (α := A) (β := B) (⇑φ : (a : A) → B)

Tactic:
AddMonoidHomClass.isometry_of_norm φ (norm_map φ)

Premises used: StarAlgEquiv.norm_map, AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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) : ℂ)
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)))⋆ :
      ℂ)
⊢ Eq (α := ℂ) ((φ : (a : A) → ℂ) a⋆ : ℂ) (((φ : (a : A) → ℂ) a)⋆ : ℂ)

Tactic:
rw [← realPart_add_I_smul_imaginaryPart a]

Premises used: realPart_add_I_smul_imaginaryPart
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 →ₗ[ℝ] ↥(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:
simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]

Premises used: StarAddMonoid.star_add, StarModule.star_smul, selfAdjoint.star_val_eq, map_add, map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
inst : CStarAlgebra A
inst_1 : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
suffices : ∀ (s : ↥(selfAdjoint A)), Eq (α := ℂ) (((φ : (a : A) → ℂ) (↑s : A))⋆ : ℂ) ((φ : (a : A) → ℂ) (↑s : A) : ℂ)
⊢ Eq (α := ℂ) ((φ : (a : A) → ℂ) a⋆ : ℂ) (((φ : (a : A) → ℂ) 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]
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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)
rw : (↑(re ((φ : (a : A) → ℂ) (↑s : A))) : ℂ)⋆ = (↑(re ((φ : (a : A) → ℂ) (↑s : A))) : ℂ)
⊢ Eq (α := ℂ) (((φ : (a : A) → ℂ) (↑s : A))⋆ : ℂ) ((φ : (a : A) → ℂ) (↑s : A) : ℂ)

Tactic:
rw [selfAdjoint.mem_spectrum_eq_re s (AlgHom.apply_mem_spectrum φ (s : A))]

Premises used: AlgHom.apply_mem_spectrum, selfAdjoint.mem_spectrum_eq_re, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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)
⊢ (↑(re ((φ : (a : A) → ℂ) (↑s : A))) : ℂ)⋆ = (↑(re ((φ : (a : A) → ℂ) (↑s : A))) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
inst : CStarAlgebra A
inst_1 : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
⊢ StarHomClass F A ℂ

Tactic:
{ WeakDual.Complex.instStarHomClass, hF with }

Premises used: WeakDual.Complex.instStarHomClass
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
inst : CStarAlgebra A
inst_1 : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
⊢ StarHomClass (↑(characterSpace ℂ A) : Type u_2) A ℂ

Tactic:
{ AlgHomClass.instStarHomClass with }

Premises used: AlgHomClass.instStarHomClass
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ 0 ≤ ‖u - 1‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
rw : √(2 * (1 - z.re)) ≤ ‖u - 1‖
⊢ 2 * (1 - z.re) ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2

Tactic:
rw [← Real.sqrt_le_left (by positivity)]

Premises used: Real.sqrt_le_left
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ Membership.mem (γ := Set ℂ) (sphere 0 1) z

Tactic:
have := spectrum.subset_circle_of_unitary hu hz
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
⊢ ‖z‖ = 1

Tactic:
simp only [mem_sphere_iff_norm, sub_zero] at this

Premises used: sub_zero, mem_sphere_iff_norm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
rw : √(2 * (1 - z.re)) ≤ ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖
⊢ √(2 * (1 - z.re)) ≤ ‖u - 1‖

Tactic:
rw [← cfc_id' ℂ u, ← cfc_one ℂ u, ← cfc_sub ..]

Premises used: cfc_sub, cfc_id', cfc_one, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
⊢ norm (E := ℂ) ((fun (z : ℂ) ↦ z - 1) z) ≤ ‖cfc (p := IsStarNormal) (fun (z : ℂ) ↦ z - 1) u‖

Tactic:
norm_apply_le_norm_cfc (fun z ↦ z - 1) u hz

Premises used: HSub.hSub, norm_apply_le_norm_cfc, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h : √(2 * (1 - z.re)) = ‖z - 1‖
⊢ √(2 * (1 - z.re)) ≤ ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖

Tactic:
convert! norm_apply_le_norm_cfc (fun z ↦ z - 1) u hz

Premises used: HSub.hSub, norm_apply_le_norm_cfc, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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)) = ‖z - 1‖

Tactic:
simpa using congr(Real.sqrt $(norm_sub_one_sq_eq_of_norm_eq_one this)).symm

Premises used: Complex.norm_sub_one_sq_eq_of_norm_eq_one, congrArg, id, Real.sqrt, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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)
inr : Nontrivial A → HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
inl : False
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)

Tactic:
exfalso
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
inl : spectrum ℂ u = ∅
⊢ False

Tactic:
apply hz.nonempty.of_image.ne_empty

Premises used: Set.Nonempty.ne_empty, IsLeast.nonempty, Set.Nonempty.of_image
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
⊢ spectrum ℂ u = ∅

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
inr : HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 = 2 * (1 - x)

Tactic:
rw [← cfc_id' ℂ u, ← cfc_one ℂ u, ← cfc_sub ..]

Premises used: cfc_sub, cfc_id', cfc_one, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
a : ℝ
_ : ∀ ⦃b : ℝ⦄, a ≤ b → LE.le (α := ℝ) ((fun (y : ℝ) ↦ 2 * (1 - y)) b) ((fun (y : ℝ) ↦ 2 * (1 - y)) a)
⊢ ∀ ⦃b : ℝ⦄, a ≤ b → LE.le (α := ℝ) ((fun (y : ℝ) ↦ 2 * (1 - y)) b) ((fun (y : ℝ) ↦ 2 * (1 - y)) a)

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
a b : ℝ
_ : a ≤ b → LE.le (α := ℝ) ((fun (y : ℝ) ↦ 2 * (1 - y)) b) ((fun (y : ℝ) ↦ 2 * (1 - y)) a)
⊢ a ≤ b → LE.le (α := ℝ) ((fun (y : ℝ) ↦ 2 * (1 - y)) b) ((fun (y : ℝ) ↦ 2 * (1 - y)) a)

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
a b : ℝ
h_1 : a ≤ b
ha : LE.le (α := ℝ) 0 2
⊢ 2 * (1 - b) ≤ 2 * (1 - a)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
⊢ Antitone (β := ℝ) fun (y : ℝ) ↦ 2 * (1 - y)

Tactic:
have : Antitone (fun y : ℝ ↦ 2 * (1 - y)) := by intro _ _ _; simp only; gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
this : Antitone (β := ℝ) fun (y : ℝ) ↦ 2 * (1 - y)
⊢ IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))

Tactic:
simpa [Set.image_image] using this.map_isLeast hz

Premises used: Set.image_image, Antitone.map_isLeast
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
⊢ IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))

Tactic:
have h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' (spectrum ℂ u)) (2 * (1 - x)) := by
    have : Antitone (fun y : ℝ ↦ 2 * (1 - y)) := by intro _ _ _; simp only; gcongr
    simpa [Set.image_image] using this.map_isLeast hz
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ Subset (α := Set ℝ) ((fun (x : ℂ) ↦ ‖x - 1‖) '' spectrum ℂ u) {x : ℝ | 0 ≤ x}

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ MonotoneOn (β := ℝ) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) a 2) ((fun (x : ℂ) ↦ ‖x - 1‖) '' spectrum ℂ u)

Tactic:
have := pow_left_monotoneOn (n := 2) |>.mono (s₂ := ((‖· - 1‖) '' spectrum ℂ u)) (by simp)
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
this : MonotoneOn (β := ℝ) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) a 2) ((fun (x : ℂ) ↦ ‖x - 1‖) '' spectrum ℂ u)
⊢ IsGreatest ((fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x - 1‖ 2) '' spectrum ℂ u)
    (HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1) u‖ 2)

Tactic:
simpa [Set.image_image] using this.map_isGreatest (IsGreatest.norm_cfc (fun z : ℂ ↦ z - 1) u)

Premises used: Set.image_image, MonotoneOn.map_isGreatest, HSub.hSub, IsGreatest.norm_cfc, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ IsGreatest ((fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x - 1‖ 2) '' spectrum ℂ u)
    (HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1) u‖ 2)

Tactic:
have h₃ : IsGreatest ((‖· - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (· - 1 : ℂ → ℂ) u‖ ^ 2) := by
    have := pow_left_monotoneOn (n := 2) |>.mono (s₂ := ((‖· - 1‖) '' spectrum ℂ u)) (by simp)
    simpa [Set.image_image] using this.map_isGreatest (IsGreatest.norm_cfc (fun z : ℂ ↦ z - 1) u)
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
h₃ :
  IsGreatest ((fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x - 1‖ 2) '' spectrum ℂ u)
    (HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1) u‖ 2)
⊢ HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)

Tactic:
h₃.unique (h_eqOn.image_eq ▸ h₂)

Premises used: Eq.rec, IsGreatest.unique, Set.EqOn.image_eq, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun (z : ℂ) ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
h₃ :
  IsGreatest ((fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x - 1‖ 2) '' spectrum ℂ u)
    (HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1) u‖ 2)
⊢ HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)

Tactic:
exact h₃.unique (h_eqOn.image_eq ▸ h₂)

Premises used: IsGreatest.unique
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h : Nontrivial A
⊢ 0 ≤ ‖u - 1‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h : Nontrivial A
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h : Nontrivial A
rw : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 ↔ -1 ∉ spectrum ℂ u
⊢ ‖u - 1‖ < 2 ↔ -1 ∉ spectrum ℂ u

Tactic:
rw [← sq_lt_sq₀ (by positivity) (by positivity)]

Premises used: sq_lt_sq₀
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h : Nontrivial A
mp : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 → -1 ∉ spectrum ℂ u
mpr : -1 ∉ spectrum ℂ u → HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 ↔ -1 ∉ spectrum ℂ u

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h_1 : Nontrivial A
h : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
h1 : -1 ∈ spectrum ℂ u
⊢ 2 * (1 - re (-1)) < HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
have := two_mul_one_sub_le_norm_sub_one_sq hu h1 |>.trans_lt h
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h_1 : Nontrivial A
h : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
h1 : -1 ∈ spectrum ℂ u
this : 2 * (1 - re (-1)) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ False

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
hu : Membership.mem (γ := Submonoid A) (unitary A) u
h : Nontrivial A
mpr : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u
⊢ -1 ∉ spectrum ℂ u → HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
contrapose!