[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
case a
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).re = (s • r • x).re
[PROOFSTEP]
simp [smul_re, smul_im, smul_comm]
[GOAL]
case a
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).im = (s • r • x).im
[PROOFSTEP]
simp [smul_re, smul_im, smul_comm]
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
case a
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).re = (r • s • x).re
[PROOFSTEP]
simp [smul_re, smul_im, smul_assoc]
[GOAL]
case a
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).im = (r • s • x).im
[PROOFSTEP]
simp [smul_re, smul_im, smul_assoc]
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).re = (r • x).re
[PROOFSTEP]
simp [smul_re, smul_im, op_smul_eq_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).im = (r • x).im
[PROOFSTEP]
simp [smul_re, smul_im, op_smul_eq_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ 1 • x = x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).re = x.re
[PROOFSTEP]
simp [smul_re, smul_im, one_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).im = x.im
[PROOFSTEP]
simp [smul_re, smul_im, one_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ (r * s) • x = r • s • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).re = (r • s • x).re
[PROOFSTEP]
simp [smul_re, smul_im, mul_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).im = (r • s • x).im
[PROOFSTEP]
simp [smul_re, smul_im, mul_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ r • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im, smul_zero]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im, smul_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ r • (x + y) = r • x + r • y
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).re = (r • x + r • y).re
[PROOFSTEP]
simp [smul_re, smul_im, smul_add]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).im = (r • x + r • y).im
[PROOFSTEP]
simp [smul_re, smul_im, smul_add]
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).re = (r • x + s • x).re
[PROOFSTEP]
simp [smul_re, smul_im, add_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).im = (r • x + s • x).im
[PROOFSTEP]
simp [smul_re, smul_im, add_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ 0 • r = 0
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im, zero_smul]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im, zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x✝ : (fun x => ℂ) r
xr xi : ℝ
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      { re := xr, im := xi } =
    { re := xr, im := xi } *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x✝ : (fun x => ℂ) r
xr xi : ℝ
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        { re := xr, im := xi }).re =
    ({ re := xr, im := xi } *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r).re
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.commutes]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x✝ : (fun x => ℂ) r
xr xi : ℝ
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        { re := xr, im := xi }).im =
    ({ re := xr, im := xi } *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r).im
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.commutes]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x : (fun x => ℂ) r
⊢ r • x =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x : (fun x => ℂ) r
⊢ (r • x).re =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x).re
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.smul_def]
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
src✝ : R →+* ℂ := RingHom.comp ofReal (algebraMap R ℝ)
r : R
x : (fun x => ℂ) r
⊢ (r • x).im =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          r *
        x).im
[PROOFSTEP]
simp [smul_re, smul_im, Algebra.smul_def]
[GOAL]
R : Type u_1
S : Type u_2
r : ℝ
x : ℂ
⊢ star (r • x) = star r • star x
[PROOFSTEP]
simp only [star_def, star_trivial, real_smul, map_mul, conj_ofReal]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
⊢ f = g
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case H.mk
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
x y : ℝ
⊢ ↑f { re := x, im := y } = ↑g { re := x, im := y }
[PROOFSTEP]
simp only [mk_eq_add_mul_I, AlgHom.map_add, AlgHom.map_coe_real_complex, AlgHom.map_mul, h]
[GOAL]
R : Type u_1
S : Type u_2
z z' : ℂ
⊢ (fun z => ![z.re, z.im]) (z + z') = (fun z => ![z.re, z.im]) z + (fun z => ![z.re, z.im]) z'
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
c : ℝ
z : ℂ
⊢ AddHom.toFun
      { toFun := fun z => ![z.re, z.im],
        map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) }
      (c • z) =
    ↑(RingHom.id ℝ) c •
      AddHom.toFun
        { toFun := fun z => ![z.re, z.im],
          map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) }
        z
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
z : ℂ
⊢ (fun c => ↑(c 0) + c 1 • I)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun z => ![z.re, z.im],
                map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
            map_smul' :=
              (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
        z) =
    z
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) =
    c
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
i : Fin 2
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) i =
    c i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.head
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) { val := 0, isLt := (_ : 0 < 2) } =
    c { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case h.tail.head
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => ![z.re, z.im],
              map_add' := (_ : ∀ (z z' : ℂ), ![z.re + z'.re, z.im + z'.im] = ![z.re, z.im] + ![z'.re, z'.im]) },
          map_smul' :=
            (_ : ∀ (c : ℝ) (z : ℂ), ![c * z.re - 0 * z.im, c * z.im + 0 * z.re] = c • ![z.re, z.im]) }.toAddHom
      ((fun c => ↑(c 0) + c 1 • I) c) { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    c { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
i j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] i)) j = ↑(Finsupp.single i 1) j
[PROOFSTEP]
fin_cases i
[GOAL]
case head
R : Type u_1
S : Type u_2
j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) })) j =
    ↑(Finsupp.single { val := 0, isLt := (_ : 0 < 2) } 1) j
[PROOFSTEP]
fin_cases j
[GOAL]
case tail.head
R : Type u_1
S : Type u_2
j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) })) j =
    ↑(Finsupp.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) j
[PROOFSTEP]
fin_cases j
[GOAL]
case head.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) })) { val := 0, isLt := (_ : 0 < 2) } =
    ↑(Finsupp.single { val := 0, isLt := (_ : 0 < 2) } 1) { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
case head.tail.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }))
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(Finsupp.single { val := 0, isLt := (_ : 0 < 2) } 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
case tail.head.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }))
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑(Finsupp.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
case tail.head.tail.head
R : Type u_1
S : Type u_2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }))
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(Finsupp.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re, Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same,
  Fin.zero_eq_one_iff]
[GOAL]
R : Type u_1
S : Type u_2
⊢ finrank ℝ ℂ = 2
[PROOFSTEP]
rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]
[GOAL]
R : Type u_1
S : Type u_2
⊢ Module.rank ℝ ℂ = 2
[PROOFSTEP]
simp [← finrank_eq_rank, finrank_real_complex]
[GOAL]
R : Type u_1
S : Type u_2
⊢ Cardinal.lift (Module.rank ℝ ℂ) = 2
[PROOFSTEP]
rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]
[GOAL]
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift (Module.rank ℝ E) = Cardinal.lift (2 * Module.rank ℂ E)
[PROOFSTEP]
rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']
[GOAL]
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ 2 * Cardinal.lift (Module.rank ℂ E) = Cardinal.lift (2 * Module.rank ℂ E)
[PROOFSTEP]
simp only [Cardinal.lift_id']
[GOAL]
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ FiniteDimensional.finrank ℝ E = 2 * FiniteDimensional.finrank ℂ E
[PROOFSTEP]
rw [← FiniteDimensional.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]
[GOAL]
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
[PROOFSTEP]
rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
[GOAL]
⊢ ∀ (r : ℝ) (x : ℂ),
    AddHom.toFun { toFun := fun x => x.re, map_add' := add_re } (r • x) =
      ↑(RingHom.id ℝ) r • AddHom.toFun { toFun := fun x => x.re, map_add' := add_re } x
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (r : ℝ) (x : ℂ),
    AddHom.toFun { toFun := fun x => x.im, map_add' := add_im } (r • x) =
      ↑(RingHom.id ℝ) r • AddHom.toFun { toFun := fun x => x.im, map_add' := add_im } x
[PROOFSTEP]
simp
[GOAL]
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) = ↑Matrix.of ![![1, 0], ![0, -1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) i j = ↑Matrix.of ![![1, 0], ![0, -1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 0, isLt := (_ : 0 < 2) } j =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      j =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 0, isLt := (_ : 0 < 2) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h.head.tail.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h.tail.head.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h.tail.head.tail.head
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (AlgEquiv.toLinearMap conjAe) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑Matrix.of ![![1, 0], ![0, -1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe
[PROOFSTEP]
refine' (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp _ _
[GOAL]
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I ^ 2 = I ^ 2
[PROOFSTEP]
rw [← map_pow, I_sq, map_neg, map_one]
[GOAL]
case refine'_1
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I = I → f = AlgHom.id ℝ ℂ
[PROOFSTEP]
refine' fun h => algHom_ext _
[GOAL]
case refine'_2
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I = -I → f = ↑conjAe
[PROOFSTEP]
refine' fun h => algHom_ext _
[GOAL]
case refine'_1
f : ℂ →ₐ[ℝ] ℂ
h : ↑f I = I
⊢ ↑f I = ↑(AlgHom.id ℝ ℂ) I
case refine'_2 f : ℂ →ₐ[ℝ] ℂ h : ↑f I = -I ⊢ ↑f I = ↑↑conjAe I
[PROOFSTEP]
exacts [h, conj_I.symm ▸ h]
[GOAL]
src✝ : ℂ ≃ ℝ × ℝ := equivRealProd
⊢ ∀ (x y : ℂ),
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (x + y) =
      Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          x +
        Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          y
[PROOFSTEP]
simp
[GOAL]
src✝ : ℂ ≃+ ℝ × ℝ := equivRealProdAddHom
r : ℝ
c : ℂ
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : ℂ), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • c) =
    ↑(RingHom.id ℝ) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ℂ), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        c
[PROOFSTEP]
simp [equivRealProdAddHom, (Prod.smul_def), smul_eq_mul]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ ↑(algebraMap ℝ A) 1 + 0 • I' = 1
[PROOFSTEP]
rw [RingHom.map_one, zero_smul, add_zero]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (↑(algebraMap ℝ A) x₁ + y₁ • I') * (↑(algebraMap ℝ A) x₂ + y₂ • I')
[PROOFSTEP]
rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    ↑(algebraMap ℝ A) x₁ * ↑(algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I' +
      (↑(algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * ↑(algebraMap ℝ A) x₂)
[PROOFSTEP]
congr 1
  -- equate "real" and "imaginary" parts
[GOAL]
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = ↑(algebraMap ℝ A) x₁ * ↑(algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'
[PROOFSTEP]
let inst : SMulCommClass ℝ A A := by
  infer_instance
    -- porting note: added
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ SMulCommClass ℝ A A
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
inst : SMulCommClass ℝ A A := inferInstance
⊢ ↑(algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = ↑(algebraMap ℝ A) x₁ * ↑(algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'
[PROOFSTEP]
rw [smul_mul_smul, hf, smul_neg, ← Algebra.algebraMap_eq_smul_one, ← sub_eq_add_neg, ← RingHom.map_mul, ←
  RingHom.map_sub]
[GOAL]
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x✝¹ x✝ : ℂ
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = ↑(algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * ↑(algebraMap ℝ A) x₂
[PROOFSTEP]
rw [Algebra.smul_def, Algebra.smul_def, Algebra.smul_def, ← Algebra.right_comm _ x₂, ← mul_assoc, ← add_mul, ←
  RingHom.map_mul, ← RingHom.map_mul, ← RingHom.map_add]
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ ↑(liftAux I' hI') I = I'
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ ↑F I * ↑F I = -1
[PROOFSTEP]
rw [← F.map_mul, I_mul_I, AlgHom.map_neg, AlgHom.map_one]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : { x // x ∈ skewAdjoint A }
⊢ -I • ↑a ∈ selfAdjoint A
[PROOFSTEP]
simp only [neg_smul, neg_mem_iff, selfAdjoint.mem_iff, star_smul, star_def, conj_I, star_val_eq, smul_neg, neg_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a b : { x // x ∈ skewAdjoint A }
⊢ (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
      (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b
[PROOFSTEP]
ext
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a b : { x // x ∈ skewAdjoint A }
⊢ ↑((fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b)) =
    ↑((fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
        (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b)
[PROOFSTEP]
simp only [AddSubgroup.coe_add, smul_add, AddMemClass.mk_add_mk]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : { x // x ∈ skewAdjoint A }
⊢ AddHom.toFun
      { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
        map_add' :=
          (_ :
            ∀ (a b : { x // x ∈ skewAdjoint A }),
              (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
      (a • b) =
    ↑(RingHom.id ℝ) a •
      AddHom.toFun
        { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
          map_add' :=
            (_ :
              ∀ (a b : { x // x ∈ skewAdjoint A }),
                (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
        b
[PROOFSTEP]
ext
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : { x // x ∈ skewAdjoint A }
⊢ ↑(AddHom.toFun
        { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
          map_add' :=
            (_ :
              ∀ (a b : { x // x ∈ skewAdjoint A }),
                (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
        (a • b)) =
    ↑(↑(RingHom.id ℝ) a •
        AddHom.toFun
          { toFun := fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) },
            map_add' :=
              (_ :
                ∀ (a b : { x // x ∈ skewAdjoint A }),
                  (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) (a + b) =
                    (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) a +
                      (fun a => { val := -I • ↑a, property := (_ : -I • ↑a ∈ selfAdjoint A) }) b) }
          b)
[PROOFSTEP]
simp only [neg_smul, skewAdjoint.val_smul, AddSubgroup.coe_mk, RingHom.id_apply, selfAdjoint.val_smul, smul_neg,
  neg_inj]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : { x // x ∈ skewAdjoint A }
⊢ I • a • ↑b = a • I • ↑b
[PROOFSTEP]
rw [smul_comm]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : { x // x ∈ skewAdjoint A }
⊢ I • ↑(↑negISMul a) = ↑a
[PROOFSTEP]
simp only [smul_smul, skewAdjoint.negISMul_apply_coe, neg_smul, smul_neg, I_mul_I, one_smul, neg_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ a) = 2⁻¹ • (a + star a)
[PROOFSTEP]
unfold realPart
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)
[PROOFSTEP]
simp only [selfAdjointPart_apply_coe, invOf_eq_inv]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ a) = -I • 2⁻¹ • (a - star a)
[PROOFSTEP]
unfold imaginaryPart
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(LinearMap.comp skewAdjoint.negISMul (skewAdjointPart ℝ)) a) = -I • 2⁻¹ • (a - star a)
[PROOFSTEP]
simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe, skewAdjointPart_apply_coe,
  invOf_eq_inv, neg_smul]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ a) + I • ↑(↑ℑ a) = a
[PROOFSTEP]
simpa only [smul_smul, realPart_apply_coe, imaginaryPart_apply_coe, neg_smul, I_mul_I, one_smul, neg_sub,
  add_add_sub_cancel, smul_sub, smul_add, neg_sub_neg, invOf_eq_inv] using invOf_two_smul_add_invOf_two_smul ℝ a
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑ℜ (I • a) = -↑ℑ a
[PROOFSTEP]
ext
  -- Porting note: was
    -- simp [smul_comm I, smul_sub, sub_eq_add_neg, add_comm]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ (I • a)) = ↑(-↑ℑ a)
[PROOFSTEP]
rw [realPart_apply_coe, AddSubgroupClass.coe_neg, imaginaryPart_apply_coe, neg_smul, neg_neg, smul_comm I, star_smul,
  star_def, conj_I, smul_sub, neg_smul, sub_eq_add_neg]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑ℑ (I • a) = ↑ℜ a
[PROOFSTEP]
ext
  -- Porting note: was
    -- simp [smul_comm I, smul_smul I]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ (I • a)) = ↑(↑ℜ a)
[PROOFSTEP]
rw [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm]
[GOAL]
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ 2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)
[PROOFSTEP]
simp [← smul_assoc]
[GOAL]
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
[PROOFSTEP]
conv_lhs => rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℜ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℜ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℜ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℜ ((↑z.re + ↑z.im * I) • a) = z.re • ↑ℜ a - z.im • ↑ℑ a
[PROOFSTEP]
simp [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg]
[GOAL]
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
[PROOFSTEP]
conv_lhs => rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℑ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℑ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
| ↑ℑ (z • a)
[PROOFSTEP]
rw [← re_add_im z]
[GOAL]
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℑ ((↑z.re + ↑z.im * I) • a) = z.re • ↑ℑ a + z.im • ↑ℜ a
[PROOFSTEP]
simp [-re_add_im, add_smul, ← smul_smul]
