awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (x : ℝ) (hx : IsLeast (re '' spectrum ℂ u) x),
    HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u

Tactic:
obtain ⟨x, hx⟩ := spectrum.isCompact (𝕜 := ℂ) u |>.image continuous_re |>.exists_isLeast <|
      (spectrum.nonempty _).image _

Premises used: IsCompact.exists_isLeast, Complex.continuous_re, spectrum.isCompact, spectrum.nonempty, Set.Nonempty.image, IsCompact.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
h : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
mpr : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u

Tactic:
rw [norm_sub_one_sq_eq hu hx]

Premises used: Unitary.norm_sub_one_sq_eq
-- 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
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
mpr :
  ∀ (z : ℂ) (hz : z ∈ spectrum ℂ u) (hx : IsLeast (re '' spectrum ℂ u) z.re),
    HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - z.re) → -1 ∈ spectrum ℂ u
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u

Tactic:
obtain ⟨z, hz, rfl⟩ := hx.1

Premises used: And.left, rfl
-- 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
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - z.re)
linarith : -1 < z.re → HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2 * (1 - z.re) + 2 * (-1 - z.re) = 0
linarith₁ : -1 < z.re → GT.gt (α := ℝ) 2 0
⊢ z.re ≤ -1

Tactic:
linarith
-- 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
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - z.re)
⊢ z.re ≤ -1

Tactic:
replace key : z.re ≤ -1 := by linarith
-- 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
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
⊢ ‖z‖ = 1

Tactic:
have hz_norm : ‖z‖ = 1 := spectrum.norm_eq_one_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
h : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
hz_norm : ‖z‖ = 1
⊢ z = -(↑1 : ℂ)

Tactic:
rw [← hz_norm, ← RCLike.re_eq_complex_re, RCLike.re_le_neg_norm_iff_eq_neg_norm, hz_norm] at key

Premises used: RCLike.re_eq_complex_re, RCLike.re_le_neg_norm_iff_eq_neg_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
h : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
hz_norm : ‖z‖ = 1
key₁ : z = -(↑1 : ℂ)
⊢ ‖z‖ = 1

Tactic:
rw [← hz_norm, ← RCLike.re_eq_complex_re, RCLike.re_le_neg_norm_iff_eq_neg_norm, hz_norm] at key

Premises used: RCLike.re_eq_complex_re, RCLike.re_le_neg_norm_iff_eq_neg_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
h : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z = -(↑1 : ℂ)
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
key ▸ hz

Premises used: Set.Mem, Eq.rec
-- 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
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z = -(↑1 : ℂ)
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
exact key ▸ 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
⊢ spectrum ℂ u ⊆ slitPlane ↔ ‖u - 1‖ < 2

Tactic:
simp [subset_slitPlane_iff_of_subset_sphere (spectrum.subset_circle_of_unitary hu),
    norm_sub_one_lt_two_iff hu]

Premises used: Complex.subset_slitPlane_iff_of_subset_sphere, Unitary.norm_sub_one_lt_two_iff, spectrum.subset_circle_of_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : A
⊢ IsSelfAdjoint (cfc (p := IsStarNormal) (ofReal ∘ arg) u)

Tactic:
simp [isSelfAdjoint_iff, ← cfc_star, Function.comp_def]

Premises used: Function.comp_def, isSelfAdjoint_iff, cfc_star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
apply : IsLeast (re '' spectrum ℂ (↑(expUnitary x) : A)) (Real.cos ‖x‖)
⊢ HPow.hPow (β := ℕ) ‖(↑(expUnitary x) : A) - 1‖ 2 = 2 * (1 - Real.cos ‖x‖)

Tactic:
apply norm_sub_one_sq_eq (expUnitary x).2

Premises used: selfAdjoint.expUnitary, Unitary.norm_sub_one_sq_eq, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
rw :
  IsLeast (re '' (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' (⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑x : A))
    (Real.cos ‖x‖)
⊢ IsLeast (re '' spectrum ℂ (NormedSpace.exp (I • (↑x : A)))) (Real.cos ‖x‖)

Tactic:
rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul I _ (x : A), cfc_map_spectrum ..,
    ← x.2.spectrumRestricts.algebraMap_image]

Premises used: cfc_comp_smul, cfc_map_spectrum, SpectrumRestricts.algebraMap_image, CFC.exp_eq_normedSpace_exp, IsSelfAdjoint.spectrumRestricts, Subtype.val, Subtype.property, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
simp : IsLeast ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)
⊢ IsLeast (re '' (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' (⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑x : A))
    (Real.cos ‖x‖)

Tactic:
simp only [Set.image_image, coe_algebraMap, smul_eq_mul, mul_comm I, ← exp_eq_exp_ℂ,
    exp_ofReal_mul_I_re]

Premises used: Set.image_image, Complex.exp_eq_exp_ℂ, Complex.exp_ofReal_mul_I_re, Complex.coe_algebraMap, mul_comm, smul_eq_mul, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
⊢ IsLeast ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)

Tactic:
⟨?_, ?_⟩

Premises used: IsLeast, And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
refine_1 : Membership.mem (γ := Set ℝ) ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)
refine_2 : Membership.mem (γ := Set ℝ) (lowerBounds ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A))) (Real.cos ‖x‖)
⊢ IsLeast ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h_1 : Nontrivial A
h : ‖(↑x : A)‖ ∈ spectrum ℝ (↑x : A)
⊢ Membership.mem (γ := Set ℝ) ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)

Tactic:
⟨_, h, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h_1 : Nontrivial A
h : ‖(↑x : A)‖ ∈ spectrum ℝ (↑x : A)
⊢ Membership.mem (γ := Set ℝ) ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)

Tactic:
exact ⟨_, h, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h_1 : Nontrivial A
h : -‖(↑x : A)‖ ∈ spectrum ℝ (↑x : A)
⊢ (fun (a : ℝ) ↦ Real.cos a) (-‖(↑x : A)‖) = Real.cos ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h_1 : Nontrivial A
h : -‖(↑x : A)‖ ∈ spectrum ℝ (↑x : A)
⊢ Membership.mem (γ := Set ℝ) ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)

Tactic:
exact ⟨_, h, by simp⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
⊢ ‖(↑x : A)‖ ∈ spectrum ℝ (↑x : A) ∨ -‖(↑x : A)‖ ∈ spectrum ℝ (↑x : A)

Tactic:
cases CStarAlgebra.norm_or_neg_norm_mem_spectrum x.2 with
    | inl h => exact ⟨_, h, rfl⟩
    | inr h => exact ⟨_, h, by simp⟩

Premises used: CStarAlgebra.norm_or_neg_norm_mem_spectrum, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
y : ℝ
hy : y ∈ spectrum ℝ (↑x : A)
⊢ 0 ≤ |y|

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
y : ℝ
hy : y ∈ spectrum ℝ (↑x : A)
⊢ Real.cos ‖x‖ ≤ (fun (a : ℝ) ↦ Real.cos a) y

Tactic:
exact Real.cos_abs y ▸ Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) hx <|
      spectrum.norm_le_norm_of_mem hy

Premises used: spectrum.norm_le_norm_of_mem
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
a : (↑(argSelfAdjoint (expUnitary x)) : A) = (↑x : A)
⊢ argSelfAdjoint (expUnitary x) = x

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ 0 ≤ ‖(↑(expUnitary x) : A) - 1‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
rw : 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane

Tactic:
rw [spectrum_subset_slitPlane_iff_norm_lt_two (expUnitary x).2,
      ← sq_lt_sq₀ (by positivity) (by positivity), norm_sq_expUnitary_sub_one hx.le]

Premises used: selfAdjoint.norm_sq_expUnitary_sub_one, sq_lt_sq₀, selfAdjoint.expUnitary, LT.lt.le, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
hbc : Real.cos π < Real.cos ‖x‖
⊢ 2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ Real.cos π < Real.cos ‖x‖

Tactic:
exact Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx

Premises used: le_rfl, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ 2 * (1 - Real.cos π) = HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
exact : 2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π)
exact₁ : 2 * (1 - Real.cos π) = HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
calc
      2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π) := by
        gcongr
        exact Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx
      _ = 2 ^ 2 := by norm_num

Premises used: Norm.norm, Real.pi, Real.cos, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane

Tactic:
have : spectrum ℂ (expUnitary x : A) ⊆ slitPlane := by
    rw [spectrum_subset_slitPlane_iff_norm_lt_two (expUnitary x).2,
      ← sq_lt_sq₀ (by positivity) (by positivity), norm_sq_expUnitary_sub_one hx.le]
    calc
      2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π) := by
        gcongr
        exact Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx
      _ = 2 ^ 2 := by norm_num
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
a : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) = (↑x : A)
rw : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) ((fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A))
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (NormedSpace.exp (I • (↑x : A))) = (↑x : A)

Tactic:
rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul .., ← cfc_comp' (hg := ?hg)]

Premises used: cfc_comp_smul, CFC.exp_eq_normedSpace_exp, cfc_comp'
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) ((fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A))

Tactic:
continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_

Premises used: Complex.continuousOn_arg, Continuous.comp_continuousOn, Complex.continuous_ofReal, ContinuousOn.mono
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
refine : (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) ((fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A))

Tactic:
refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_

Premises used: Complex.continuousOn_arg, Continuous.comp_continuousOn, Complex.continuous_ofReal, ContinuousOn.mono
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
rwa :
  ∀ (this : spectrum ℂ (NormedSpace.exp (I • (↑x : A))) ⊆ slitPlane),
    (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
rwa₁ :
  ∀ (this : spectrum ℂ (cfc (R := ℂ) (p := IsStarNormal) NormedSpace.exp (I • (↑x : A))) ⊆ slitPlane),
    (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
rwa₂ :
  ∀ (this : spectrum ℂ (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) (↑x : A)) ⊆ slitPlane),
    (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane),
    (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
⊢ (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane

Tactic:
rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul ..,
      cfc_map_spectrum ..] at this

Premises used: cfc_comp_smul, cfc_map_spectrum, CFC.exp_eq_normedSpace_exp, selfAdjoint.expUnitary_coe
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) ((fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A))

Tactic:
case hg =>
    refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_
    rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul ..,
      cfc_map_spectrum ..] at this

Premises used: Complex.continuousOn_arg, cfc_comp_smul, Continuous.comp_continuousOn, cfc_map_spectrum, CFC.exp_eq_normedSpace_exp, Complex.continuous_ofReal, ContinuousOn.mono, selfAdjoint.expUnitary_coe
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑x : A)
| (↑x : A)

Tactic:
rw [← cfc_id' ℂ (x : A)]

Premises used: cfc_id', Complex, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
a :
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑x : A)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) = (↑x : A)

Tactic:
conv_rhs => rw [← cfc_id' ℂ (x : A)]

Premises used: cfc_id', Complex, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑x : 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
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
a : ∀ (y : ℂ) (hy : y ∈ spectrum ℂ (↑x : A)), (↑(NormedSpace.exp (I • y)).arg : ℂ) = y
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑x : 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
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℂ
hy : y ∈ spectrum ℂ (↑x : A)
⊢ Membership.mem (γ := Set ℂ) ((⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑x : A)) y

Tactic:
rw [← x.2.spectrumRestricts.algebraMap_image] at hy

Premises used: SpectrumRestricts.algebraMap_image, IsSelfAdjoint.spectrumRestricts, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℂ
hy : Membership.mem (γ := Set ℂ) ((⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑x : A)) y
a :
  ∀ (y : ℝ) (hy : y ∈ spectrum ℝ (↑x : A)),
    (↑(NormedSpace.exp (HSMul.hSMul (β := ℂ) I ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ))).arg : ℂ) =
      (algebraMap ℝ ℂ : (a : ℝ) → ℂ) y
⊢ (↑(NormedSpace.exp (I • y)).arg : ℂ) = y

Tactic:
obtain ⟨y, hy, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℝ
hy : y ∈ spectrum ℝ (↑x : A)
a : (cexp ((↑y : ℂ) * I)).arg = y
⊢ (↑(NormedSpace.exp (HSMul.hSMul (β := ℂ) I ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ))).arg : ℂ) =
    (algebraMap ℝ ℂ : (a : ℝ) → ℂ) y

Tactic:
simp only [coe_algebraMap, smul_eq_mul, mul_comm I, ← exp_eq_exp_ℂ, ofReal_inj]

Premises used: Complex.exp_eq_exp_ℂ, Complex.coe_algebraMap, mul_comm, Complex.ofReal_inj, smul_eq_mul, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℝ
hy : y ∈ spectrum ℝ (↑x : A)
⊢ ‖y‖ < π

Tactic:
replace hy : ‖y‖ < π := spectrum.norm_le_norm_of_mem hy |>.trans_lt hx
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℝ
hy : ‖y‖ < π
⊢ -π < y ∧ y < π

Tactic:
simp only [Real.norm_eq_abs, abs_lt] at hy

Premises used: abs_lt, Real.norm_eq_abs
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℝ
hy : -π < y ∧ y < π
a : arg (↑((Circle.exp : (a : ℝ) → Circle) y) : ℂ) = y
a₁ a₂ : y = y
⊢ (cexp ((↑y : ℂ) * I)).arg = y

Tactic:
rw [← Circle.coe_exp, Circle.arg_exp hy.1 hy.2.le]

Premises used: LT.lt.le, And.right, And.left, Circle.arg_exp, Circle.coe_exp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
a : (↑(expUnitary (argSelfAdjoint u)) : A) = (↑u : A)
⊢ expUnitary (argSelfAdjoint u) = u

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ ContinuousOn arg (spectrum ℂ (↑u : A))

Tactic:
have : ContinuousOn arg (spectrum ℂ (u : A)) :=
    continuousOn_arg.mono <| (spectrum_subset_slitPlane_iff_norm_lt_two u.2).mpr hu
-- 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 : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) = (↑u : A)
⊢ (↑(expUnitary (argSelfAdjoint u)) : A) = (↑u : A)

Tactic:
rw [expUnitary_coe, argSelfAdjoint_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ),
    ← cfc_comp_smul .., ← cfc_comp' ..]

Premises used: cfc_comp_smul, CFC.exp_eq_normedSpace_exp, cfc_comp', Unitary.argSelfAdjoint_coe, selfAdjoint.expUnitary_coe
-- 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))
rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑u : A)
| (↑u : A)

Tactic:
rw [← cfc_id' ℂ (u : A)]

Premises used: cfc_id', Complex, Subtype.val
-- 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 :
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑u : A)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) = (↑u : A)

Tactic:
conv_rhs => rw [← cfc_id' ℂ (u : A)]

Premises used: cfc_id', Complex, Subtype.val