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 : ↥(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 < √ε
⊢ ContinuousOn (Y := A) (fun (x : ↥(unitary A)) ↦ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (↑x : A))
    (closedBall 1 √ε)
have 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 √ε))
Tactic: apply ContinuousOn.image_comp_continuous ?_ continuous_subtype_val
-- 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 < √ε
⊢ 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 √ε))
have 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) ≤ ε}}
Tactic: apply continuousOn_cfc A (s := sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}) ?_ _ ?_ |>.mono
-- 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 < √ε
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) ≤ ε}}
⊢ 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 √ε))
have apply₁ : IsCompact (X := ℂ) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})
Tactic: apply continuousOn_cfc A (s := sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}) ?_ _ ?_ |>.mono
-- 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 < √ε
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) ≤ ε})
⊢ 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 √ε))
have apply₂ : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})
Tactic: apply continuousOn_cfc A (s := sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}) ?_ _ ?_ |>.mono
-- 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 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
⊢ Membership.mem (γ := Set A) {a : A | IsStarNormal a ∧ spectrum ℂ a ⊆ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}}
    (↑v : A)
have simp : IsStarNormal (↑v : A) ∧ spectrum ℂ (↑v : A) ⊆ sphere 0 1 ∧ spectrum ℂ (↑v : A) ⊆ {z : ℂ | 2 * (1 - z.re) ≤ ε}
Tactic: simp only [Set.subset_inter_iff, Set.mem_setOf_eq]
-- 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 < √ε
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) ≤ ε}
have refine : spectrum ℂ (↑v : A) ⊆ {z : ℂ | 2 * (1 - z.re) ≤ ε}
Tactic: refine ⟨inferInstance, spectrum_subset_circle v, ?_⟩
-- 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 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
z : ℂ
hz : z ∈ spectrum ℂ (↑v : A)
⊢ 2 * (1 - z.re) ≤ ε
have trans : 2 * (1 - z.re) ≤ HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2
Tactic: trans ‖(v - 1 : A)‖ ^ 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
ε : ℝ
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
⊢ 2 * (1 - z.re) ≤ ε
have trans₁ : HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2 ≤ ε
Tactic: trans ‖(v - 1 : A)‖ ^ 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
ε : ℝ
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)
⊢ HPow.hPow (β := ℕ) ‖(↑v : A) - 1‖ 2 ≤ ε
have refine : ‖(↑v : A) - 1‖ ≤ √ε
Tactic: refine Real.le_sqrt (by positivity) (by positivity) |>.mp ?_
-- 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 < √ε
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})
have refine : sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε} ⊆ 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
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 < √ε
⊢ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε} ⊆ slitPlane
have apply : -(↑1 : ℂ) ∉ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}
Tactic: apply subset_slitPlane_iff_of_subset_sphere Set.inter_subset_left |>.mpr
-- 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 < √ε
⊢ -(↑1 : ℂ) ∉ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}
have norm_num : ∀ (hε2 : ε < 4), ε < 4
Tactic: norm_num at hε2 ⊢
Cleared hypotheses: hε2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) u
⊢ Membership.mem (γ := Set ↥(selfAdjoint A)) (ball 0 π) (argSelfAdjoint u)
have simp : ∀ (hu : ‖(↑u : A) - 1‖ < 2), ‖argSelfAdjoint u‖ < π
Tactic: simp only [mem_ball, Subtype.dist_eq, OneMemClass.coe_one, dist_eq_norm, sub_zero] at hu ⊢
Cleared hypotheses: 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‖ < π
have rw : Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < π
Tactic: rw [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
⊢ 1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
have h : LT.lt (α := ℝ) 0 2
Tactic: gcongr
-- 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
h : LT.lt (α := ℝ) 0 2
⊢ 1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
have h₁ : 0 ≤ ‖(↑u : A) - 1‖
Tactic: gcongr
-- 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
h : LT.lt (α := ℝ) 0 2
h₁ : 0 ≤ ‖(↑u : A) - 1‖
⊢ 1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
have h₂ : Ne (α := ℕ) 2 0
Tactic: gcongr
-- 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
⊢ Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)
have apply : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
Tactic: apply Real.arccos_lt_arccos (by norm_num) (by gcongr)
-- 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 ≤ 1
have linarith : 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
Tactic: linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- 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 : 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
have linarith₁ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- 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 : 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
linarith₁ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
have linarith₂ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
Tactic: linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- 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 : 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
linarith₁ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
have linarith₃ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- 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 : 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
linarith₁ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
linarith₃ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
have linarith₄ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- 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 : 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2
linarith₁ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
linarith₃ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → 2 / 2 = 1
linarith₇ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
have linarith₉ : 1 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 →
  HMul.hMul (α := ℝ) 2 1 - (HMul.hMul (α := ℝ) 2 1 - 1 * HPow.hPow (β := ℕ) (1 * ‖(↑u : A) - 1‖) 2) +
      (HMul.hMul (α := ℝ) 2 0 - 1 * HPow.hPow (β := ℕ) (1 * ‖(↑u : A) - 1‖) 2) =
    0
Tactic: linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- 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
⊢ Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < π
have apply : Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)
Tactic: calc
      Real.arccos (1 - ‖(u - 1 : A)‖ ^ 2 / 2) < Real.arccos (1 - 2 ^ 2 / 2) := by
        apply Real.arccos_lt_arccos (by norm_num) (by gcongr)
        linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
      _ = π := by norm_num
-- 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
apply :
  Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)
⊢ Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < π
have apply₁ : Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2) = π
Tactic: calc
      Real.arccos (1 - ‖(u - 1 : A)‖ ^ 2 / 2) < Real.arccos (1 - 2 ^ 2 / 2) := by
        apply Real.arccos_lt_arccos (by norm_num) (by gcongr)
        linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 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 : Membership.mem (γ := Set ↥(selfAdjoint A)) (ball 0 π) x
⊢ Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) (expUnitary x)
have simp : ∀ (hx : ‖x‖ < π), ‖(↑(expUnitary x) : A) - 1‖ < 2
Tactic: simp only [mem_ball, Subtype.dist_eq, OneMemClass.coe_one, dist_eq_norm, sub_zero] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ ‖(↑(expUnitary x) : A) - 1‖ < 2
have rw : 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: rw [← sq_lt_sq₀ (by positivity) (by positivity), norm_sq_expUnitary_sub_one hx.le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
have this : -1 < Real.cos ‖(↑x : A)‖
Tactic: have : -1 < Real.cos ‖(x : A)‖ :=
      Real.cos_pi ▸ Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖(↑x : A)‖
⊢ 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
have simp : 2 - 2 * Real.cos ‖(↑x : A)‖ < HMul.hMul (α := ℝ) 2 2
Tactic: simp only [AddSubgroupClass.coe_norm, mul_sub, mul_one, sq, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖(↑x : A)‖
⊢ 2 - 2 * Real.cos ‖(↑x : A)‖ < HMul.hMul (α := ℝ) 2 2
have linarith : HMul.hMul (α := ℝ) 2 2 ≤ 2 - 2 * Real.cos ‖(↑x : A)‖ →
  2 * (-1 - Real.cos ‖(↑x : A)‖) + (HMul.hMul (α := ℝ) 2 2 - (2 - 2 * Real.cos ‖(↑x : A)‖)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖(↑x : A)‖
linarith :
  HMul.hMul (α := ℝ) 2 2 ≤ 2 - 2 * Real.cos ‖(↑x : A)‖ →
    2 * (-1 - Real.cos ‖(↑x : A)‖) + (HMul.hMul (α := ℝ) 2 2 - (2 - 2 * Real.cos ‖(↑x : A)‖)) = 0
⊢ 2 - 2 * Real.cos ‖(↑x : A)‖ < HMul.hMul (α := ℝ) 2 2
have linarith₁ : HMul.hMul (α := ℝ) 2 2 ≤ 2 - 2 * Real.cos ‖(↑x : A)‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖(↑v : A) - (↑u : A)‖ < 2
⊢ expUnitary (HSMul.hSMul (α := ℝ) (↑0 : ℝ) (argSelfAdjoint (v * star u))) * u = u
have a : (↑(expUnitary (HSMul.hSMul (α := ℝ) (↑0 : ℝ) (argSelfAdjoint (v * star u))) * u) : A) = (↑u : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
this : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
⊢ IsPathConnected (ball u δ)
have h : ball u δ = (fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ
Tactic: convert! this |>.image (f := (u * ·)) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
this : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
⊢ ball u δ = (fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ
have h : ∀ (v : ↥(unitary A)),
  v ∈ ball u δ ↔ Membership.mem (γ := Set ↥(unitary A)) ((fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
this : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
v : ↥(unitary A)
⊢ v ∈ ball u δ ↔ Membership.mem (γ := Set ↥(unitary A)) ((fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ) v
have h : v ∈ ball u δ ↔ Membership.mem (γ := Set ↥(unitary A)) ((fun (x : ↥(unitary A)) ↦ u * x) '' ball (u⁻¹ * u) δ) v
Tactic: rw [← inv_mul_cancel u]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
⊢ IsPathConnected (ball u δ)
have suffices : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
Tactic: suffices IsPathConnected (ball (1 : unitary A) δ) by
    convert! this |>.image (f := (u * ·)) (by fun_prop)
    ext v
    rw [← inv_mul_cancel u]
    simp [-inv_mul_cancel, Subtype.dist_eq, dist_eq_norm, ← mul_sub]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
⊢ IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
have refine : ∀ {u : ↥(unitary A)} (hu : Membership.mem (γ := Set ↥(unitary A)) (ball 1 δ) u), JoinedIn (ball 1 δ) 1 u
Tactic: refine ⟨1, by simpa, fun {u} hu ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
u_1 : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
u : ↥(unitary A)
hu : Membership.mem (γ := Set ↥(unitary A)) (ball 1 δ) u
⊢ JoinedIn (ball 1 δ) 1 u
have hu₁ : ‖(↑u : A) - 1‖ < δ
Tactic: have hu : ‖(u - 1 : A)‖ < δ := by simpa [Subtype.dist_eq, dist_eq_norm] using hu
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u_1 : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
u : ↥(unitary A)
hu_1 : Membership.mem (γ := Set ↥(unitary A)) (ball 1 δ) u
hu : ‖(↑u : A) - 1‖ < δ
⊢ JoinedIn (ball 1 δ) 1 u
have refine : ∀ (t : (↑unitInterval : Type)),
  Membership.mem (α := ↥(unitary A)) (γ := Set ↥(unitary A)) (ball 1 δ)
    ((path 1 u sorry : (a : (↑unitInterval : Type)) → ↥(unitary A)) t : ↥(unitary A))
Tactic: refine ⟨path 1 u (hu.trans hδ₂), fun t ↦ ?_⟩
-- 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)) (pathComponent 1) u ↔
    ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
have mp : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u →
  ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
mp :
  Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u →
    ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u ↔
    ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
have mpr : (∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u) →
  Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u
Tactic: constructor
-- 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)) (pathComponent 1) u →
    ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
have mp : ∀ {u : ↥(unitary A)},
  Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u →
    ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
Tactic: revert u
Cleared hypotheses: u
-- 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)) (pathComponent 1) u →
      ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u
have mp : Subset.{u_1} (α := Set ↥(unitary A)) (connectedComponent 1)
  (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
Tactic: simp_rw [← Set.mem_range, ← Set.subset_def, pathComponent_eq_connectedComponent]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ Subset.{u_1} (α := Set ↥(unitary A)) (connectedComponent 1)
    (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
have mp : IsClopen.{u_1} (X := ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
Tactic: refine IsClopen.connectedComponent_subset ?_ ⟨[], by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Connected (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ IsClopen.{u_1} (X := ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
have mp : Subset.{u_1} (α := Set ↥(unitary A))
  (thickening 2 (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod))
  (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
Tactic: refine .of_thickening_subset_self zero_lt_two ?_