awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : Membership.mem (γ := Set ↥(unitary A)) (closedBall 1 √ε) v
z : ℂ
hz : z ∈ spectrum ℂ (↑v : A)
⊢ 0 ≤ ε

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

Tactic:
refine Real.le_sqrt (by positivity) (by positivity) |>.mp ?_

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

Tactic:
simpa [Subtype.dist_eq, dist_eq_norm] using hv

Premises used: dist_eq_norm, Subtype.dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ Continuous (Y := ℝ) fun (z : ℂ) ↦ 2 * (1 - z.re)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ Continuous (Y := ℝ) fun (z : ℂ) ↦ ε

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ IsCompact (X := ℂ) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})

Tactic:
exact isCompact_sphere 0 1 |>.inter_right <| isClosed_le (by fun_prop) (by fun_prop)

Premises used: isClosed_le, isCompact_sphere, IsCompact.inter_right, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})

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
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 < √ε
refine : sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε} ⊆ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ)) (sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε})

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
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 : -(↑1 : ℂ) ∉ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}
⊢ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε} ⊆ slitPlane

Tactic:
apply subset_slitPlane_iff_of_subset_sphere Set.inter_subset_left |>.mpr

Premises used: Iff.mpr, Complex.subset_slitPlane_iff_of_subset_sphere, Set.inter_subset_left
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : HPow.hPow (β := ℕ) (dist u 1) 2 < ε
hε2 : ε < HPow.hPow (α := ℝ) (β := ℕ) 2 2
hε : 0 < ε
huε' : dist u 1 < √ε
norm_num : ∀ (hε2 : ε < 4), ε < 4
⊢ -(↑1 : ℂ) ∉ sphere 0 1 ∩ {z : ℂ | 2 * (1 - z.re) ≤ ε}

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

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

Tactic:
exact hε2
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) u
simp : ∀ (hu : ‖(↑u : A) - 1‖ < 2), ‖argSelfAdjoint u‖ < π
⊢ Membership.mem (γ := Set ↥(selfAdjoint A)) (ball 0 π) (argSelfAdjoint u)

Tactic:
simp only [mem_ball, Subtype.dist_eq, OneMemClass.coe_one, dist_eq_norm, sub_zero] at hu ⊢

Premises used: dist_eq_norm, sub_zero, OneMemClass.coe_one, Subtype.dist_eq, Metric.mem_ball
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
rw : Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < π
⊢ ‖argSelfAdjoint u‖ < π

Tactic:
rw [norm_argSelfAdjoint hu]

Premises used: Unitary.norm_argSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ -1 ≤ 1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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‖
h₂ : Ne (α := ℕ) 2 0
⊢ 1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2 < 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
apply : 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1
⊢ Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2) < Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)

Tactic:
apply Real.arccos_lt_arccos (by norm_num) (by gcongr)

Premises used: Real.arccos_lt_arccos
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
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
⊢ 1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 2 / 2 ≤ 1

Tactic:
linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : ‖(↑u : A) - 1‖ < 2
⊢ Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2) = π

Tactic:
norm_num
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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)
apply₁ : Real.arccos (1 - HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2) = π
⊢ Real.arccos (1 - HPow.hPow (β := ℕ) ‖(↑u : A) - 1‖ 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

Premises used: Norm.norm, HSub.hSub, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Subtype.val, Real.arccos
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : Membership.mem (γ := Set ↥(selfAdjoint A)) (ball 0 π) x
simp : ∀ (hx : ‖x‖ < π), ‖(↑(expUnitary x) : A) - 1‖ < 2
⊢ Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) (expUnitary x)

Tactic:
simp only [mem_ball, Subtype.dist_eq, OneMemClass.coe_one, dist_eq_norm, sub_zero] at hx ⊢

Premises used: dist_eq_norm, sub_zero, OneMemClass.coe_one, Subtype.dist_eq, Metric.mem_ball
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ 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‖ < π
⊢ 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‖ < π
rw : 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ ‖(↑(expUnitary x) : A) - 1‖ < 2

Tactic:
rw [← 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₀, LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ 0 ≤ ‖(↑x : A)‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ -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
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖(↑x : A)‖
simp : 2 - 2 * Real.cos ‖(↑x : A)‖ < HMul.hMul (α := ℝ) 2 2
⊢ 2 * (1 - Real.cos ‖x‖) < HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
simp only [AddSubgroupClass.coe_norm, mul_sub, mul_one, sq, gt_iff_lt]

Premises used: mul_sub, sq, gt_iff_lt, AddSubgroupClass.coe_norm, mul_one
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
linarith₁ : HMul.hMul (α := ℝ) 2 2 ≤ 2 - 2 * Real.cos ‖(↑x : A)‖ → GT.gt (α := ℝ) 2 0
⊢ 2 - 2 * Real.cos ‖(↑x : A)‖ < HMul.hMul (α := ℝ) 2 2

Tactic:
linarith
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu : Membership.mem (γ := Set ↥(unitary A)) (ball 1 2) u
⊢ ‖(↑u : A) - 1‖ < 2

Tactic:
simpa [Subtype.dist_eq, dist_eq_norm] using hu

Premises used: dist_eq_norm, Subtype.dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : Membership.mem (γ := Set ↥(selfAdjoint A)) (ball 0 π) x
⊢ ‖x‖ < π

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ ContinuousOn.{u_1, u_1} (X := ↥(unitary A)) argSelfAdjoint (ball 1 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ ContinuousOn.{u_1, u_1} (X := ↥(selfAdjoint A)) expUnitary (ball 0 π)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
⊢ ‖(↑u : A) - (↑v : A)‖ = ‖((↑u : A) * (↑(star v) : A) - 1) * (↑v : A)‖

Tactic:
simp [sub_mul, mul_assoc]

Premises used: mul_assoc, sub_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
⊢ ‖((↑u : A) * (↑(star v) : A) - 1) * (↑v : A)‖ = ‖(↑(u * star v) : A) - 1‖

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖(↑u : A) - (↑v : A)‖ < 2
⊢ expUnitary (argSelfAdjoint (u * star v)) = u * star v

Tactic:
expUnitary_argSelfAdjoint <| norm_sub_eq u v ▸ huv

Premises used: Eq.rec, expUnitary_argSelfAdjoint, Unitary.norm_sub_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
⊢ Continuous.{0, u_1} (Y := ↥(unitary A)) fun (t : (↑unitInterval : Type)) ↦ expUnitary ((↑t : ℝ) • x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
⊢ expUnitary (HSMul.hSMul (α := ℝ) (↑0 : ℝ) x) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
⊢ expUnitary (HSMul.hSMul (α := ℝ) (↑1 : ℝ) x) = expUnitary x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
⊢ Joined 1 (expUnitary x)

Tactic:
⟨expUnitaryPathToOne x⟩

Premises used: Nonempty.intro, selfAdjoint.expUnitaryPathToOne, Joined
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖(↑v : A) - (↑u : A)‖ < 2
⊢ Continuous.{0, u_1} (Y := ↥(unitary A)) fun (t : (↑unitInterval : Type)) ↦
    expUnitary ((↑t : ℝ) • argSelfAdjoint (v * star u)) * u

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖(↑v : A) - (↑u : A)‖ < 2
a : (↑(expUnitary (HSMul.hSMul (α := ℝ) (↑0 : ℝ) (argSelfAdjoint (v * star u))) * u) : A) = (↑u : A)
⊢ expUnitary (HSMul.hSMul (α := ℝ) (↑0 : ℝ) (argSelfAdjoint (v * star u))) * u = u

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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) : A) = (↑u : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖(↑v : A) - (↑u : A)‖ < 2
⊢ expUnitary (HSMul.hSMul (α := ℝ) (↑1 : ℝ) (argSelfAdjoint (v * star u))) * u = v

Tactic:
simp [expUnitary_eq_mul_inv v u huv, mul_assoc]

Premises used: mul_assoc, Unitary.expUnitary_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖(↑v : A) - (↑u : A)‖ < 2
⊢ Joined u v

Tactic:
⟨path u v huv⟩

Premises used: Unitary.path, Nonempty.intro, Joined
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
this : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
⊢ Continuous (Y := ↥(unitary A)) fun (x : ↥(unitary A)) ↦ u * x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
this : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
h : ball u δ = (fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ
⊢ IsPathConnected (ball u δ)

Tactic:
convert! this |>.image (f := (u * ·)) (by fun_prop)

Premises used: IsPathConnected.image
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
this : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
h :
  ∀ (v : ↥(unitary A)),
    v ∈ ball u δ ↔ Membership.mem (γ := Set ↥(unitary A)) ((fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ) v
⊢ ball u δ = (fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ

Tactic:
ext v
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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)
h : v ∈ ball u δ ↔ Membership.mem (γ := Set ↥(unitary A)) ((fun (x : ↥(unitary A)) ↦ u * x) '' ball (u⁻¹ * u) δ) v
⊢ v ∈ ball u δ ↔ Membership.mem (γ := Set ↥(unitary A)) ((fun (x : ↥(unitary A)) ↦ u * x) '' ball 1 δ) v

Tactic:
rw [← inv_mul_cancel u]

Premises used: inv_mul_cancel
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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 (u⁻¹ * u) δ) v

Tactic:
simp [-inv_mul_cancel, Subtype.dist_eq, dist_eq_norm, ← mul_sub]

Premises used: dist_eq_norm, inv_mul_cancel, mul_sub, Subtype.dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
suffices : IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)
⊢ IsPathConnected (ball u δ)

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]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
⊢ Membership.mem (γ := Set ↥(unitary A)) (ball 1 δ) 1

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
refine : ∀ {u : ↥(unitary A)} (hu : Membership.mem (γ := Set ↥(unitary A)) (ball 1 δ) u), JoinedIn (ball 1 δ) 1 u
⊢ IsPathConnected.{u_1} (X := ↥(unitary A)) (ball 1 δ)

Tactic:
refine ⟨1, by simpa, fun {u} hu ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
⊢ ‖(↑u : A) - 1‖ < δ

Tactic:
simpa [Subtype.dist_eq, dist_eq_norm] using hu

Premises used: dist_eq_norm, Subtype.dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
⊢ ‖(↑u : A) - 1‖ < δ

Tactic:
have hu : ‖(u - 1 : A)‖ < δ := by simpa [Subtype.dist_eq, dist_eq_norm] using hu
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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

Tactic:
⟨path 1 u (hu.trans hδ₂), fun t ↦ ?_⟩

Premises used: JoinedIn, Unitary.path, Exists.intro, LT.lt.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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‖ < δ
refine :
  ∀ (t : (↑unitInterval : Type)),
    Membership.mem (α := ↥(unitary A)) (γ := Set ↥(unitary A)) (ball 1 δ)
      ((path 1 u ⋯ : (a : (↑unitInterval : Type)) → ↥(unitary A)) t : ↥(unitary A))
⊢ JoinedIn (ball 1 δ) 1 u

Tactic:
refine ⟨path 1 u (hu.trans hδ₂), fun t ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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‖ < δ
t : (↑unitInterval : Type)
⊢ Membership.mem (α := ↥(unitary A)) (γ := Set ↥(unitary A)) (ball 1 δ)
    ((path 1 u ⋯ : (a : (↑unitInterval : Type)) → ↥(unitary A)) t : ↥(unitary A))

Tactic:
simpa [Subtype.dist_eq, dist_eq_norm] using
    norm_expUnitary_smul_argSelfAdjoint_sub_one_le u t.2 (hu.trans hδ₂) |>.trans_lt hu

Premises used: Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, dist_eq_norm, Subtype.dist_eq, LT.lt.trans, LE.le.trans_lt, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ ∀ (x : ↥(unitary A)) (i : ℝ),
    0 < i ∧ i < 2 →
      IsPathConnected.{u_1} (X := ↥(unitary A))
        {y : ↥(unitary A) |
          Membership.mem (γ := SetRel ↥(unitary A) ↥(unitary A)) {p : ↥(unitary A) × ↥(unitary A) | dist p.1 p.2 < i}
            (y, x)}

Tactic:
simpa using isPathConnected_ball

Premises used: Unitary.isPathConnected_ball
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
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
mpr :
  (∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u) →
    Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u ↔
    ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
mp :
  ∀ {u : ↥(unitary A)},
    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

Tactic:
revert u
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
mp :
  Subset.{u_1} (α := Set ↥(unitary A)) (connectedComponent 1)
    (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
⊢ ∀ {u : ↥(unitary A)},
    Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) u →
      ∃ (l : List ↥(selfAdjoint A)), (List.map expUnitary l).prod = u

Tactic:
simp_rw [← Set.mem_range, ← Set.subset_def, pathComponent_eq_connectedComponent]

Premises used: Set.mem_range, Set.subset_def, pathComponent_eq_connectedComponent
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ Eq.{u_1 + 1} (α := ↥(unitary A)) ((fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) []) 1

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
mp : IsClopen.{u_1} (X := ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
⊢ Subset.{u_1} (α := Set ↥(unitary A)) (connectedComponent 1)
    (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)

Tactic:
refine IsClopen.connectedComponent_subset ?_ ⟨[], by simp⟩