E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ 2 * Cardinal.lift (Module.rank ℂ E) = Cardinal.lift (2 * Module.rank ℂ E)
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift (Module.rank ℝ E) = Cardinal.lift (2 * Module.rank ℂ E)
rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']
no goals
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ 2 * Cardinal.lift (Module.rank ℂ E) = Cardinal.lift (2 * Module.rank ℂ E)
simp only [Cardinal.lift_id']