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

Goal state before:
pp: x y : ℝ
⊢ ↑(exp (x + y)) = ↑(exp x * exp y)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖toContinuousLinearMap
        (adjoint ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A) ∘ₗ
          (toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A)‖ =
    ‖A‖ * ‖A‖

Tactic:
exact ContinuousLinearMap.norm_adjoint_comp_self _

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ exp (↑n * x) = exp x ^ n

Tactic:
by

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

Goal state before:
pp: x : ℝ
z : ℤ
⊢ exp (↑z * x) = exp x ^ z

Tactic:
by

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

Goal state before:
pp: h : exp Real.pi = 1
⊢ ↑(exp Real.pi) = 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
by

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

Goal state before:
pp: ⊢ exp Real.pi ≠ 1

Tactic:
by

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

Goal state before:
pp: e : AddChar ℝ Circle
x : ℝ
⊢ star ↑(e x) = ↑(e (-x))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ Circle.exp (2 * π * 0) = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: ⊢ 𝐞 ≠ 1

Tactic:
by

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

Goal state before:
pp: ⊢ probChar ≠ 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
⊢ ‖A * B‖ ≤ ‖A‖ * ‖B‖

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' F x' (cast ⋯ b) = { proj := x, snd := b }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
y y' : E b
⊢ mk' F b y = mk' F b y' ↔ y = y'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) = proj ⁻¹' {b}

Tactic:
by

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

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
e' : OpenPartialHomeomorph Y Z
⊢ (e.symm.restrOpen e'.source ⋯).symm.target = (e'.restrOpen e.target ⋯).source

Tactic:
by

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.trans (ofSet s hs)).source = (e.restr (↑e ⁻¹' s)).source

Tactic:
by

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.trans (ofSet s hs) = e.restr (e.source ∩ ↑e ⁻¹' s)

Tactic:
by

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
⊢ ((ofSet s hs).trans e).source = (e.restr s).source

Tactic:
by

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
⊢ (ofSet s hs).trans e = e.restr (e.source ∩ s)

Tactic:
by

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).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯

Tactic:
by

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)
x : EuclideanSpace 𝕜 n
⊢ 0 ≤ ‖T x‖

Tactic:
by

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)
x : EuclideanSpace 𝕜 n
⊢ 0 ≤ ‖v‖ * ‖x‖

Tactic:
by

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)
x : EuclideanSpace 𝕜 n
i : n
x✝ : i ∈ Finset.univ
⊢ (‖v i‖ * ‖x.ofLp i‖) ^ 2 ≤ ?m.78 i

Tactic:
by

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)
x : EuclideanSpace 𝕜 n
⊢ ∑ i, ‖v‖ ^ 2 * ‖x.ofLp i‖ ^ 2 = (‖v‖ * ‖x‖) ^ 2

Tactic:
by

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‖ = ‖T (toLp 2 (Pi.single i 1))‖

Tactic:
by

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
⊢ ‖T (toLp 2 (Pi.single i 1))‖ ≤ ‖T‖

Tactic:
by

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 → 𝕜
⊢ ‖diagonal v‖ = ‖v‖

Tactic:
by

Goal state after:
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 • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by

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
a : X
b : Y
ha : IsOpen[inst✝⁵] {a}
hb : IsOpen[inst✝³] {b}
⊢ ContinuousOn (↑(PartialEquiv.single a b)) (PartialEquiv.single a b).source

Tactic:
by

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
a : X
b : Y
ha : IsOpen[inst✝⁵] {a}
hb : IsOpen[inst✝³] {b}
⊢ ContinuousOn (PartialEquiv.single a b).invFun (PartialEquiv.single a b).target

Tactic:
by

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.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
by

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.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
by

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'
e f : OpenPartialHomeomorph X Y
e' f' : OpenPartialHomeomorph X' Y'
⊢ (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f')

Tactic:
by

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
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source

Tactic:
e.open_source.inter_frontier_eq,

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
⊢ ∅ = e'.source ∩ frontier e.source
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
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (↑e '' s)

Tactic:
by

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
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source

Tactic:
by

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'.target ∩ ↑e'.symm ⁻¹' s)

Tactic:
by

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
⊢ EqOn (↑e) (↑e') (e.source ∩ frontier e.source)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
f' : Y ≃ₜ Z
f'' : Z ≃ₜ Z'
⊢ (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
e' : OpenPartialHomeomorph Y Z
f'' : Z ≃ₜ Z'
⊢ (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

Tactic:
by

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
⊢ (e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source

Tactic:
by

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
⊢ ↑e ↑x ∈ (e.subtypeRestr hs).target

Tactic:
by

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
⊢ (e.subtypeRestr hs).target ⊆ e.target

Tactic:
by

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)
⊢ f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s

Tactic:
by

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
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
f : OpenPartialHomeomorph Y Z
f' : OpenPartialHomeomorph Z Z'
⊢ (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f')

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
e' : Y ≃ₜ Z
f'' : OpenPartialHomeomorph Z Z'
⊢ (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')

Tactic:
by

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
⊢ (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Tactic:
by

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
⊢ ↑(e.subtypeRestr hU) (↑(e.subtypeRestr hU).symm y) = y

Tactic:
(e.subtypeRestr hU).right_inv hy

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
⊢ y = y
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
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y = ↑e.symm y

Tactic:
by

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 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
⊢ ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target

Tactic:
by

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 V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
⊢ EqOn (↑(e.subtypeRestr hV).symm) (inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

Tactic:
by

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 ∈ f '' e.source → extend f (↑e) (fun x ↦ Classical.arbitrary Z) x ∈ e.target

Tactic:
by

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 ∈ f '' e.source → (f ∘ e.invFun) (extend f (↑e) (fun x ↦ Classical.arbitrary Z) x) = x

Tactic:
by

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
z : Z
hz : z ∈ e.target
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) ((f ∘ e.invFun) z) = z

Tactic:
by

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
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
⊢ EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)

Tactic:
by

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
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
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ ContinuousOn (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)

Tactic:
by

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
⊢ ContinuousOn (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source)

Tactic:
by

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

Goal state before:
pp: 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
⊢ ↑(e.lift_openEmbedding hf) (f x) = ↑e x

Tactic:
by

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

Goal state before:
pp: 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
⊢ (e.lift_openEmbedding hf).symm.target = f '' e.source

Tactic:
by

Goal state after: