case h.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
a b : ℝ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } =
    ↑(smulRight reClm x + I • smulRight imClm x) { re := a, im := b }
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (smulRight 1 x) = smulRight reClm x + I • smulRight imClm x
ext ⟨a, b⟩
no goals
case h.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
a b : ℝ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } =
    ↑(smulRight reClm x + I • smulRight imClm x) { re := a, im := b }
simp [mk_eq_add_mul_I, mul_smul, smul_comm I b x]