awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑u : A)

Tactic:
cfc_congr fun y hy ↦ ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
a : ∀ (y : ℂ) (hy : y ∈ spectrum ℂ (↑u : A)), NormedSpace.exp (I • (↑y.arg : ℂ)) = y
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑u : A)

Tactic:
refine cfc_congr fun y hy ↦ ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
⊢ ‖y‖ = 1

Tactic:
have hy₁ : ‖y‖ = 1 := spectrum.norm_eq_one_of_unitary u.2 hy
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
hy₁ : ‖y‖ = 1
⊢ (I * (↑y.arg : ℂ)).re = (log y).re

Tactic:
simp [log_re, spectrum.norm_eq_one_of_unitary u.2 hy]

Premises used: Complex.log_re, spectrum.norm_eq_one_of_unitary, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
hy₁ : ‖y‖ = 1
⊢ (I * (↑y.arg : ℂ)).im = (log y).im

Tactic:
simp [log_im]

Premises used: Complex.log_im
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
hy₁ : ‖y‖ = 1
⊢ I * (↑y.arg : ℂ) = log y

Tactic:
have : I * y.arg = log y :=
    Complex.ext (by simp [log_re, spectrum.norm_eq_one_of_unitary u.2 hy]) (by simp [log_im])
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this_1 : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
hy₁ : ‖y‖ = 1
this : I * (↑y.arg : ℂ) = log y
⊢ y ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this_1 : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
hy₁ : ‖y‖ = 1
this : I * (↑y.arg : ℂ) = log y
⊢ NormedSpace.exp (I • (↑y.arg : ℂ)) = y

Tactic:
simpa [← exp_eq_exp_ℂ, this] using exp_log (by aesop)

Premises used: Complex.exp_eq_exp_ℂ, Complex.exp_log
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
⊢ 0 ≤ π

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
⊢ ‖(↑y.arg : ℂ)‖ ≤ π

Tactic:
simpa using abs_arg_le_pi y

Premises used: Complex.abs_arg_le_pi
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
rw : HPow.hPow (β := ℕ) ‖(↑(expUnitary (argSelfAdjoint u)) : A) - 1‖ 2
| HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2

Tactic:
rw [← expUnitary_argSelfAdjoint hu]

Premises used: expUnitary_argSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
conv_rhs : 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = HPow.hPow (β := ℕ) ‖(↑(expUnitary (argSelfAdjoint u)) : A) - 1‖ 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2

Tactic:
conv_rhs => rw [← expUnitary_argSelfAdjoint hu]

Premises used: expUnitary_argSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = HPow.hPow (β := ℕ) ‖(↑(expUnitary (argSelfAdjoint u)) : A) - 1‖ 2

Tactic:
Eq.symm <| norm_sq_expUnitary_sub_one <| norm_argSelfAdjoint_le_pi u

Premises used: selfAdjoint.norm_sq_expUnitary_sub_one, Unitary.norm_argSelfAdjoint_le_pi, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = HPow.hPow (β := ℕ) ‖(↑(expUnitary (argSelfAdjoint u)) : A) - 1‖ 2

Tactic:
exact Eq.symm <| norm_sq_expUnitary_sub_one <| norm_argSelfAdjoint_le_pi u

Premises used: selfAdjoint.norm_sq_expUnitary_sub_one, Unitary.norm_argSelfAdjoint_le_pi, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ 0 ≤ ‖argSelfAdjoint u‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
refine : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
⊢ ‖argSelfAdjoint u‖ = Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2)

Tactic:
refine Real.arccos_eq_of_eq_cos (by positivity) (norm_argSelfAdjoint_le_pi u) ?_ |>.symm

Premises used: Real.arccos_eq_of_eq_cos, Unitary.norm_argSelfAdjoint_le_pi, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
linarith :
  1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁ : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → 2 / 2 = 1
linarith₂ : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → GT.gt (α := ℝ) 2 0
linarith₄ :
  1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ →
    HMul.hMul (α := ℝ) 2 1 - 1 * HPow.hPow (β := ℕ) (1 * ‖(↑u : A) - 1‖) 2 - 2 * Real.cos ‖argSelfAdjoint u‖ +
        -(2 * (1 - Real.cos ‖argSelfAdjoint u‖) - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2) =
      0
linarith₅ :
  Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
linarith₇ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 →
    2 * Real.cos ‖argSelfAdjoint u‖ - (HMul.hMul (α := ℝ) 2 1 - 1 * HPow.hPow (β := ℕ) (1 * ‖(↑u : A) - 1‖) 2) +
        (2 * (1 - Real.cos ‖argSelfAdjoint u‖) - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2) =
      0
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖

Tactic:
linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]

Premises used: Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
rw : ‖t • argSelfAdjoint u‖ ≤ 1 * ‖argSelfAdjoint u‖
⊢ ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖

Tactic:
rw [← one_mul ‖argSelfAdjoint u‖]

Premises used: Norm.norm, Unitary.argSelfAdjoint, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
simp_rw : t * ‖(↑(argSelfAdjoint u) : A)‖ ≤ 1 * ‖(↑(argSelfAdjoint u) : A)‖
⊢ ‖t • argSelfAdjoint u‖ ≤ 1 * ‖argSelfAdjoint u‖

Tactic:
simp_rw [AddSubgroupClass.coe_norm, val_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht.1]

Premises used: norm_smul, selfAdjoint.val_smul, And.left, abs_of_nonneg, AddSubgroupClass.coe_norm, Real.norm_eq_abs
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
hbc : t ≤ 1
⊢ t * ‖(↑(argSelfAdjoint u) : A)‖ ≤ 1 * ‖(↑(argSelfAdjoint u) : A)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
⊢ t ≤ 1

Tactic:
ht.2

Premises used: And.right
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
⊢ t ≤ 1

Tactic:
exact ht.2

Premises used: And.right
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
⊢ ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖

Tactic:
have key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖ := by
    rw [← one_mul ‖argSelfAdjoint u‖]
    simp_rw [AddSubgroupClass.coe_norm, val_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht.1]
    gcongr
    exact ht.2
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 0 ≤ ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 0 ≤ ‖(↑u : A) - 1‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
rw : HPow.hPow (β := ℕ) ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ 2 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
⊢ ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ ≤ ‖(↑u : A) - 1‖

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

Premises used: sq_le_sq₀
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
rw : 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
⊢ HPow.hPow (β := ℕ) ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ 2 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2

Tactic:
rw [norm_sq_expUnitary_sub_one (key.trans <| norm_argSelfAdjoint_le_pi u)]

Premises used: selfAdjoint.norm_sq_expUnitary_sub_one, LE.le.trans, Unitary.norm_argSelfAdjoint_le_pi
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
trans : 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)
trans₁ : 2 * (1 - Real.cos ‖argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
⊢ 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2

Tactic:
trans 2 * (1 - Real.cos ‖argSelfAdjoint u‖)

Premises used: Norm.norm, Real.cos, Unitary.argSelfAdjoint, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
hbc : Real.cos ‖argSelfAdjoint u‖ ≤ Real.cos ‖t • argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 0 ≤ ‖t • argSelfAdjoint u‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ Real.cos ‖argSelfAdjoint u‖ ≤ Real.cos ‖t • argSelfAdjoint u‖

Tactic:
exact Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) (norm_argSelfAdjoint_le_pi u) key

Premises used: Unitary.norm_argSelfAdjoint_le_pi, Real.cos_le_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2

Tactic:
(two_mul_one_sub_cos_norm_argSelfAdjoint hu).le

Premises used: Eq.le, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2

Tactic:
exact (two_mul_one_sub_cos_norm_argSelfAdjoint hu).le

Premises used: Eq.le, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
rw :
  ContinuousOn.{u_1, u_1} (X := ↥(unitary A))
    (Subtype.val (p := fun (x : A) ↦ x ∈ (↑(selfAdjoint A) : Set A)) ∘ argSelfAdjoint) (ball 1 2)
⊢ ContinuousOn.{u_1, u_1} (X := ↥(unitary A)) argSelfAdjoint (ball 1 2)

Tactic:
rw [Topology.IsInducing.subtypeVal.continuousOn_iff]

Premises used: Topology.IsInducing.continuousOn_iff, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
rw :
  ∀ ⦃a : ↥(unitary A)⦄,
    Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) a →
      ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) a
⊢ ContinuousOn (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A))
    (ball 1 2)

Tactic:
rw [isOpen_ball.continuousOn_iff]

Premises used: IsOpen.continuousOn_iff, Metric.isOpen_ball
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
dist :
  ∀ (hu : Dist.dist u 1 < 2),
    ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
⊢ Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) u →
    ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u

Tactic:
(hu : dist u 1 < 2)
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
⊢ 0 ≤ dist u 1

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
obtain :
  ∀ (ε : ℝ) (huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε) (hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2),
    ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
⊢ ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u

Tactic:
obtain ⟨ε, huε, hε2⟩ := exists_between (sq_lt_sq₀ (by positivity) (by positivity) |>.mpr hu)

Premises used: Iff.mpr, sq_lt_sq₀, exists_between
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ 0 ≤ HPow.hPow (β := ℕ) (dist u 1) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ 0 < ε

Tactic:
have hε : 0 < ε := lt_of_le_of_lt (by positivity) huε
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
⊢ dist u 1 < √ε

Tactic:
have huε' : dist u 1 < √ε := Real.lt_sqrt_of_sq_lt huε
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
apply :
  ContinuousOn (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A))
    (closedBall 1 √ε)
⊢ ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u

Tactic:
apply ContinuousOn.continuousAt ?_ (closedBall_mem_nhds_of_mem huε')

Premises used: Metric.closedBall_mem_nhds_of_mem, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
apply :
  ContinuousOn (cfc (p := IsStarNormal) fun (x : ℂ) ↦ (↑x.arg : ℂ))
    (Set.image (α := ↥(unitary A)) (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x))
      (closedBall 1 √ε))
⊢ ContinuousOn (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A))
    (closedBall 1 √ε)

Tactic:
apply ContinuousOn.image_comp_continuous ?_ continuous_subtype_val

Premises used: ContinuousOn.image_comp_continuous, continuous_subtype_val
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
apply :
  Subset.{u_1} (α := Set A)
    (Set.image (α := ↥(unitary A)) (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x))
      (closedBall 1 √ε))
    {a : A | IsStarNormal a ∧ spectrum ℂ a ⊆ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}}
apply₁ : IsCompact (X := ℂ) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})
apply₂ : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})
⊢ ContinuousOn (cfc (p := IsStarNormal) fun (x : ℂ) ↦ (↑x.arg : ℂ))
    (Set.image (α := ↥(unitary A)) (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x))
      (closedBall 1 √ε))

Tactic:
apply continuousOn_cfc A (s := sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}) ?_ _ ?_ |>.mono

Premises used: ContinuousOn.mono, continuousOn_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
simp : IsStarNormal (↑v : A) ∧ spectrum ℂ (↑v : A) ⊆ sphere 0 1 ∧ spectrum ℂ (↑v : A) ⊆ {z : ℂ | 2 * (1 - z.re) ≤ ε}
⊢ Membership.mem (γ := Set A) {a : A | IsStarNormal a ∧ spectrum ℂ a ⊆ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}}
    (↑v : A)

Tactic:
simp only [Set.subset_inter_iff, Set.mem_setOf_eq]

Premises used: Set.subset_inter_iff, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
⊢ IsStarNormal (↑v : A) ∧ spectrum ℂ (↑v : A) ⊆ sphere 0 1 ∧ spectrum ℂ (↑v : A) ⊆ {z : ℂ | 2 * (1 - z.re) ≤ ε}

Tactic:
⟨inferInstance, spectrum_subset_circle v, ?_⟩

Premises used: inferInstance, And.intro, Unitary.spectrum_subset_circle
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
refine : spectrum ℂ (↑v : A) ⊆ {z : ℂ | 2 * (1 - z.re) ≤ ε}
⊢ IsStarNormal (↑v : A) ∧ spectrum ℂ (↑v : A) ⊆ sphere 0 1 ∧ spectrum ℂ (↑v : A) ⊆ {z : ℂ | 2 * (1 - z.re) ≤ ε}

Tactic:
refine ⟨inferInstance, spectrum_subset_circle v, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
z : ℂ
hz : z ∈ spectrum ℂ (↑v : A)
trans : 2 * (1 - z.re) ≤ HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2
trans₁ : HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2 ≤ ε
⊢ 2 * (1 - z.re) ≤ ε

Tactic:
trans ‖(v - 1 : A)‖ ^ 2

Premises used: HSub.hSub, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
z : ℂ
hz : z ∈ spectrum ℂ (↑v : A)
⊢ 2 * (1 - z.re) ≤ HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2

Tactic:
two_mul_one_sub_le_norm_sub_one_sq v.2 hz

Premises used: Unitary.two_mul_one_sub_le_norm_sub_one_sq, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
z : ℂ
hz : z ∈ spectrum ℂ (↑v : A)
⊢ 2 * (1 - z.re) ≤ HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2

Tactic:
exact two_mul_one_sub_le_norm_sub_one_sq v.2 hz

Premises used: Unitary.two_mul_one_sub_le_norm_sub_one_sq, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
z : ℂ
hz : z ∈ spectrum ℂ (↑v : A)
⊢ 0 ≤ ‖(↑v : A) - 1‖

Tactic:
positivity