Easiest way to play with casts in C

Stream: new members

[Srivatsa Srinivas]

Hi all,

What is the easiest way to deal with this minimal working example?

example (a b c : ℝ) : (↑a = (2 : ℂ) * ↑b * ↑c) ↔ (a = 2 *b *c) := by sorry

Best,
Vatsa

[Aaron Liu]

import Mathlib

example (a b c : ℝ) : (↑a = (2 : ℂ) * ↑b * ↑c) ↔ (a = 2 *b *c) := by norm_cast

[Srivatsa Srinivas]

Thanks!