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

Goal state before:
pp: case refine_1
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst✝¹] fst

pp: case refine_2
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst✝¹] fst

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst✝¹] fst

case refine_2
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst✝¹] fst
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f → ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) → IsLocallyInjective f

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f → ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) → IsLocallyInjective f
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inl
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e.source
hs : p ∈ proj ⁻¹' s
⊢ (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p

pp: case inr
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e'.source
hs : p ∉ proj ⁻¹' s
⊢ (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p

Tactic:
<;>

Goal state after:
case inl
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e.source
hs : p ∈ proj ⁻¹' s
⊢ (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p

case inr
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e'.source
hs : p ∉ proj ⁻¹' s
⊢ (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.1 x✝ = x✝¹.toProd.1 x✝

pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.2 x✝ = x✝¹.toProd.2 x✝

Tactic:
<;>

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.1 x✝ = x✝¹.toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.2 x✝ = x✝¹.toProd.2 x✝
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.1 x✝ = (star x✝² + star x✝¹).toProd.1 x✝

pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.2 x✝ = (star x✝² + star x✝¹).toProd.2 x✝

Tactic:
<;>

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.1 x✝ = (star x✝² + star x✝¹).toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.2 x✝ = (star x✝² + star x✝¹).toProd.2 x✝
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.1 x✝ = (star x✝¹ * star x✝²).toProd.1 x✝

pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.2 x✝ = (star x✝¹ * star x✝²).toProd.2 x✝

Tactic:
<;>

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.1 x✝ = (star x✝¹ * star x✝²).toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.2 x✝ = (star x✝¹ * star x✝²).toProd.2 x✝
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² : 𝕜
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² • x✝¹)).toProd.1 x✝ = (star x✝² • star x✝¹).toProd.1 x✝

pp: case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² : 𝕜
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² • x✝¹)).toProd.2 x✝ = (star x✝² • star x✝¹).toProd.2 x✝

Tactic:
<;>

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² : 𝕜
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² • x✝¹)).toProd.1 x✝ = (star x✝² • star x✝¹).toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² : 𝕜
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² • x✝¹)).toProd.2 x✝ = (star x✝² • star x✝¹).toProd.2 x✝
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inl
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source

pp: case inl.hi
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source

Tactic:
<;>

Goal state after:
case inl
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source

case inl.hi
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ IsTopologicalBasis {U | ∃ V, IsOpen[inst✝] V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ ∀ u ∈ {U | ∃ V, IsOpen[inst✝] V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, IsOpen[inst✝¹] u

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
⊢ ∃ v ∈ {U | ∃ V, IsOpen[inst✝] V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, x ∈ v ∧ v ⊆ U
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

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:
<;>

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
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

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.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

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:
<;>

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)
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

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
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : 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
| exp (cfc id a)

Tactic:
cfc_apply id a ha

Goal state after:
𝕜 : 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
| exp ((cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: 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

pp: 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 * π

Tactic:
<;>

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: 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

pp: 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 * π

Tactic:
<;>

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: 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

pp: 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 * π

Tactic:
<;>

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: case pos
x y : Circle
hxy : (↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp ((↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y

pp: case neg
x y : Circle
hxy : ¬(↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp (2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y

Tactic:
<;>

Goal state after:
case pos
x y : Circle
hxy : (↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp ((↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y

case neg
x y : Circle
hxy : ¬(↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp (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 : ι
⊢ ContinuousOn (fun x ↦ F.invFun (x, i)) {a | (a, i) ∈ F.target}

Tactic:
simp_rw [F, Set.prodMk_mem_set_prod_eq, Set.mem_univ, and_true]
    refine (continuousOn_open_iff open_V).mpr fun W open_W ↦ ?_
    rw [open_iff i Set.inter_subset_left]
    convert! ((open_iff i subset_rfl).mp open_V).inter open_W using 1
    refine Set.ext fun e ↦ and_right_comm.trans (and_congr_right fun ⟨hV, hU⟩ ↦ ?_)
    rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]

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

Goal state before:
pp: case refine_1
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' Ioo 0 1 ⊆ ⇑(x.path y) '' Ioc 0 1

pp: case refine_2
x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ ⇑(y.path x) '' Ioc 0 1

Tactic:
<;>

Goal state after:
case refine_1
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' Ioo 0 1 ⊆ ⇑(x.path y) '' Ioc 0 1

case refine_2
x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ ⇑(y.path x) '' Ioc 0 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hyx : y ≠ x
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
obtain hxP | hxP := (em (x ∈ range (path (-x) y))).symm

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

case inr
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
⊢ JoinedIn {x}ᶜ (-x) y
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 ↔ -1 ∉ spectrum ℂ u

Tactic:
← sq_lt_sq₀ (by positivity) (by positivity)

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: x y : Circle
hxy : x ≠ y
⊢ {x, y} ⊆ range ⇑(y.path x)

Tactic:
by simp only [pair_subset_iff,
      (path y x).source_mem_range, (path y x).target_mem_range, and_self]

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

Goal state before:
pp: case ofNat
T : ℝ
x : AddCircle T
a✝ : ℕ
⊢ (Int.ofNat a✝ • x).toCircle = x.toCircle ^ Int.ofNat a✝

pp: case negSucc
T : ℝ
x : AddCircle T
a✝ : ℕ
⊢ (Int.negSucc a✝ • x).toCircle = x.toCircle ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
T : ℝ
x : AddCircle T
a✝ : ℕ
⊢ (Int.ofNat a✝ • x).toCircle = x.toCircle ^ Int.ofNat a✝

case negSucc
T : ℝ
x : AddCircle T
a✝ : ℕ
⊢ (Int.negSucc a✝ • x).toCircle = x.toCircle ^ Int.negSucc a✝
Module: Mathlib.Analysis.Normed.Module.Normalize

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

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize x = 0 ↔ x = 0

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : x = 0
⊢ normalize x = 0 ↔ x = 0

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize x = 0 ↔ x = 0
Module: Mathlib.Analysis.Normed.Module.Normalize

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

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ ‖x‖ • normalize x = x

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : x = 0
⊢ ‖x‖ • normalize x = x

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ ‖x‖ • normalize x = x
Module: Mathlib.Analysis.Normed.Module.Normalize

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

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : x = 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0