Theorem: ExpToNatPowersOfI (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
k : ℕ
⊢ cexp (↑π * I * ↑k / 2) = I ^ k
Tactic:
induction' k with K Kih
State after:
case zero

⊢ cexp (↑π * I * ↑0 / 2) = I ^ 0

case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑(K + 1) / 2) = I ^ (K + 1)

State before:
case zero

⊢ cexp (↑π * I * ↑0 / 2) = I ^ 0
Tactic:
simp only [Nat.zero_eq, CharP.cast_eq_zero, mul_zero, zero_div, Complex.exp_zero, pow_zero]
State after:
no goals

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑(K + 1) / 2) = I ^ (K + 1)
Tactic:
simp_rw [Nat.cast_succ]
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)
Tactic:
have h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I := by
  simp only [ofReal_div, ofReal_ofNat]
  ring_nf
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)
Tactic:
rw [h₀]
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)
Tactic:
clear h₀
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)
Tactic:
rw [Complex.exp_add, Kih, ExpPiMulIHalf]
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ I ^ K * I = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ I ^ K * I = I ^ (K + 1)
Tactic:
have h₂ := zpow_add₀ I_ne_zero K 1
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ ↑K * I ^ 1
⊢ I ^ K * I = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ ↑K * I ^ 1
⊢ I ^ K * I = I ^ (K + 1)
Tactic:
simp only [zpow_natCast, zpow_one] at h₂
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ K * I = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ K * I = I ^ (K + 1)
Tactic:
rw [←h₂]
State after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ (↑K + 1) = I ^ (K + 1)

State before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ (↑K + 1) = I ^ (K + 1)
Tactic:
exact rfl
State after:
no goals

State before:
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
Tactic:
simp only [ofReal_div, ofReal_ofNat]
State after:
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑π / 2 * I

State before:
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑π / 2 * I
Tactic:
ring_nf
State after:
no goals