no goals
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ FiniteDimensional.finrank ℝ E = 2 * FiniteDimensional.finrank ℂ E
rw [← FiniteDimensional.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]