mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
⊢ automorphize (g ∘ Quotient.mk' • f) = g • automorphize f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.RealVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_2
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousSMul ℝ F
inst✝² : T2Space F
G : Type u_3
inst✝¹ : FunLike G E F
inst✝ : AddMonoidHomClass G E F
f : G
hf : Continuous ⇑f
c : ℝ
x : E
⊢ Continuous fun c ↦ f (c • x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ r • s • x = s • r • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s) • x = r • s • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ MulOpposite.op r • x = r • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ (r * s) • x = r • s • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ 1 • x = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ r • 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ r • (x + y) = r • x + r • y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ (r + s) • x = r • x + s • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ 0 • r = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ (ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi } =
    { re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ r • x = (ofRealHom.comp (algebraMap R ℝ)) r * x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
r : ℝ
x : ℂ
⊢ star (r • x) = star r • star x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
⊢ Semiring.toNatAlgebra = instAlgebraOfReal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
⊢ Ring.toIntAlgebra ℂ = instAlgebraOfReal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
⊢ Module.restrictScalars ℝ ℂ ℂ = instModule

Tactic:
by

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
z z' : ℂ
⊢ ![(z + z').re, (z + z').im] = ![z.re, z.im] + ![z'.re, z'.im]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
c : ℝ
z : ℂ
⊢ ![(c • z).re, (c • z).im] = (RingHom.id ℝ) c • ![z.re, z.im]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
z : ℂ
⊢ (fun c ↦ ↑(c 0) + c 1 • I) ((fun z ↦ ![z.re, z.im]) z) = z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) = c

Tactic:
by

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

Goal state before:
pp: i j : Fin 2
⊢ (basisOneI.repr (![1, I] i)) j = (Finsupp.single i 1) j

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
inst : Algebra ℂ A
⊢ Algebra.toModule = Module.complexToReal A

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star (r • a) = star r • star a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (m : ℝ) (x : ℂ), (m • x).re = (RingHom.id ℝ) m • x.re

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (m : ℝ) (x : ℂ), (m • x).im = (RingHom.id ℝ) m • x.im

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✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = ↑r • x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ re 1 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ (LinearMap.toMatrix basisOneI basisOneI) ↑↑conjAe = !![1, 0; 0, -1]

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f I ^ 2 = I ^ 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (↑r * z) = r * re z

Tactic:
by

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

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe

Tactic:
by

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

Goal state before:
pp: r : ℝ
c : ℂ
⊢ equivRealProdAddHom.toFun (r • c) = (RingHom.id ℝ) r • equivRealProdAddHom.toFun c

Tactic:
by

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

Goal state before:
pp: z : ℂ
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
x : ℝ
h : r₁ < x ∧ x < r₂
⊢ r₁ < ‖↑x‖ ∧ ‖↑x‖ < r₂

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
r : ℝ
z : K
⊢ im (↑r * z) = r * im z

Tactic:
by

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

Goal state before:
pp: z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖₊ = ‖n‖₊

Tactic:
by

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

Goal state before:
pp: ⊢ Continuous ⇑normSq

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ im (z * ↑r) = im z * r

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (r • z) = r * re z

Tactic:
by

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

Goal state before:
pp: ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (r • z) = r * im z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : ℝ
n : ℕ
⊢ re (↑a ^ n) = a ^ n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : ℝ
n : ℕ
⊢ im (↑a ^ n) = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im I * im z = im 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 (I * z) = -im z

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
⊢ (starRingEnd K) ↑r = ↑r

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : ↑b = ∑ i ∈ s, ↑‖f i‖
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖equivRealProd 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) (↑(re z) + ↑(im z) * I) = ↑(re z) - ↑(im z) * I

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ LipschitzWith 1 ⇑equivRealProd

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 = ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I)

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ≤ ↑(NNReal.sqrt 2) * ‖equivRealProdLm z‖

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖reLm x‖ ≤ 1 * ‖x‖

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) + ↑(im z) * I - (↑(re z) - ↑(im z) * I) = 2 * ↑(im z) * I

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖imLm x‖ ≤ 1 * ‖x‖

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = reCLM.smulRight x + I • imCLM.smulRight x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = x • 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ (starRingEnd K) (r • z) = r • (starRingEnd K) z

Tactic:
by

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

Goal state before:
pp: z w : ℂ
⊢ dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)

Tactic:
by

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

Goal state before:
pp: f : ℂ →+* ℂ
hf : Continuous ⇑f
⊢ f = RingHom.id ℂ ∨ f = starRingEnd ℂ

Tactic:
by

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

Goal state before:
pp: ⊢ ↑↑conjCLE = conjAe.toLinearMap

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 = ↑(re z) + ↑(im z) * I + (↑(re z) - ↑(im z) * I)

Tactic:
by

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

Goal state before:
pp: f : ℝ →+* ℂ
h : Continuous ⇑f
⊢ f = ofRealHom

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ x.im = 0 ↔ IsSelfAdjoint x

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) + ↑(im z) * I + (↑(re z) - ↑(im z) * I) = 2 * ↑(re z)

Tactic:
by

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

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ x.re = 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
⊢ ↑(re z) = (z + (starRingEnd K) z) / 2

Tactic:
by

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

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = x.re ↔ ↑y = x

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x : 𝕜
⊢ (fun x ↦ ↑x.re + ↑x.im * RCLike.I) ((fun x ↦ ↑(RCLike.re x) + ↑(RCLike.im x) * I) x) = x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI') I = I'

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x : ℂ
⊢ (fun x ↦ ↑(RCLike.re x) + ↑(RCLike.im x) * I) ((fun x ↦ ↑x.re + ↑x.im * RCLike.I) 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
⊢ ↑(im z) = I * ((starRingEnd K) z - z) / 2

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ I ∈ {I}

Tactic:
by

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

Goal state before:
pp: ⊢ ℝ[I] = ⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ im z = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI').range = ℝ[I']

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re (x * y)) + ↑(RCLike.im (x * y)) * I =
    (↑(RCLike.re x) + ↑(RCLike.im x) * I) * (↑(RCLike.re y) + ↑(RCLike.im y) * I)

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re (x + y)) + ↑(RCLike.im (x + y)) * I =
    ↑(RCLike.re x) + ↑(RCLike.im x) * I + (↑(RCLike.re y) + ↑(RCLike.im y) * I)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ F I * F I = -1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
⊢ ↑(re z) = z

Tactic:
by

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

Goal state before:
pp: ⊢ I ∈ skewAdjoint ℂ

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
a : A
⊢ I • a ∈ skewAdjoint A ↔ IsSelfAdjoint a

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜' : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
h : RCLike.im RCLike.I = 1
a : 𝕜
⊢ 0 ≤ (RCLike.map 𝕜 𝕜') a ↔ 0 ≤ 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
a : A
⊢ IsSelfAdjoint (I • a) ↔ a ∈ skewAdjoint A

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝¹ : ℝ
x✝ : 𝕜
⊢ (RCLike.complexRingEquiv h).toFun (x✝¹ • x✝) = (RingHom.id ℝ) x✝¹ • (RCLike.complexRingEquiv h).toFun 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
a : ↥(skewAdjoint A)
⊢ -I • ↑a ∈ selfAdjoint A

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ 0 ≤
    ‖{ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝‖

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ 0 ≤ ‖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
a b : ↥(skewAdjoint A)
⊢ ⟨-I • ↑(a + b), ⋯⟩ = ⟨-I • ↑a, ⋯⟩ + ⟨-I • ↑b, ⋯⟩

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
x✝ : (starRingEnd K) z = z
⊢ IsSelfAdjoint 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
a : ℝ
b : ↥(skewAdjoint A)
⊢ ⟨-I • ↑(a • b), ⋯⟩ = (RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩

Tactic:
by

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ ‖{ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        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
a : ↥(skewAdjoint A)
⊢ I • ↑(negISMul a) = ↑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
a : A
⊢ ↑(ℜ a) = 2⁻¹ • (a + star 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
a : A
⊢ ↑(ℑ a) = -I • 2⁻¹ • (a - star 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
a : A
⊢ ↑(ℜ a) + I • ↑(ℑ a) = a

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
tfae_1_to_5 : (starRingEnd K) z = z → IsSelfAdjoint z
hz : IsSelfAdjoint z
⊢ (starRingEnd K) z = z

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

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
a : A
⊢ ℜ (I • a) = -ℑ a

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : 0 ≤ z
⊢ z = ↑‖z‖

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ x.re ↔ 0 ≤ 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
a : A
⊢ ℑ (I • a) = ℜ a

Tactic:
by

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

Goal state before:
pp: x y : ℂ
h : x ≤ y
⊢ x.re ≤ y.re

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
⊢ ?m.43

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, ∃ r, ↑r = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z].TFAE

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 : α → ℝ
x : ℝ
h : HasSum (fun x ↦ ↑(f x)) (↑x) L
⊢ HasSum f x L

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 : α → ℝ
h : Summable (fun x ↦ ↑(f x)) L
⊢ Summable f 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:
have := by congrm (ℜ ($((re_add_im z).symm) • a))

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
this : ℜ (z • a) = ℜ ((↑z.re + ↑z.im * I) • a)
⊢ ℜ (z • a) = z.re • ℜ a - z.im • ℑ a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (∃ r, ↑r = z) ↔ ∃ r, z = ↑r

Tactic:
by

Goal state after: