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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsOpen[inst✝¹] s
hX : ∀ (a : ↑s), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
⊢ Subtype.val ⁻¹' ↑e '' {x} = {⟨↑e x, ⋯⟩}

Tactic:
ext

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsOpen[inst✝¹] s
hX : ∀ (a : ↑s), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
x✝ : { x // x ∈ ↑e '' s }
⊢ x✝ ∈ Subtype.val ⁻¹' ↑e '' {x} ↔ x✝ ∈ {⟨↑e x, ⋯⟩}
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
hf : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
⊢ g = g'

Tactic:
by
    have ⟨U, heU, hU⟩ := hf.disjoint e
    simpa [inv_mul_eq_one, eq_comm] using hU (g'⁻¹ * g)
      ⟨e, ⟨e, mem_of_mem_nhds heU, by simpa [mul_smul, inv_smul_eq_iff]⟩, mem_of_mem_nhds heU⟩

Goal state after:
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
Y : Type u_4
inst✝ : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap (⇑φ ∘ f) G
⊢ f = ⇑φ.symm ∘ ⇑φ ∘ f

Tactic:
ext

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
Y : Type u_4
inst✝ : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap (⇑φ ∘ f) G
x✝ : E
⊢ f x✝ = (⇑φ.symm ∘ ⇑φ ∘ f) x✝
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
hf : IsQuotientCoveringMap f G
x : X
this : MulAction G ↑(f ⁻¹' {x}) := hf.mulActionFiber x
⊢ MulAction.IsPretransitive G ↑(f ⁻¹' {x})

Tactic:
constructor

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
hf : IsQuotientCoveringMap f G
x : X
this : MulAction G ↑(f ⁻¹' {x}) := ⋯
⊢ ∀ (x_1 y : ↑(f ⁻¹' {x})), ∃ g, g • x_1 = y
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case h
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 : IsQuotientCoveringMap f G
x : X
e : ↑(f ⁻¹' {x})
this✝ : MulAction G ↑(f ⁻¹' {x}) := ⋯
this : MulAction.IsPretransitive G ↑(f ⁻¹' {x})
g : G
⊢ ((hf.toPermFiber x) g) e = g • e

Tactic:
ext

Goal state after:
case h
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 : IsQuotientCoveringMap f G
x : X
e : ↑(f ⁻¹' {x})
this✝ : MulAction G ↑(f ⁻¹' {x}) := ⋯
this : MulAction.IsPretransitive G ↑(f ⁻¹' {x})
g : G
⊢ ↑(((hf.toPermFiber x) g) e) = ↑(g • e)
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
I : Type u_3
inst✝ : TopologicalSpace I
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ ↑({ toFun := fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2),
            invFun := fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
            continuous_toFun := ⋯, continuous_invFun := ⋯ }
          x✝).1 =
    s.restrictPreimage f ↑x✝

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ ↑↑({ toFun := fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2),
              invFun := fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
              continuous_toFun := ⋯, continuous_invFun := ⋯ }
            x✝).1 =
    ↑(s.restrictPreimage f ↑x✝)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Subtype.val ∘ f ⁻¹' Subtype.val '' U = f ⁻¹' U

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : E
⊢ x✝ ∈ Subtype.val ∘ f ⁻¹' Subtype.val '' U ↔ x✝ ∈ f ⁻¹' U
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
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
⊢ Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝¹ : Nonempty I
hUs : U ⊆ s
x✝ : E
⊢ x✝ ∈ Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U ↔ x✝ ∈ f ⁻¹' U
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
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
E' : Type u_4
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsEvenlyCovered (f ∘ ⇑g) x I
⊢ f = (f ∘ ⇑g) ∘ ⇑g.symm

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
E' : Type u_4
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsEvenlyCovered (f ∘ ⇑g) x I
x✝ : E
⊢ f x✝ = ((f ∘ ⇑g) ∘ ⇑g.symm) x✝
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_5
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

Tactic:
ext

Goal state after:
case e'_5
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
x✝ : E
⊢ f x✝ = (⇑g.symm ∘ ⇑g ∘ f) x✝
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_6
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ x = g.symm (g x)

Tactic:
ext

Goal state after:
case e'_6
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ x = g.symm (g x)
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_5
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝ : AddCircle p
⊢ HSMul.hSMul n = HSMul.hSMul ↑n

Tactic:
ext

Goal state after:
case e'_5
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝¹ x✝ : AddCircle p
⊢ n • x✝ = ↑n • x✝
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝ : AddCircle p
⊢ nsmulAddMonoidHom n = zsmulAddGroupHom ↑n

Tactic:
ext

Goal state after:
case e'_6
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝¹ : AddCircle p
x✝ : 𝕜
⊢ ((nsmulAddMonoidHom n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝ =
    ((zsmulAddGroupHom ↑n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_7
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
⊢ nsmulAddMonoidHom n = zsmulAddGroupHom ↑n

Tactic:
ext

Goal state after:
case e'_7
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
x✝ : 𝕜
⊢ ((nsmulAddMonoidHom n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝ =
    ((zsmulAddGroupHom ↑n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_8
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
e_7✝ : (nsmulAddMonoidHom n).ker.toAddGroup ≍ (zsmulAddGroupHom ↑n).ker.toAddGroup
⊢ nsmulAddMonoidHom n = zsmulAddGroupHom ↑n

Tactic:
ext

Goal state after:
case e'_8
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
e_7✝ : (nsmulAddMonoidHom n).ker.toAddGroup ≍ (zsmulAddGroupHom ↑n).ker.toAddGroup
x✝ : 𝕜
⊢ ((nsmulAddMonoidHom n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝ =
    ((zsmulAddGroupHom ↑n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝
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
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty ↑(f ⁻¹' {f x})
e : Trivialization (↑(f ⁻¹' {f x})) f := ⋯.toTrivialization
h : f x ∈ ⋯.toTrivialization.baseSet
he : x ∈ e.source := (Trivialization.mem_source e).mpr h
⊢ (↑e.symm.symm x).1 ∈ e.baseSet

Tactic:
e.toOpenPartialHomeomorph.symm_symm,

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty ↑(f ⁻¹' {f x})
e : Trivialization (↑(f ⁻¹' {f x})) f := ⋯.toTrivialization
h : f x ∈ ⋯.toTrivialization.baseSet
he : x ∈ e.source := (Trivialization.mem_source e).mpr h
⊢ (↑e.toOpenPartialHomeomorph x).1 ∈ e.baseSet
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
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMapOn (f ∘ ⇑g) s
⊢ f = (f ∘ ⇑g) ∘ ⇑g.symm

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMapOn (f ∘ ⇑g) s
x✝ : E
⊢ f x✝ = ((f ∘ ⇑g) ∘ ⇑g.symm) x✝
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_5
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

Tactic:
ext

Goal state after:
case e'_5
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
x✝ : E
⊢ f x✝ = (⇑g.symm ∘ ⇑g ∘ f) x✝
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_6
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
⊢ s = ⇑g.symm.symm ⁻¹' ⇑g.symm ⁻¹' s

Tactic:
ext

Goal state after:
case e'_6
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
x✝ : X
⊢ x✝ ∈ s ↔ x✝ ∈ ⇑g.symm.symm ⁻¹' ⇑g.symm ⁻¹' s
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
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMap (f ∘ ⇑g)
⊢ f = (f ∘ ⇑g) ∘ ⇑g.symm

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMap (f ∘ ⇑g)
x✝ : E
⊢ f x✝ = ((f ∘ ⇑g) ∘ ⇑g.symm) x✝
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
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

Tactic:
ext

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
x✝ : E
⊢ f x✝ = (⇑g.symm ∘ ⇑g ∘ f) x✝
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: case e_6
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ { toFun := (spectrum 𝕜 a).domRestrict exp, continuous_toFun := ⋯ } =
    exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ }

Tactic:
ext

Goal state after:
case e_6
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
a✝ : ↑(spectrum 𝕜 a)
⊢ { toFun := (spectrum 𝕜 a).domRestrict exp, continuous_toFun := ⋯ } a✝ =
    (exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ }) a✝
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
r : ℝ
⊢ log ((algebraMap ℝ A) r) = (algebraMap ℝ A) (Real.log r)

Tactic:
by
  simp [log]

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

Goal state before:
pp: x y : ℝ
⊢ exp x = exp y ↔ ∃ m, x = y + ↑m * (2 * π)

Tactic:
rw [Subtype.ext_iff, coe_exp, coe_exp, exp_eq_exp_iff_exists_int]

Goal state after:
x y : ℝ
⊢ (∃ n, ↑x * I = ↑y * I + ↑n * (2 * ↑π * I)) ↔ ∃ m, x = y + ↑m * (2 * π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: a b : ℝ
h : b - a < 2 * π
x : ℝ
x✝¹ : x ∈ Icc a b
y : ℝ
x✝ : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ x - y ∈ Ioo (-2 * π) (2 * π)

Tactic:
constructor

Goal state after:
case left
a b : ℝ
h : b - a < 2 * π
x : ℝ
x✝¹ : x ∈ Icc a b
y : ℝ
x✝ : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ -2 * π < x - y

case right
a b : ℝ
h : b - a < 2 * π
x : ℝ
x✝¹ : x ∈ Icc a b
y : ℝ
x✝ : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ x - y < 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ico a b
y : ℝ
x✝ : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ x - y ∈ Ioo (-2 * π) (2 * π)

Tactic:
constructor

Goal state after:
case left
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ico a b
y : ℝ
x✝ : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ -2 * π < x - y

case right
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ico a b
y : ℝ
x✝ : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ x - y < 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ioc a b
y : ℝ
x✝ : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ x - y ∈ Ioo (-2 * π) (2 * π)

Tactic:
constructor

Goal state after:
case left
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ioc a b
y : ℝ
x✝ : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ -2 * π < x - y

case right
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ioc a b
y : ℝ
x✝ : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ x - y < 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
← image_union,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' (Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Icc (↑y).arg (y.angleDiff x + (↑y).arg)) = univ
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 (↑y).arg (y.angleDiff x + (↑y).arg) = univ

Tactic:
← image_union,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' (Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)) = univ
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:
constructor

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

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.Analysis.CStarAlgebra.Unitary.Connected

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

Tactic:
ext

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ ↑(argSelfAdjoint (expUnitary x)) = ↑x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case e'_5
⊢ ⇑exp = ⇑(homeomorphCircle ⋯) ∘ QuotientAddGroup.mk

Tactic:
ext

Goal state after:
case e'_5
x✝ : ℝ
⊢ ↑(exp x✝) = ↑((⇑(homeomorphCircle ⋯) ∘ QuotientAddGroup.mk) x✝)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case e'_5
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ ⇑(zpowGroupHom n) ∘ ⇑e = ⇑e ∘ fun x ↦ n • x

Tactic:
ext

Goal state after:
case e'_5
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := ⋯
x✝ : AddCircle 1
⊢ ↑((⇑(zpowGroupHom n) ∘ ⇑e) x✝) = ↑((⇑e ∘ fun x ↦ n • x) x✝)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ ⇑e ⁻¹' ↑(zpowGroupHom n).ker = {x | n • x = 0}

Tactic:
ext

Goal state after:
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
x✝ : AddCircle 1
⊢ x✝ ∈ ⇑e ⁻¹' ↑(zpowGroupHom n).ker ↔ x✝ ∈ {x | n • x = 0}
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
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
y : ℂ
hy : y ∈ spectrum ℂ ↑x
⊢ ↑(NormedSpace.exp (I • y)).arg = y

Tactic:
rw [← x.2.spectrumRestricts.algebraMap_image] at hy

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
y : ℂ
hy : y ∈ ⇑(algebraMap ℝ ℂ) '' spectrum ℝ ↑x
⊢ ↑(NormedSpace.exp (I • y)).arg = y
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:
ext

Goal state after:
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✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits 1);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    1 x✝
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:
ext

Goal state after:
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)
x✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits (x✝² * x✝¹));
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    ((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' := ⋯ })
      x✝