awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 2 * (1 - b) ≤ 2 * (1 - a)
have ha : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- 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
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))
have this : Antitone (β := ℝ) fun (y : ℝ) ↦ 2 * (1 - y)
Tactic: have : Antitone (fun y : ℝ ↦ 2 * (1 - y)) := by intro _ _ _; simp only; gcongr
-- 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
h_eqOn : Set.EqOn (β := ℝ) (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) ‖z - 1‖ 2) (fun (z : ℂ) ↦ 2 * (1 - z.re)) (spectrum ℂ u)
⊢ HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)
have h₂ : 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
-- 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
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)
have this : 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)
-- 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
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))
⊢ HPow.hPow (β := ℕ) ‖cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x - 1 x) u‖ 2 = 2 * (1 - x)
have h₃ : 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)
-- 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
⊢ ‖u - 1‖ < 2 ↔ -1 ∉ spectrum ℂ u
have a : Nontrivial A
Tactic: nontriviality 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
h : Nontrivial A
⊢ ‖u - 1‖ < 2 ↔ -1 ∉ spectrum ℂ u
have rw : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 ↔ -1 ∉ spectrum ℂ u
Tactic: rw [← sq_lt_sq₀ (by positivity) (by positivity)]
-- 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
h : Nontrivial A
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 ↔ -1 ∉ spectrum ℂ u
have mp : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 → -1 ∉ spectrum ℂ u
Tactic: constructor
-- 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
h : Nontrivial A
mp : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 → -1 ∉ spectrum ℂ u
⊢ HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2 ↔ -1 ∉ spectrum ℂ u
have mpr : -1 ∉ spectrum ℂ u → HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: constructor
-- 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
h_1 : Nontrivial A
h : HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
h1 : -1 ∈ spectrum ℂ u
⊢ False
have this : 2 * (1 - re (-1)) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: have := two_mul_one_sub_le_norm_sub_one_sq hu h1 |>.trans_lt h
-- 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
h : Nontrivial A
⊢ -1 ∉ spectrum ℂ u → HPow.hPow (β := ℕ) ‖u - 1‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
have mpr : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u
Tactic: contrapose!
-- 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
h : Nontrivial A
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u
have mpr : ∀ (x : ℝ) (hx : IsLeast (re '' spectrum ℂ u) x),
  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 _
-- 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
h : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) ‖u - 1‖ 2 → -1 ∈ spectrum ℂ u
have mpr : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u
Tactic: rw [norm_sub_one_sq_eq hu hx]
-- 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
h : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u
have mpr : ∀ (z : ℂ) (hz : z ∈ spectrum ℂ u) (hx : IsLeast (re '' spectrum ℂ u) z.re),
  HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - z.re) → -1 ∈ spectrum ℂ u
Tactic: obtain ⟨z, hz, rfl⟩ := hx.1
Cleared hypotheses: x, hx
-- 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
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
have linarith : -1 < z.re → HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2 * (1 - z.re) + 2 * (-1 - z.re) = 0
Tactic: linarith
-- 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
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
⊢ z.re ≤ -1
have linarith₁ : -1 < z.re → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
h : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 2 * (1 - z.re)
⊢ -1 ∈ spectrum ℂ u
have key₁ : z.re ≤ -1
Tactic: replace key : z.re ≤ -1 := by linarith
Cleared hypotheses: key
-- 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
h : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
⊢ -1 ∈ spectrum ℂ u
have hz_norm : ‖z‖ = 1
Tactic: have hz_norm : ‖z‖ = 1 := spectrum.norm_eq_one_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
h : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
have key₁ : z = -(↑1 : ℂ)
Tactic: rw [← hz_norm, ← RCLike.re_eq_complex_re, RCLike.re_le_neg_norm_iff_eq_neg_norm, hz_norm] at key
Cleared hypotheses: key, hz_norm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
⊢ HPow.hPow (β := ℕ) ‖(↑(expUnitary x) : A) - 1‖ 2 = 2 * (1 - Real.cos ‖x‖)
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
⊢ HPow.hPow (β := ℕ) ‖(↑(expUnitary x) : A) - 1‖ 2 = 2 * (1 - Real.cos ‖x‖)
have apply : IsLeast (re '' spectrum ℂ (↑(expUnitary x) : A)) (Real.cos ‖x‖)
Tactic: apply norm_sub_one_sq_eq (expUnitary x).2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
⊢ IsLeast (re '' spectrum ℂ (NormedSpace.exp (I • (↑x : A)))) (Real.cos ‖x‖)
have rw : IsLeast (re '' (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' (⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
⊢ IsLeast (re '' (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' (⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑x : A))
    (Real.cos ‖x‖)
have simp : IsLeast ((fun (a : ℝ) ↦ Real.cos 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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‖)
have refine_1 : Membership.mem (γ := Set ℝ) ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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‖)
⊢ IsLeast ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)
have refine_2 : Membership.mem (γ := Set ℝ) (lowerBounds ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A))) (Real.cos ‖x‖)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
h : Nontrivial A
⊢ Membership.mem (γ := Set ℝ) ((fun (a : ℝ) ↦ Real.cos a) '' spectrum ℝ (↑x : A)) (Real.cos ‖x‖)
have x₁ : ‖(↑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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ argSelfAdjoint (expUnitary x) = x
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ argSelfAdjoint (expUnitary x) = x
have a : (↑(argSelfAdjoint (expUnitary x)) : A) = (↑x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
have rw : 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ 2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π)
have hbc : Real.cos π < Real.cos ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
have exact : 2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π)
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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 π)
⊢ 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
have exact₁ : 2 * (1 - Real.cos π) = 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
⊢ (↑(argSelfAdjoint (expUnitary x)) : A) = (↑x : A)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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 : ℂ) ↦ (↑x.arg : ℂ)) (NormedSpace.exp (I • (↑x : A))) = (↑x : A)
have a : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) = (↑x : A)
Tactic: rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul .., ← cfc_comp' (hg := ?hg)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (NormedSpace.exp (I • (↑x : A))) = (↑x : A)
have rw : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) ((fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A))
Tactic: rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul .., ← cfc_comp' (hg := ?hg)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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))
have refine : (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
Tactic: refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
⊢ (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
have rwa : ∀ (this : spectrum ℂ (NormedSpace.exp (I • (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
have rwa₁ : ∀ (this : spectrum ℂ (cfc (R := ℂ) (p := IsStarNormal) NormedSpace.exp (I • (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
have 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
Tactic: rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul ..,
      cfc_map_spectrum ..] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ (fun (x : ℂ) ↦ NormedSpace.exp (I • x)) '' spectrum ℂ (↑x : A) ⊆ slitPlane
have rwa₃ : ∀ (this : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
h : Nontrivial A
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
| (↑x : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑x : A)
Tactic: rw [← cfc_id' ℂ (x : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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) = (↑x : A)
have a : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(NormedSpace.exp (I • x)).arg : ℂ)) (↑x : A) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑x : A)
Tactic: conv_rhs => rw [← cfc_id' ℂ (x : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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)
have a : ∀ (y : ℂ) (hy : y ∈ spectrum ℂ (↑x : A)), (↑(NormedSpace.exp (I • y)).arg : ℂ) = y
Tactic: refine cfc_congr fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
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)
⊢ (↑(NormedSpace.exp (I • y)).arg : ℂ) = y
have hy₁ : Membership.mem (γ := Set ℂ) ((⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) '' spectrum ℝ (↑x : A)) y
Tactic: rw [← x.2.spectrumRestricts.algebraMap_image] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ (↑(NormedSpace.exp (I • y)).arg : ℂ) = y
have a : ∀ (y : ℝ) (hy : y ∈ spectrum ℝ (↑x : A)),
  (↑(NormedSpace.exp (HSMul.hSMul (β := ℂ) I ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ))).arg : ℂ) =
    (algebraMap ℝ ℂ : (a : ℝ) → ℂ) y
Tactic: obtain ⟨y, hy, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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)
⊢ (↑(NormedSpace.exp (HSMul.hSMul (β := ℂ) I ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ))).arg : ℂ) =
    (algebraMap ℝ ℂ : (a : ℝ) → ℂ) y
have a : (cexp ((↑y : ℂ) * I)).arg = y
Tactic: simp only [coe_algebraMap, smul_eq_mul, mul_comm I, ← exp_eq_exp_ℂ, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
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)
⊢ (cexp ((↑y : ℂ) * I)).arg = y
have hy₁ : ‖y‖ < π
Tactic: replace hy : ‖y‖ < π := spectrum.norm_le_norm_of_mem hy |>.trans_lt hx
Cleared hypotheses: hy