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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x✝ : ℝ
⊢ re ((algebraMap ℝ 𝕜) 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
y : ℝ
hx : IsSelfAdjoint x
⊢ re 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 : K
y : ℝ
hx : IsSelfAdjoint x
⊢ y = re x ↔ ↑y = x

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
z : ℂ
a : A
⊢ ℜ (z • a) = z.re • ℜ a - z.im • ℑ a

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
⊢ re 0 * re 0 + im 0 * im 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 : K
⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
by

Goal state after:
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
z : ℂ
a : A
⊢ ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Tactic:
by

Goal state after:
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
x : A
⊢ ↑((skewAdjointPart ℝ) x) = I • ↑(ℑ x)

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ z ∈ slitPlane ∨ -z ∈ slitPlane

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
x : A
hx : IsSelfAdjoint x
⊢ ℑ x = 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 w : K
⊢ re (z * w) * re (z * w) + im (z * w) * im (z * w) = (re z * re z + im z * im z) * (re w * re w + im w * im w)

Tactic:
by

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

Goal state before:
pp: ⊢ Metric.ball 1 1 ⊆ slitPlane

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ 1 + z ∈ Metric.ball 1 1

Tactic:
by

Goal state after:
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
⊢ ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0

Tactic:
by

Goal state after:
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
x : ↥(selfAdjoint A)
⊢ ↑(ℑ (I • ↑x)) = ↑x

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ s ⊆ slitPlane ↔ -↑r ∉ s

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
x y : A
h₁ : ℜ x = ℜ y
h₂ : ℑ 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
z : K
⊢ normSq (-z) = normSq z

Tactic:
by

Goal state after:
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
x y : A
⊢ 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
z : K
⊢ normSq ((starRingEnd K) z) = normSq z

Tactic:
by

Goal state after:
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
B : Type u_2
F : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module ℂ B
inst✝⁴ : StarAddMonoid B
inst✝³ : StarModule ℂ B
inst✝² : FunLike F A B
inst✝¹ : StarHomClass F A B
inst✝ : LinearMapClass F ℂ A B
f : F
x : A
⊢ f ↑(ℜ x) = ↑(ℜ (f x))

Tactic:
by

Goal state after:
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
B : Type u_2
F : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module ℂ B
inst✝⁴ : StarAddMonoid B
inst✝³ : StarModule ℂ B
inst✝² : FunLike F A B
inst✝¹ : StarHomClass F A B
inst✝ : LinearMapClass F ℂ A B
f : F
x : A
⊢ f ↑(ℑ x) = ↑(ℑ (f x))

Tactic:
by

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
⊢ ‖x‖ + ‖star x‖ ≤ 2 * ‖x‖

Tactic:
by

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 x‖ ≤ ‖x‖

Tactic:
by

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
⊢ ‖imaginaryPart x‖ = ‖realPart (Complex.I • -x)‖

Tactic:
by

Goal state after:
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
⊢ ℑ.ker = selfAdjoint.submodule ℝ A

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ normSq (z + w) = normSq z + normSq w + 2 * re (z * (starRingEnd K) w)

Tactic:
by

Goal state after:
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
x : A
⊢ ℑ x = 0 ↔ IsSelfAdjoint x

Tactic:
by

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

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
⊢ ‖imaginaryPart x‖ ≤ ‖x‖

Tactic:
by

Goal state after:
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
⊢ span ℂ ↑(selfAdjoint A) = ⊤

Tactic:
refine eq_top_iff'.mpr fun x ↦ ?_
  rw [← realPart_add_I_smul_imaginaryPart x]
  exact add_mem (subset_span (ℜ x).property) <|
    SMulMemClass.smul_mem _ <| subset_span (ℑ x).property

Goal state after:
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
⊢ span ℂ ↑(selfAdjoint A) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
⊢ ∀ (x y : ↥(selfAdjoint ℂ)), (↑(x + y)).re = (↑x).re + (↑y).re

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
⊢ ∀ (m : ℝ) (x : ↥(selfAdjoint ℂ)), (↑(m • x)).re = (RingHom.id ℝ) m • (↑x).re

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z * (starRingEnd K) z = ↑‖z‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ ↑(ℜ ↑r) = ↑r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ ℑ ↑r = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) z * z = ↑‖z‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: z : ℂ
⊢ ↑(ℜ z) = ↑z.re

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : ‖z‖ = 1
⊢ (starRingEnd K) z * z = 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
⊢ normSq (z - w) = normSq z + normSq w - 2 * re (z * (starRingEnd K) w)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ √(normSq z) = ‖z‖

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) + (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) =
    2 • (↑(ℜ a) * ↑(ℜ a) + ↑(ℑ a) * ↑(ℑ a))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * re ((starRingEnd K) z) = re z / ‖z‖ ^ 2

Tactic:
conj_re,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * re z = re z / ‖z‖ ^ 2
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) - (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) =
    2 • I • (↑(ℜ a) * ↑(ℑ a) - ↑(ℑ a) * ↑(ℜ a))

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⁻¹ = re z / normSq z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z⁻¹ = -im z / normSq z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ re (z / w) = re z * re w / normSq w + im z * im w / normSq w

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ im (z / w) = im z * re w / normSq w - re z * im w / normSq w

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ ‖1‖ = 1 ∧ ↑‖0‖ = 1 * 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖↑‖x‖ / x‖ = 1 ∧ ↑‖x‖ = ↑‖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
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ IsStarNormal x ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ ‖1‖ = 1 ∧ 1 * ↑‖0‖ = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖x / ↑‖x‖‖ = 1 ∧ x / ↑‖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
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖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
r : ℝ
⊢ re (z / ↑r) = re z / r

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ I⁻¹ = -I

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z / I = -(z * I)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ star x * x = ↑(ℜ x) * ↑(ℜ x) + ↑(ℑ x) * ↑(ℑ x) + I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ 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
⊢ ‖(starRingEnd K) 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
⊢ ‖(starRingEnd K) 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
⊢ ‖(starRingEnd K) z‖ₑ = ‖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 : K
r : ℝ
a : K
⊢ star (r • a) = star r • star a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ re ↑n = ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ im ↑n = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ re (OfNat.ofNat n * z) = OfNat.ofNat n * re z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ im (OfNat.ofNat n * z) = OfNat.ofNat n * im z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑n = ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ im ↑n = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ re ↑q = ↑q

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ ↑(ℜ x) * ↑(ℜ x) + ↑(ℑ x) * ↑(ℑ x) + I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = ↑(ℜ x) * ↑(ℜ x) + ↑(ℑ x) * ↑(ℑ x)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ im ↑q = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ re ↑q = ↑q

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ im ↑q = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ re (ofScientific m s e) = ofScientific m s e

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ im (ofScientific m s e) = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖₊ = ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑q‖ = ↑q

Tactic:
by

Goal state after:
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
⊢ 0 ≤ a ↔ 0 ≤ ℜ a ∧ ℑ a = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

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✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖ = n • ‖x‖

Tactic:
by

Goal state after:
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:
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✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖₊ = n • ‖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‖ * ‖z‖ = normSq z

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
⊢ ℜ 1 = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| ≤ ‖z‖

Tactic:
by

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

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
x✝ : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
this : IsStarNormal x
⊢ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ ↑(re a) = a

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‖| ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ unitary A ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z / ‖z‖| ≤ 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star x) = star (φ x)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ ‖I‖ = if I = 0 then 0 else 1

Tactic:
by

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

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

Tactic:
by

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

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

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
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ e.source

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

Tactic:
by

Goal state after: