Theorem: SpiroOffset (NazgandLean4/SymmetricSpirographs.lean)

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

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

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

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