Theorem: RouForm (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
x : ℕ
⊢ cexp (2 * ↑π * (↑x / ↑↑n) * I) ^ ↑n = 1
Tactic:
rw [(Complex.exp_nat_mul _ n).symm, Complex.exp_eq_one_iff]
State after:
n : ℕ+
x : ℕ
⊢ ∃ n_1, ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑n_1 * (2 * ↑π * I)

State before:
n : ℕ+
x : ℕ
⊢ ∃ n_1, ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑n_1 * (2 * ↑π * I)
Tactic:
use x
State after:
case h
n : ℕ+
x : ℕ
⊢ ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑↑x * (2 * ↑π * I)

State before:
case h
n : ℕ+
x : ℕ
⊢ ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑↑x * (2 * ↑π * I)
Tactic:
field_simp
State after:
case h
n : ℕ+
x : ℕ
⊢ 2 * ↑π * ↑x * I = ↑x * (2 * ↑π * I)

State before:
case h
n : ℕ+
x : ℕ
⊢ 2 * ↑π * ↑x * I = ↑x * (2 * ↑π * I)
Tactic:
ring_nf
State after:
no goals