Theorem: SimpleGeneralSpiro (NazgandLean4/SymmetricSpirographs.lean)

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
⊢ (fun t => cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k))) ∈ SetSpiro k m
Tactic:
simp [SetSpiro] at *
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
⊢ ∀ (t : ℂ),
    cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
      cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
⊢ ∀ (t : ℂ),
    cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
      cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
intros t
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
rw [(show I * (t + 2 * ↑π / ↑↑k) * ↑m = (I * 2 * ↑m * ↑π / ↑↑k) + (I * t * ↑m) by ring), Complex.exp_add]
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
field_simp
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
have h₀ : (I * (t * ↑↑k + 2 * ↑π)).exp = (I * t * ↑↑k).exp := by
  rw [(show I * (t * ↑↑k + 2 * ↑π) = I * t * ↑↑k + 2 * ↑π * I by ring), Complex.exp_add, Complex.exp_two_pi_mul_I]
  simp only [mul_one]
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
rw [h₀]
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
ring
State after:
no goals

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ I * (t + 2 * ↑π / ↑↑k) * ↑m = I * 2 * ↑m * ↑π / ↑↑k + I * t * ↑m
Tactic:
ring
State after:
no goals

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
Tactic:
rw [(show I * (t * ↑↑k + 2 * ↑π) = I * t * ↑↑k + 2 * ↑π * I by ring), Complex.exp_add, Complex.exp_two_pi_mul_I]
State after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * t * ↑↑k) * 1 = cexp (I * t * ↑↑k)

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * t * ↑↑k) * 1 = cexp (I * t * ↑↑k)
Tactic:
simp only [mul_one]
State after:
no goals

State before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ I * (t * ↑↑k + 2 * ↑π) = I * t * ↑↑k + 2 * ↑π * I
Tactic:
ring
State after:
no goals