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

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 : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
⊢ Continuous[inst✝³, inst✝⁵] ↑e.symm

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ ∀ (x : ↑e.source), e.source.domRestrict (↑e.toPartialEquiv) x ∈ e.target

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖(starRingEnd K) x + x‖ ^ 2 = re ((starRingEnd K) x + x) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ range Subtype.val ⊆ e.source

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsEmbedding (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
f : CauSeq K norm
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ re (↑f n)) j - (fun n ↦ re (↑f n)) i| ≤ ‖↑f j - ↑f i‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

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 : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ∀ (a : ↑f.source), f.source.domRestrict (↑f) a ∈ f.target

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

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 : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ContinuousOn (↑f) f.source

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
f : CauSeq K norm
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ im (↑f n)) j - (fun n ↦ im (↑f n)) i| ≤ ‖↑f j - ↑f i‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

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 : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ∀ (a : ↑f.target), f.target.domRestrict f.invFun a ∈ f.source

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ I ∈ skewAdjoint K

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
⊢ (AddMonoidHom.id ℝ) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : ℝ
⊢ (algebraMap ℝ ℝ) ((AddMonoidHom.id ℝ) z) + (algebraMap ℝ ℝ) (0 z) * 0 = z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

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 : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ContinuousOn f.invFun f.target

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z w : ℝ
⊢ (AddMonoidHom.id ℝ) (z * w) = (AddMonoidHom.id ℝ) z * (AddMonoidHom.id ℝ) w - 0 z * 0 w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z w : ℝ
⊢ 0 (z * w) = (AddMonoidHom.id ℝ) z * 0 w + 0 z * (AddMonoidHom.id ℝ) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : ℝ
⊢ (AddMonoidHom.id ℝ) ((starRingEnd ℝ) z) = (AddMonoidHom.id ℝ) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x✝ : ℝ
⊢ 0 ((starRingEnd ℝ) x✝) = -0 x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
⊢ (starRingEnd ℝ) 0 = -0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : ℝ
⊢ ‖z‖ ^ 2 = (AddMonoidHom.id ℝ) z * (AddMonoidHom.id ℝ) z + 0 z * 0 z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : ℝ
⊢ ‖z‖ ^ 2 = (AddMonoidHom.id ℝ) z * (AddMonoidHom.id ℝ) z + 0 z * 0 z

Tactic:
by simp only [sq, Real.norm_eq_abs, ← abs_mul, abs_mul_self z, add_zero,
    mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x✝ : ℝ
⊢ 0 x✝ * 0 0 = 0 x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖ = q • ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖₊ = q • ‖x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

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'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsHomeomorph ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x✝¹ : ℕ
x✝ : E
⊢ ‖(↑x✝¹)⁻¹ • x✝‖ = (↑x✝¹)⁻¹ • ‖x✝‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toPartialHomeomorph f h).symm (f x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toPartialHomeomorph f h).symm x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : Nonempty ↑s
⊢ (s.partialHomeomorphSubtypeCoe hs).target = s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ z < w ↔ re z < re w ∧ im z = im w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ 0 ≤ re z ∧ im z = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ 0 < re z ∧ im z = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ re z < 0 ∧ im z = 0

Tactic:
by

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

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
hse : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
⊢ IsOpen[inst✝¹] (↑e.symm '' t) ↔ IsOpen[inst✝] t

Tactic:
by

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

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 : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s) ↔ IsOpen[inst✝¹] s

Tactic:
by

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

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 : PartialEquiv X Y
hc : ContinuousOn (↑e) e.source
ho : IsOpenMap (e.source.domRestrict ↑e)
hs : IsOpen[inst✝⁵] e.source
⊢ IsOpen[inst✝³] (PartialHomeomorph.ofContinuousOpenRestrict e hc ho).target

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] (range (e.source.domRestrict ↑e))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toOpenPartialHomeomorph f h).symm (f x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, ↑x = z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toOpenPartialHomeomorph f h).symm x) = x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Opens X
hs : Nonempty ↥s
⊢ (s.openPartialHomeomorphSubtypeCoe hs).target = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ 0 ≤ ↑x ↔ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ ↑x ≤ 0 ↔ x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ 0 < ↑x ↔ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ ↑x < 0 ↔ x < 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' ∈ {x}

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ Tendsto (↑e.symm) (𝓝 (↑e x)) (𝓝 x)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 (↑e.symm (↑e x)) = 𝓝 x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ map (↑e) (𝓝[↑e ⁻¹' s] x) = 𝓝[s] ↑e x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝 (↑e x), p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝 x), p b

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝 (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p (↑e x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ ≤ re z ↔ z = ↑‖z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z ≤ -‖z‖ ↔ z = -↑‖z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : IsSelfAdjoint x
⊢ 0 ≤ re x ↔ 0 ≤ x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
h : x ≤ y
⊢ re x ≤ re y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z⁻¹ ↔ 0 < z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
h : 0 ≤ re x ∧ im x = 0
⊢ x = star ↑√(re x) * ↑√(re x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ x ↔ ∃ s, x = star s * s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
hz : 0 < z
hw : 0 < w
⊢ 0 < z * w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
y z : K
r : ℝ
hx : 0 ≤ re ↑r ∧ im ↑r = 0
hyz : r * re y < r * re z ∧ (im y = im z ∨ r = 0)
⊢ 0 ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Contravariant { x // 0 ≤ x } K (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
hr : 0 < r
a b : K
hab : a < b
⊢ r • a < r • b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
ha : 0 < a
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ r₁ • a < r₂ • a

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < ↑x * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ 0 < ↑x * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z

Tactic:
by
  simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]
  obtain hx | hx | hx := lt_trichotomy x 0
  · simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne,
      or_false]
  · simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]
  · simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,
      hx.ne', false_or]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ ↑x * z < 0 ↔ x < 0 ∧ 0 < z ∨ 0 < x ∧ z < 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
y : Z
hy : y ∈ s ∩ f ⁻¹' e.source
⊢ f y = (↑e.symm ∘ ↑e ∘ f) y

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ f x = (↑e.symm ∘ ↑e ∘ f) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: x : ℝ
⊢ normSq x = x * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖reLm x‖ ≤ 1 * ‖x‖

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖imLm x‖ ≤ 1 * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re x - re y‖ₑ = ‖re (x - y)‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x

Tactic:
by

Goal state after: