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

Goal state before:
pp: x : ℝ
z : ℤ
⊢ exp x ^ z = exp x ^ z

Tactic:
]

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

Goal state before:
pp: h : exp Real.pi = 1
heq : -1 = 1
⊢ False

Tactic:
]

Goal state after:
h : exp Real.pi = 1
heq : -1 = 1
⊢ False
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖v‖ = ‖v‖

Tactic:
]

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

Goal state before:
pp: x y : ℝ
⊢ Circle.exp (2 * π * x) * Circle.exp (2 * π * y) = Circle.exp (2 * π * x) * Circle.exp (2 * π * y)

Tactic:
]

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

Goal state before:
pp: ⊢ ∃ a, 𝐞 a ≠ 1 a

Tactic:
]

Goal state after:
⊢ ∃ a, 𝐞 a ≠ 1 a
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: case h
⊢ Circle.exp π ≠ 1

Tactic:
]

Goal state after:
case h
⊢ Circle.exp π ≠ 1
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: ⊢ ∃ a, probChar a ≠ 1 a

Tactic:
]

Goal state after:
⊢ ∃ a, probChar a ≠ 1 a
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ ↑e ⁻¹' interior s

Tactic:
hs.interior_eq

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ ↑e ⁻¹' s
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ ↑e ⁻¹' s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.restr (↑e ⁻¹' s) = e.restr (↑e ⁻¹' s)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst✝¹] s
⊢ e.restr s = e.restr s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖toEuclideanCLM (diagonal v)‖ = ‖v‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖toEuclideanCLM (diagonal v)‖ = ‖v‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e.symm ⁻¹' e'.source ∩ ↑e '' s

Tactic:
]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e.symm ⁻¹' e'.source ∩ ↑e '' s
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
i : n
x✝ : i ∈ Finset.univ
⊢ ‖v‖ ^ 2 * ‖x.ofLp i‖ ^ 2 ≤ ?m.78 i

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ = ‖toLp 2 (diagonal v *ᵥ Pi.single i 1)‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ = ‖toLp 2 (diagonal v *ᵥ Pi.single i 1)‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e '' s ∩ ↑e.symm ⁻¹' e'.source

Tactic:
]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e '' s ∩ ↑e.symm ⁻¹' e'.source
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T‖ * ‖toLp 2 (Pi.single i 1)‖ ≤ ‖T‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T‖ * ‖toLp 2 (Pi.single i 1)‖ ≤ ‖T‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = ↑e '' e.source ∩ ↑e '' s

Tactic:
]

Goal state after:
case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = ↑e '' e.source ∩ ↑e '' s
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖r • (toEuclideanLin ≪≫ₗ toContinuousLinearMap) x‖ ≤ ‖r‖ * ‖x‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖r • (toEuclideanLin ≪≫ₗ toContinuousLinearMap) x‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : ↑e x = ↑e y
⊢ ↑e.symm (↑e y) = ↑e.symm (↑e y)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX'.prod eY').source.Nonempty
⊢ eX = eX' ∧ eY = eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace X'
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace Y'
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace Z'
e✝ e e' : OpenPartialHomeomorph X Y
inst✝¹ : (x : X) → Decidable (x ∈ e.source)
inst✝ : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (↑e' '' (e'.source ∩ s))

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (↑e' '' (e'.source ∩ s))
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace X'
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace Y'
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace Z'
e✝ e e' : OpenPartialHomeomorph X Y
inst✝¹ : (x : X) → Decidable (x ∈ e.source)
inst✝ : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn ↑e ↑e' ∅

Tactic:
]

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace X'
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace Y'
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace Z'
e✝ e e' : OpenPartialHomeomorph X Y
inst✝¹ : (x : X) → Decidable (x ∈ e.source)
inst✝ : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn ↑e ↑e' ∅
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace X'
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace Y'
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace Z'
e✝ e e' : OpenPartialHomeomorph X Y
inst✝¹ : (x : X) → Decidable (x ∈ e.source)
inst✝ : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn ↑e ↑e' ∅

Tactic:
exact eqOn_empty _ _

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑x ∈ ↑s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑x ∈ ↑s
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ ↑(e.subtypeRestr hs) '' Subtype.val ⁻¹' e.source ⊆ ↑e '' e.source

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ ↑(e.subtypeRestr hs) '' Subtype.val ⁻¹' e.source ⊆ ↑e '' e.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ ↑e'.symm ⁻¹' e.source ∩ (e'.target ∩ ↑e'.symm ⁻¹' s) =
    ↑e'.symm ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ ↑e'.symm ⁻¹' s))

Tactic:
]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ ↑e'.symm ⁻¹' e.source ∩ (e'.target ∩ ↑e'.symm ⁻¹' s) =
    ↑e'.symm ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ ↑e'.symm ⁻¹' s))
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ e'.target ∩ ↑e'.symm ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ ↑e'.symm ⁻¹' s)

Tactic:
]

Goal state after:
case e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ e'.target ∩ ↑e'.symm ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ ↑e'.symm ⁻¹' s)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm).trans f'

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm).trans f'
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ e'.target ∩ ↑e'.symm ⁻¹' s = e'.target ∩ ↑e'.symm ⁻¹' s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen[inst✝¹] ↑s
⊢ f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s) openness₂)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen[inst✝¹] ↑s
⊢ f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s) openness₂)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e ((Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y) = y

pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e ((Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y) = y

X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ y = y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : ↑(e.subtypeRestr hU).symm y ∈ Subtype.val ⁻¹' e.source
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : ↑(e.subtypeRestr hU).symm y ∈ Subtype.val ⁻¹' e.source
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' ↑U
⊢ ↑e.symm y ∈ ↑V

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' ↑U
⊢ ↑e.symm y ∈ ↑V
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))

Tactic:
]

Goal state after:
case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑e.symm y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ ↑e x₀ ∈ e.target

Tactic:
]

Goal state after:
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ ↑e x₀ ∈ e.target
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ f (e.invFun (↑e x₀)) = f x₀

Tactic:
]

Goal state after:
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ f (e.invFun (↑e x₀)) = f x₀
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ ↑e x₀ = ↑e x₀

Tactic:
]

Goal state after: