Theorem: SetSpiroRelated (NazgandLean4/SymmetricSpirographs.lean)

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

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

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

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

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

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

State before:
case e_a.e_z
f₀ : ℂ → ℂ
k₀ k₁ : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k₀) = cexp (I * 2 * ↑m * ↑π / ↑↑k₀) * f₀ t
t : ℂ
⊢ ↑↑k₀ * (I * 2 * ↑m * ↑π / ↑↑k₀) = I * 2 * (↑m * ↑↑k₁) * ↑π / ↑↑k₁
Tactic:
ring_nf
State after:
case e_a.e_z
f₀ : ℂ → ℂ
k₀ k₁ : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k₀) = cexp (I * 2 * ↑m * ↑π / ↑↑k₀) * f₀ t
t : ℂ
⊢ ↑↑k₀ * I * ↑m * ↑π * (↑↑k₀)⁻¹ * 2 = I * ↑m * ↑π * ↑↑k₁ * (↑↑k₁)⁻¹ * 2

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

State before:
case e_a.e_z.e_a
f₀ : ℂ → ℂ
k₀ k₁ : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k₀) = cexp (I * 2 * ↑m * ↑π / ↑↑k₀) * f₀ t
t : ℂ
⊢ ↑↑k₀ * I * ↑m * ↑π * (↑↑k₀)⁻¹ = I * ↑m * ↑π * ↑↑k₁ * (↑↑k₁)⁻¹
Tactic:
field_simp
State after:
case e_a.e_z.e_a
f₀ : ℂ → ℂ
k₀ k₁ : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k₀) = cexp (I * 2 * ↑m * ↑π / ↑↑k₀) * f₀ t
t : ℂ
⊢ ↑↑k₀ * I * ↑m * ↑π = I * ↑m * ↑π * ↑↑k₀

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

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