mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : ℝ
⊢ z + 2 * π = z + 2 * π

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc (fun x ↦ Real.log (Real.exp x)) a = a

Tactic:
]

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc (fun x ↦ Real.log (Real.exp x)) a = a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ t₁ = t₂

Tactic:
]

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ t₁ = t₂
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc (fun x ↦ Real.exp (Real.log x)) a = a

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc (fun x ↦ Real.exp (Real.log x)) a = a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1

Tactic:
]

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : (cexp (↑(t₁ - t₂) * I)).re = re 1 ∧ (cexp (↑(t₁ - t₂) * I)).im = im 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1

Tactic:
]

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : (cexp (↑(t₁ - t₂) * I)).re = re 1 ∧ (cexp (↑(t₁ - t₂) * I)).im = im 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
e : E
he : e ∈ F.source
⊢ IsOpen[inst✝⁴] V

Tactic:
]

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
e : E
he : e ∈ F.source
⊢ IsOpen[inst✝⁴] V
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r : ℝ
hr : r ≤ π
t : ℝ
ht : t ∈ {x | |x| < r}
htπ : |t| < π
⊢ |t| < r

Tactic:
]

Goal state after:
r : ℝ
hr : r ≤ π
t : ℝ
ht : t ∈ {x | |x| < r}
htπ : |t| < π
⊢ |t| < r
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s

Tactic:
]

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s

Tactic:
]

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : ↑n * |(↑z).arg| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s

pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ (↑(↑z).arg).toReal ∈ Ioo (-π / ↑n) (π / ↑n)

Tactic:
]

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : ↑n * |(↑z).arg| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s

z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ (↑(↑z).arg).toReal ∈ Ioo (-π / ↑n) (π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ |(↑z).arg| < π / ↑n

Tactic:
]

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ |(↑z).arg| < π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ exp
      ((if (↑(exp (↑x).arg)).arg ≤ (↑y).arg then (↑y).arg - (↑(exp (↑x).arg)).arg
        else 2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg) +
        (↑x).arg) =
    y

Tactic:
]

Goal state after:
x y : Circle
⊢ exp
      ((if (↑(exp (↑x).arg)).arg ≤ (↑y).arg then (↑y).arg - (↑(exp (↑x).arg)).arg
        else 2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg) +
        (↑x).arg) =
    y
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case refine_3
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
W : Set E
open_W : IsOpen[inst✝⁵] W
⊢ IsOpen[inst✝⁵] (f ⁻¹' (V ∩ (fun x ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) ⁻¹' W) ∩ U i)

Tactic:
]

Goal state after:
case refine_3
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
W : Set E
open_W : IsOpen[inst✝⁵] W
⊢ IsOpen[inst✝⁵] (f ⁻¹' (V ∩ (fun x ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) ⁻¹' W) ∩ U i)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
t : ↑unitInterval
⊢ ↑(exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) t)) =
    ↑(exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) t))

Tactic:
]

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ Injective (⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)))

Tactic:
]

Goal state after:
x y : Circle
hne : x ≠ y
⊢ Injective (⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ Icc (↑x).arg (x.angleDiff y + (↑x).arg) ⊆ Icc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
]

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

Goal state before:
pp: x y : Circle
⊢ ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg) = ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
]

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' Ico (↑x).arg (x.angleDiff y + (↑x).arg) = ⇑exp '' Ico (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
]

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg) = ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
]

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ range ⇑exp = univ

Tactic:
]

Goal state after:
x y : Circle
h : x ≠ y
⊢ range ⇑exp = univ
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✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
W : Set E
open_W : IsOpen[inst✝⁵] W
e : E
x✝ : f e ∈ V ∧ e ∈ U i
hV : f e ∈ V
hU : e ∈ U i
⊢ e ∈ W ↔ e ∈ W

Tactic:
]

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

Goal state before:
pp: x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
⊢ Disjoint (⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (⇑exp '' Ioc (↑y).arg (y.angleDiff x + (↑y).arg))

Tactic:
]

Goal state after:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
⊢ Disjoint (⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (⇑exp '' Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_1
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)

Tactic:
]

Goal state after:
case refine_1
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ √(2 * (1 - z.re)) ≤ ‖u - 1‖

Tactic:
]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ √(2 * (1 - z.re)) ≤ ‖u - 1‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_2
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ b ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)

Tactic:
]

Goal state after:
case refine_2
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ b ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
this : ‖z‖ = 1
⊢ √(2 * (1 - z.re)) ≤ ‖cfc (fun x ↦ x - 1 x) u‖

Tactic:
]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
this : ‖z‖ = 1
⊢ √(2 * (1 - z.re)) ≤ ‖cfc (fun x ↦ x - 1 x) u‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ {x}ᶜ

Tactic:
]

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ {x}ᶜ
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

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

Tactic:
]

Goal state after:
case inr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
⊢ ‖cfc (fun x ↦ x - 1 x) u‖ ^ 2 = 2 * (1 - x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ (range ⇑(x.path y))ᶜ.Nonempty

Tactic:
]

Goal state after:
x y : Circle
⊢ (range ⇑(x.path y))ᶜ.Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case inr
x y : Circle
hne : x ≠ y
⊢ (⇑(y.path x) '' Ioo 0 1).Nonempty

Tactic:
]

Goal state after:
case inr
x y : Circle
hne : x ≠ y
⊢ (⇑(y.path x) '' Ioo 0 1).Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' insert 0 (insert 1 (Ioo 0 1)) ∩ ⇑(y.path x) '' insert 0 (insert 1 (Ioo 0 1)) = {x, y}

Tactic:
]

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' insert 0 (insert 1 (Ioo 0 1)) ∩ ⇑(y.path x) '' insert 0 (insert 1 (Ioo 0 1)) = {x, y}
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
hP₂ : x ∈ range ⇑(y.path (-x))
h : x ∈ {-x, y}
⊢ False

Tactic:
]

Goal state after:
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
hP₂ : x ∈ range ⇑(y.path (-x))
h : x ∈ {-x, y}
⊢ False
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
⊢ ‖u - 1‖ ^ 2 < 2 ^ 2 ↔ -1 ∉ spectrum ℂ u

Tactic:
]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ ‖u - 1‖ ^ 2 < 2 ^ 2 ↔ -1 ∉ spectrum ℂ u
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_1
x y : Circle
hxy : x ≠ y
⊢ ¬range ⇑(x.path y) = univ

Tactic:
]

Goal state after:
case refine_1
x y : Circle
hxy : x ≠ y
⊢ ¬range ⇑(x.path y) = univ
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ 2 ^ 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u

Tactic:
]

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ 2 ^ 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_2
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ⊆ univ

Tactic:
]

Goal state after:
case refine_2
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ⊆ univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ {x, y} = ∅

Tactic:
]

Goal state after:
case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ {x, y} = ∅
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 ⊆ f '' (φ e).source

Tactic:
]

Goal state after:
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 ⊆ f '' (φ e).source
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬range ⇑(y.path x) = univ

Tactic:
]

Goal state after:
case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬range ⇑(y.path x) = univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case mpr
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 : z = -↑1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
]

Goal state after:
case mpr
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 : z = -↑1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case h
x✝ : ℝ
⊢ ↑x✝ = ↑x✝

Tactic:
]

Goal state after: