mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_4
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
⊢ ∀ (i : G), Set.SurjOn f ((fun x ↦ i • x) ⁻¹' U) (f '' U)

pp: case refine_5
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
x✝ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁ ⊓ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
h₁ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁
h₂ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
⊢ (fun x ↦ (g₁ * g₂⁻¹) • x) ((fun x ↦ g₂ • x) e) = (fun x ↦ g₁ • x) e

Tactic:
·

Goal state after:
case refine_4
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
⊢ ∀ (i : G), Set.SurjOn f ((fun x ↦ i • x) ⁻¹' U) (f '' U)
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_5
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
x✝ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁ ⊓ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
h₁ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁
h₂ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
⊢ (fun x ↦ (g₁ * g₂⁻¹) • x) ((fun x ↦ g₂ • x) e) = (fun x ↦ g₁ • x) e

Tactic:
·

Goal state after:
case refine_5
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
x✝ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁ ⊓ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
h₁ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁
h₂ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
⊢ (fun x ↦ (g₁ * g₂⁻¹) • x) ((fun x ↦ g₂ • x) e) = (fun x ↦ g₁ • x) e
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case pos
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
hxf : ↑x ∈ Set.range f
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑x})

pp: case neg
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
hxf : ↑x ∉ Set.range f
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑x})

Tactic:
·

Goal state after:
case pos
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
hxf : ↑x ∈ Set.range f
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑x})
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
hxf : ↑x ∉ Set.range f
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑x})

Tactic:
·

Goal state after:
case neg
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
hxf : ↑x ∉ Set.range f
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑x})
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inl
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
h✝ : IsEmpty E
⊢ IsCoveringMapOn f s

pp: case inr
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
h✝ : Nonempty E
⊢ IsCoveringMapOn f s

Tactic:
·

Goal state after:
case inl
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
h✝ : IsEmpty E
⊢ IsCoveringMapOn f s
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
⊢ f '' {e | MulAction.stabilizer G e = ⊥} = Set.univ

pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e

Tactic:
·

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
⊢ f '' {e | MulAction.stabilizer G e = ⊥} = Set.univ
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e

Tactic:
·

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
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
⊢ log (exp a) = a

Tactic:
have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := simp)

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)
⊢ log (exp a) = a
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case refine_1
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
e' : E
he' : e' ∈ U (idx e he) ∩ F.source
⊢ e' ∈ {x | (fun x ↦ (fun x ↦ idx e he) x = (fun x ↦ if he : f x ∈ V then idx x he else Classical.arbitrary ι) x) x}

Tactic:
by_contra h; apply (disjoint h).le_bot
    · dsimp only; rw [dif_pos (by exact he'.2)]; exact ⟨he'.1, idx_U ..⟩

Goal state after:
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 : ι
⊢ ContinuousOn (fun x ↦ F.invFun (x, i)) {a | (a, i) ∈ F.target}

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 : ι
⊢ ContinuousOn (fun x ↦ F.invFun (x, i)) {a | (a, i) ∈ F.target}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : s ≤ 0
⊢ z ^ n ∉ centeredArc s

Tactic:
simp [centeredArc_eq_empty h2]

Goal state after:
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
⊢ z ∈ centeredArc (s / ↑n)

Tactic:
mem_centeredArc ((div_le_self hs0.le hn).trans hs),

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
⊢ |(↑z).arg| < s / ↑n
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

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

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
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)

Tactic:
·

Goal state after:
case inl
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Subsingleton A
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inl
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✝ : IsEmpty ↑(f ⁻¹' {x})
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

pp: case inr
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})
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
·

Goal state after:
case inl
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✝ : IsEmpty ↑(f ⁻¹' {x})
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

pp: case inr
x y : Circle
hne : x ≠ y
⊢ (range ⇑(x.path y))ᶜ.Nonempty

Tactic:
·

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

Goal state before:
pp: case inl
x y : Circle
hyx : y ≠ x
hxP : x ∉ range ⇑((-x).path y)
⊢ JoinedIn {x}ᶜ (-x) y

pp: case inr
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
·

Goal state after:
case inl
x y : Circle
hyx : y ≠ x
hxP : x ∉ range ⇑((-x).path y)
⊢ JoinedIn {x}ᶜ (-x) y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case inl
x y : Circle
hyx : y ≠ x
hxP : x ∉ range ⇑((-x).path y)
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
exact ⟨(path (-x) y), fun t ↦ by grind⟩

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

Goal state before:
pp: case mp
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ ‖u - 1‖ ^ 2 < 2 ^ 2 → -1 ∉ spectrum ℂ u

pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ -1 ∉ spectrum ℂ u → ‖u - 1‖ ^ 2 < 2 ^ 2

Tactic:
·

Goal state after:
case mp
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
⊢ ¬{x, y}ᶜ ⊆ range ⇑(x.path y)

pp: case refine_2
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ⊆ range ⇑(x.path y) ∪ range ⇑(y.path x)

pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y}ᶜ ⊆ range ⇑(y.path x)

Tactic:
·

Goal state after:
case refine_1
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y}ᶜ ⊆ range ⇑(x.path y)
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
⊢ -1 ∉ spectrum ℂ u → ‖u - 1‖ ^ 2 < 2 ^ 2

Tactic:
·

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ -1 ∉ spectrum ℂ u → ‖u - 1‖ ^ 2 < 2 ^ 2
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inr.refine_2
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)
⊢ IsOpen[inst✝¹] s

pp: case inr.refine_3
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})
⊢ InjOn f (V' e)

Tactic:
·

Goal state after:
case inr.refine_2
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)
⊢ IsOpen[inst✝¹] s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y}ᶜ ⊆ range ⇑(y.path x)

Tactic:
·

Goal state after:
case refine_2
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ⊆ range ⇑(x.path y) ∪ range ⇑(y.path x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y}ᶜ ⊆ range ⇑(y.path x)

Tactic:
·

Goal state after:
case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case inl
⊢ Periodic (fun x ↦ Circle.exp (2 * π / 0 * x)) 0

pp: case inr
T : ℝ
hT : T ≠ 0
⊢ Periodic (fun x ↦ Circle.exp (2 * π / T * x)) T

Tactic:
·

Goal state after:
case inl
⊢ Periodic (fun x ↦ Circle.exp (2 * π / 0 * x)) 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
·

Goal state after:
case inr
T : ℝ
hT : T ≠ 0
⊢ Periodic (fun x ↦ Circle.exp (2 * π / T * x)) T
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

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

pp: case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ Real.cos ‖x‖ ∈ lowerBounds ((fun a ↦ Real.cos a) '' spectrum ℝ ↑x)

Tactic:
·

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