Theorem: SpiroPseudoPeriodic (NazgandLean4/SymmetricSpirographs.lean)

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ ∀ (n : ℤ) (t : ℂ), f₀ (t + 2 * ↑n * ↑π / ↑↑k) = cexp (I * 2 * ↑n * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [IntegerInduction]
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * ↑(m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * ↑(m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * ↑(m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * ↑(m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
simp [SetSpiro] at *
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
constructor
State after:
case left
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t

case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (m_1 : ℤ),
    (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
      ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case left
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
use 0
State after:
case h
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑0 * ↑π / ↑↑k) = cexp (I * 2 * ↑0 * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case h
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑0 * ↑π / ↑↑k) = cexp (I * 2 * ↑0 * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
simp only [Int.cast_zero, mul_zero, zero_mul, zero_div, add_zero, Complex.exp_zero, one_mul,
  implies_true]
State after:
no goals

State before:
case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (m_1 : ℤ),
    (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
      ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
intros m₁
State after:
case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) ↔
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) ↔
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
constructor
State after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t

case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
intros h₁ t
State after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show t + 2 * (↑m₁ + 1) * ↑π / ↑↑k = t + 2 * ↑m₁ * ↑π / ↑↑k + 2 * ↑π / ↑↑k by ring), h₀, h₁]
State after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show (I * 2 * ↑m * ↑π / ↑↑k).exp * ((I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * f₀ t) =
  (I * 2 * ↑m * ↑π / ↑↑k).exp * (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * f₀ t by ring), ←Complex.exp_add]
State after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k + I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k + I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
ring_nf
State after:
no goals

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

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

State before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
intros h₁ t
State after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show t + 2 * ↑m₁ * ↑π / ↑↑k = (t - 2 * ↑π / ↑↑k) + 2 * (↑m₁ + 1) * ↑π / ↑↑k by ring), h₁]
State after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t

State before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show f₀ t = f₀ ((t - 2 * ↑π / ↑↑k) + 2 * ↑π / ↑↑k) by ring_nf), h₀]
State after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k))

State before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k))
Tactic:
rw [(show (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * ((I * 2 * ↑m * ↑π / ↑↑k).exp * f₀ (t - 2 * ↑π / ↑↑k)) =
  (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * (I * 2 * ↑m * ↑π / ↑↑k).exp * f₀ (t - 2 * ↑π / ↑↑k) by ring_nf), ←Complex.exp_add]
State after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k + I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)

State before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k + I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)
Tactic:
ring_nf
State after:
no goals

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

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ t = f₀ (t - 2 * ↑π / ↑↑k + 2 * ↑π / ↑↑k)
Tactic:
ring_nf
State after:
no goals

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)
Tactic:
ring_nf
State after:
no goals