mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
h : (-f).NormNoninc
x : V₁
⊢ ‖f x‖ ≤ ‖x‖

Tactic:
simpa using

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
h : (-f).NormNoninc
x : V₁
⊢ ‖f x‖ ≤ ‖x‖
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ (fun x ↦ x ^ 2) x ≤ (fun x ↦ x ^ 2) y

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ x * x ≤ y * y
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : StarMul A
a : A
U : ↥(unitary A)
⊢ spectrum R (star ↑U * a * ↑U) = spectrum R a

Tactic:
simpa using

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : StarMul A
a : A
U : ↥(unitary A)
⊢ spectrum R (star ↑U * a * ↑U) = spectrum R a
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
A : E
U : ↥(unitary E)
⊢ ‖A * ↑U‖ = ‖A‖

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
A : E
U : ↥(unitary E)
⊢ ‖(↑U)⋆ * A⋆‖ = ‖A‖
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ a * ‖f.symm y‖ = ‖y‖
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun b ↦ e (f b)) y L
⊢ HasSum f (e.symm y) L

Tactic:
simpa using

Goal state after:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun b ↦ e (f b)) y L
⊢ HasSum f (e.symm y) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (e.symm y) L
⊢ HasSum (fun b ↦ e (f b)) y L

Tactic:
simpa using

Goal state after:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (e.symm y) L
⊢ HasSum (fun b ↦ e (f b)) y L
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
simp only [tsum_bot hL, eq_symm_apply]

Goal state after:
case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑ᶠ (z : ι), e (f z) = y ↔ e (∑ᶠ (z : ι), f z) = y
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg.refine_2
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y

Tactic:
simpa using

Goal state after:
case neg.refine_2
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ Continuous ⇑normSq

Tactic:
simpa using

Goal state after:
⊢ Continuous ⇑normSq
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
h : I * I = -1
⊢ im I = 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
h : I * I = -1
⊢ im I = 1
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ ‖equivRealProd z‖ ≤ 1 * ‖z‖

Tactic:
simpa using

Goal state after:
z : ℂ
⊢ |z.re| ≤ ‖z‖ ∧ |z.im| ≤ ‖z‖
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ Tendsto (⇑normSq) (cocompact ℂ) atTop

Tactic:
simpa using

Goal state after:
⊢ Tendsto (⇑normSq) (cocompact ℂ) atTop
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ↥(skewAdjoint A)
⊢ -I • ↑a ∈ selfAdjoint A

Tactic:
simp [selfAdjoint.mem_iff]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x : ℝ
h : HasSum (fun x ↦ ↑(f x)) (↑x) L
⊢ HasSum f x L

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x : ℝ
h : HasSum (fun x ↦ ↑(f x)) (↑x) L
⊢ HasSum f x L
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
h : Summable (fun x ↦ ↑(f x)) L
⊢ Summable f L

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
h : Summable (fun x ↦ ↑(f x)) L
⊢ Summable f L
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
y : ℝ
hx : IsSelfAdjoint x
⊢ y = re x ↔ ↑y = x

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
y : ℝ
hx : IsSelfAdjoint x
⊢ y = re x ↔ x = ↑y
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x ↦ re (f x)) (re c) L
h₂ : HasSum (fun x ↦ im (f x)) (im c) L
⊢ HasSum f c L

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x ↦ re (f x)) (re c) L
h₂ : HasSum (fun x ↦ im (f x)) (im c) L
⊢ HasSum f c L
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℝ
⊢ -↑x ∈ slitPlane ↔ x < 0

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ -↑x ∈ slitPlane ↔ x < 0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n ∈ slitPlane ↔ n ≠ 0

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ ↑n ∈ slitPlane ↔ ¬n = 0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
hz : z ∈ Metric.ball 1 1
⊢ 0 < z.re

Tactic:
simpa using

Goal state after:
z : ℂ
hz : z ∈ Metric.ball 1 1
⊢ 0 < z.re
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
hr : -↑r ∈ s
⊢ -↑r ≤ 0

Tactic:
simpa using

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
hr : -↑r ∈ s
⊢ 0 ≤ r
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
⊢ ‖z‖ = r

Tactic:
simpa using

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
⊢ ‖z‖ = r
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖x‖ + ‖star x‖ ≤ 2 * ‖x‖

Tactic:
by simp [two_mul]

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖realPart (Complex.I • -x)‖ ≤ ‖x‖

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖imaginaryPart x‖ ≤ ‖x‖
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: z : ↥(selfAdjoint ℂ)
⊢ ↑(selfAdjointEquiv z) = ↑z

Tactic:
simpa using

Goal state after:
z : ↥(selfAdjoint ℂ)
⊢ ↑(↑z).re = ↑z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖ = n • ‖x‖

Tactic:
simpa using

Goal state after:
K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖ = ↑n * ‖x‖
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
⊢ a ≤ 0 ↔ ℜ a ≤ 0 ∧ ℑ a = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
⊢ a ≤ 0 ↔ ℜ a ≤ 0 ∧ IsSelfAdjoint a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖₊ = n • ‖x‖₊

Tactic:
simpa using

Goal state after:
K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖₊ = ↑n * ‖x‖₊
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a b : A
⊢ a ≤ b ↔ ℜ a ≤ ℜ b ∧ ℑ a = ℑ b

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a b : A
⊢ a ≤ b ↔ ℜ a ≤ ℜ b ∧ ℑ b = ℑ a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ im a = 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ im a = 0
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

Tactic:
simpa using

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

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

Goal state after:
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
⊢ |re (↑f j) - re (↑f i)| ≤ ‖↑f j - ↑f i‖
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:
simpa using

Goal state after:
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
⊢ |im (↑f j) - im (↑f i)| ≤ ‖↑f j - ↑f i‖
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:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ 0 ≤ re z ∧ 0 = im z
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:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ 0 < re z ∧ 0 = im z
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:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0
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:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ re z < 0 ∧ im z = 0
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:
simpa only [map_zero] using lt_iff_re_im (z := z) (w := 0)

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

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

Goal state after:
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)
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z ≤ -‖z‖ ↔ z = -↑‖z‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re x ≤ re y ∧ im x = im y
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
simp [@RCLike.le_iff_re_im K]

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

Goal state after:
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
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:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
hr : 0 < r
a b : K
hab : a < b
⊢ re a < re b ∧ im a = im b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : 0 < x
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Tactic:
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:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ ↑x * z < 0 ↔ x < 0 ∧ 0 < z ∨ 0 < x ∧ z < 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z ≤ -‖z‖ ↔ z = -(I * ↑‖z‖)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z ≤ -‖z‖ ↔ z = -(I * ↑‖z‖)
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹
⊢ f =Θ[l] g

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹
⊢ f =Θ[l] g
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ (fun x ↦ f₁ x * (f₂ x)⁻¹) =Θ[l] fun x ↦ g₁ x * (g₂ x)⁻¹
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.ofNat a✝) =Θ[l] fun x ↦ g x ^ Int.ofNat a✝

Tactic:
simpa using

Goal state after:
case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ a✝) =Θ[l] fun x ↦ g x ^ a✝
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.negSucc a✝) =Θ[l] fun x ↦ g x ^ Int.negSucc a✝

Tactic:
simpa using

Goal state after:
case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ (f x ^ (a✝ + 1))⁻¹) =Θ[l] fun x ↦ (g x ^ (a✝ + 1))⁻¹
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
c₁ : E''
c₂ : F''
⊢ ((fun x ↦ c₁) =Θ[l] fun x ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Tactic:
simpa using

Goal state after:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
c₁ : E''
c₂ : F''
⊢ (c₂ = 0 ↔ c₁ = 0) ↔ (c₁ = 0 ↔ c₂ = 0)