awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖ < π
⊢ (cexp ((↑y : ℂ) * I)).arg = y
have hy₁ : -π < y ∧ y < π
Tactic: simp only [Real.norm_eq_abs, abs_lt] 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 : -π < y ∧ y < π
⊢ (cexp ((↑y : ℂ) * I)).arg = y
have a : arg (↑((Circle.exp : (a : ℝ) → Circle) y) : ℂ) = y
Tactic: rw [← Circle.coe_exp, Circle.arg_exp hy.1 hy.2.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
this : spectrum ℂ (↑(expUnitary x) : A) ⊆ slitPlane
y : ℝ
hy : -π < y ∧ y < π
a : arg (↑((Circle.exp : (a : ℝ) → Circle) y) : ℂ) = y
⊢ (cexp ((↑y : ℂ) * I)).arg = y
have a₁ : y = y
Tactic: rw [← Circle.coe_exp, Circle.arg_exp hy.1 hy.2.le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ expUnitary (argSelfAdjoint u) = u
have a : (↑(expUnitary (argSelfAdjoint u)) : A) = (↑u : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ (↑(expUnitary (argSelfAdjoint u)) : A) = (↑u : A)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
⊢ (↑(expUnitary (argSelfAdjoint u)) : A) = (↑u : A)
have a : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) = (↑u : A)
Tactic: rw [expUnitary_coe, argSelfAdjoint_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ),
    ← cfc_comp_smul .., ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
| (↑u : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑u : A)
Tactic: rw [← cfc_id' ℂ (u : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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) = (↑u : A)
have a : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ NormedSpace.exp (I • (↑x.arg : ℂ))) (↑u : A) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ x) (↑u : A)
Tactic: conv_rhs => rw [← cfc_id' ℂ (u : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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)
have a : ∀ (y : ℂ) (hy : y ∈ spectrum ℂ (↑u : 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
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ (↑u : A))
y : ℂ
hy : y ∈ spectrum ℂ (↑u : A)
⊢ NormedSpace.exp (I • (↑y.arg : ℂ)) = y
have hy₁ : ‖y‖ = 1
Tactic: have hy₁ : ‖y‖ = 1 := spectrum.norm_eq_one_of_unitary u.2 hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
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
⊢ NormedSpace.exp (I • (↑y.arg : ℂ)) = y
have this₁ : 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])
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
| HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
have rw : HPow.hPow (β := ℕ) ‖(↑(expUnitary (argSelfAdjoint u)) : A) - 1‖ 2
Tactic: rw [← expUnitary_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
have conv_rhs : 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = HPow.hPow (β := ℕ) ‖(↑(expUnitary (argSelfAdjoint u)) : A) - 1‖ 2
Tactic: conv_rhs => rw [← expUnitary_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ ‖argSelfAdjoint u‖ = Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2)
have refine : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
Tactic: refine Real.arccos_eq_of_eq_cos (by positivity) (norm_argSelfAdjoint_le_pi u) ?_ |>.symm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₁ : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → 2 / 2 = 1
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₂ : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₃ : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 < Real.cos ‖argSelfAdjoint u‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have 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
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₅ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₆ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₇ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have linarith₈ : Real.cos ‖argSelfAdjoint u‖ < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 = Real.cos ‖argSelfAdjoint u‖
have 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
Tactic: linarith [two_mul_one_sub_cos_norm_argSelfAdjoint hu]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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‖
have rw : ‖t • argSelfAdjoint u‖ ≤ 1 * ‖argSelfAdjoint u‖
Tactic: rw [← one_mul ‖argSelfAdjoint u‖]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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‖ ≤ 1 * ‖argSelfAdjoint u‖
have simp_rw : t * ‖(↑(argSelfAdjoint u) : A)‖ ≤ 1 * ‖(↑(argSelfAdjoint u) : A)‖
Tactic: simp_rw [AddSubgroupClass.coe_norm, val_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht.1]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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) : A)‖ ≤ 1 * ‖(↑(argSelfAdjoint u) : A)‖
have hbc : t ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
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
⊢ ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ ≤ ‖(↑u : A) - 1‖
have key : ‖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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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‖
⊢ ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ ≤ ‖(↑u : A) - 1‖
have rw : HPow.hPow (β := ℕ) ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ 2 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
Tactic: rw [← sq_le_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 : ↥(unitary A)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
hu : ‖(↑u : A) - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ HPow.hPow (β := ℕ) ‖(↑(expUnitary (t • argSelfAdjoint u)) : A) - 1‖ 2 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
have rw : 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
Tactic: rw [norm_sq_expUnitary_sub_one (key.trans <| norm_argSelfAdjoint_le_pi u)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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 ‖t • argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
have trans : 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)
Tactic: trans 2 * (1 - Real.cos ‖argSelfAdjoint u‖)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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‖)
⊢ 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
have trans₁ : 2 * (1 - Real.cos ‖argSelfAdjoint u‖) ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2
Tactic: trans 2 * (1 - Real.cos ‖argSelfAdjoint u‖)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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 ‖t • argSelfAdjoint u‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)
have hbc : Real.cos ‖argSelfAdjoint u‖ ≤ Real.cos ‖t • argSelfAdjoint u‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ ContinuousOn.{u_1, u_1} (X := ↥(unitary A)) argSelfAdjoint (ball 1 2)
have rw : ContinuousOn.{u_1, u_1} (X := ↥(unitary A))
  (Subtype.val (p := fun (x : A) ↦ x ∈ (↑(selfAdjoint A) : Set A)) ∘ argSelfAdjoint) (ball 1 2)
Tactic: rw [Topology.IsInducing.subtypeVal.continuousOn_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ ContinuousOn (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A))
    (ball 1 2)
have 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
Tactic: rw [isOpen_ball.continuousOn_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
⊢ 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
have dist : ∀ (hu : dist u 1 < 2),
  ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
Tactic: (hu : dist u 1 < 2)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
⊢ ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
have 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
Tactic: obtain ⟨ε, huε, hε2⟩ := exists_between (sq_lt_sq₀ (by positivity) (by positivity) |>.mpr hu)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
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
⊢ ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
have hε : 0 < ε
Tactic: have hε : 0 < ε := lt_of_le_of_lt (by positivity) huε
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
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 < ε
⊢ ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
have huε' : dist u 1 < √ε
Tactic: have huε' : dist u 1 < √ε := Real.lt_sqrt_of_sq_lt huε
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
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 < √ε
⊢ ContinuousAt (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A)) u
have apply : ContinuousOn (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A))
  (closedBall 1 √ε)
Tactic: apply ContinuousOn.continuousAt ?_ (closedBall_mem_nhds_of_mem huε')