mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖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 ↦ ‖x - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (fun x ↦ x - 1) u‖ ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
⊢ -x ≠ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
⊢ x ∉ range ⇑(y.path (-x))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ 0 ≤ ‖u - 1‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ 0 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x : Circle
⊢ IsPathConnected {x}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hxy : x ≠ y
⊢ {x, y} ⊆ range ⇑(x.path y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : 2 ^ 2 ≤ 2 * (1 - z.re)
⊢ z.re ≤ -1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hxy : x ≠ y
⊢ {x, y} ⊆ range ⇑(y.path x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hxy : x ≠ y
⊢ ¬IsPreconnected {x, y}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝² : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝¹ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
⊢ f '' V' e ⊆ (φ e).target

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ : Angle
⊢ ↑θ.toCircle = ↑θ.cos + ↑θ.sin * I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ toCircle 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ toCircle 0 = 1

Tactic:
by rw [← coe_zero, toCircle_coe, Circle.exp_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ : Angle
⊢ (-θ).toCircle = θ.toCircle⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
⊢ ‖u - 1‖ < 2 ↔ -1 ∉ spectrum ℂ u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ : Angle
⊢ ↑(↑θ.toCircle).arg = θ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
⊢ spectrum ℂ u ⊆ slitPlane ↔ ‖u - 1‖ < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
⊢ IsSelfAdjoint (cfc (ofReal ∘ arg) u)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
⊢ Periodic (fun x ↦ Circle.exp (2 * π / T * x)) T

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x y : AddCircle T
⊢ (x + y).toCircle = x.toCircle * y.toCircle

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
⊢ toCircle 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x : AddCircle T
⊢ (-x).toCircle * x.toCircle = x.toCircle⁻¹ * x.toCircle

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
h : -‖↑x‖ ∈ spectrum ℝ ↑x
⊢ (fun a ↦ Real.cos a) (-‖↑x‖) = Real.cos ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case refine_1.inr
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
h : -‖↑x‖ ∈ spectrum ℝ ↑x
⊢ Real.cos ‖x‖ ∈ (fun a ↦ Real.cos a) '' spectrum ℝ ↑x

Tactic:
exact ⟨_, h, by simp⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x : AddCircle T
n : ℕ
⊢ (n • x).toCircle = x.toCircle ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
y : ℝ
hy : y ∈ spectrum ℝ ↑x
⊢ 0 ≤ |y|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x : AddCircle T
n : ℤ
⊢ (n • x).toCircle = x.toCircle ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
⊢ Continuous (HMul.hMul (2 * π / T))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
⊢ ‖↑(expUnitary x) - 1‖ ^ 2 = 2 * (1 - Real.cos ‖x‖)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝² : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝³ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝² : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝¹ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝¹ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this✝ : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h✝ : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
e'' : E
left✝ : e'' ∈ V ↑e
mem : e'' ∈ (φ e).source
eq : f e'' = f e'
⊢ ↑(φ e) e'' = ↑(φ e) e'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 0 ≤ ‖↑(expUnitary x) - 1‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 0 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 0 ≤ ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
hT : T ≠ 0
⊢ Injective toCircle

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 2 * (1 - Real.cos π) = 2 ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
⊢ Continuous fun x ↦ ↑(↑x).arg

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
hT : T ≠ 0
⊢ 2 * π ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ spectrum ℂ ↑(expUnitary x) ⊆ slitPlane

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
hT : T ≠ 0
x : AddCircle T
⊢ (homeomorphCircle hT) x = x.toCircle

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ IsAddQuotientCoveringMap ⇑exp ↥(AddSubgroup.zmultiples (2 * π))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x✝¹ : ℕ
x✝ : True
⊢ 0 < π / 2 ^ (x✝¹ + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ ∀ᶠ (i : ℕ) in Filter.atTop, True

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ (nhds 1).HasBasis (fun x ↦ True) fun n ↦ centeredArc (π / 2 ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r : ℝ
⊢ {x | |x| < r} = Ioo (-r) r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r : ℝ
⊢ IsOpen (centeredArc r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
⊢ z ∈ centeredArc (π / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
ih : z ∈ centeredArc (π / 2 ^ (n + 1))
⊢ z ∈ centeredArc (π / ↑(2 ^ (n + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
ih : z ∈ centeredArc (π / 2 ^ (n + 1))
⊢ 2 ^ (n + 1) > 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
⊢ z ∈ centeredArc (π / 2 ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
⊢ z = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
⊢ IsUnit ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
x✝ : ℝ
⊢ ∀ ⦃a₂ : ℝ⦄, (fun x ↦ n • x) x✝ = (fun x ↦ n • x) a₂ → x✝ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits 1);
    { toLinearEquiv := __spread.0, norm_map' := ⋯ }) =
    1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
x✝¹ x✝ : ↥(unitary A)
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits (x✝¹ * x✝));
    { toLinearEquiv := __spread.0, norm_map' := ⋯ }) =
    (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits x✝¹);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ }) *
      let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits x✝);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
u : ↥(unitary A)
⊢ ((mulLeft R A) u).symm = (mulLeft R A) (star u)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
inst✝ : T2Space E
hf : IsClosedMap f
hs : ∀ x ∈ s, (f ⁻¹' {x}).Finite
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
hx : x ∈ s
e : E
he : e ∈ f ⁻¹' {x}
⊢ e ∈ f ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
u v : ↥(unitary A)
x : A
⊢ ((mulLeft R A) (u * v)) x = ((mulLeft R A) u) (((mulLeft R A) v) x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
inst✝ : T2Space E
hf : IsClosedMap f
hs : ∀ x ∈ s, (f ⁻¹' {x}).Finite
h : IsLocalHomeomorphOn f (f ⁻¹' s)
⊢ IsCoveringMapOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
u : ↥(unitary A)
⊢ (mulRight R u).symm = mulRight R (star u)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
u v : ↥(unitary A)
⊢ (mulRight R u).trans (mulRight R v) = mulRight R (u * v)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
s : Set X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
hf : Continuous[inst✝⁴, inst✝³] f
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
hx : x ∈ s
e : E
he : e ∈ f ⁻¹' {x}
⊢ e ∈ f ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
u v : ↥(unitary A)
x : A
⊢ (mulRight R (u * v)) x = (mulRight R v) ((mulRight R u) x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
⊢ mulRight R 1 = LinearIsometryEquiv.refl R A

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
s : Set X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
hf : Continuous[inst✝⁴, inst✝³] f
h : IsLocalHomeomorphOn f (f ⁻¹' s)
⊢ IsCoveringMapOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ argSelfAdjoint (expUnitary x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
h : IsLocalHomeomorph f
⊢ Continuous[inst✝⁴, inst✝³] f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
⊢ normalize 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ normalize x = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ ‖x‖ • normalize x = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
h : ‖x‖ = 1
⊢ normalize x = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
⊢ IsLocalHomeomorph f ↔ IsCoveringMap f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ normalize (normalize x) = normalize x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ normalize (-x) = -normalize x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
r : ℝ
hr : 0 < r
x : V
⊢ normalize (r • x) = normalize x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
r : ℝ
hr : r < 0
x : V
⊢ normalize (r • x) = -normalize x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ 0 ≤ ‖a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
r : ℝ
x : V
⊢ normalize (r • x) = ↑(SignType.sign r) • normalize x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
⊢ (I * ↑y.arg).re = (log y).re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
⊢ (I * ↑y.arg).im = (log y).im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this✝ : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
this : I * ↑y.arg = log y
⊢ y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ expUnitary (argSelfAdjoint u) = u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ 0 ≤ π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
⊢ ‖↑y.arg‖ ≤ π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = ‖↑u - 1‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 0 ≤ ‖argSelfAdjoint u‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ ‖argSelfAdjoint u‖ = Real.arccos (1 - ‖↑u - 1‖ ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖

Tactic:
by

Goal state after: