Theorem: SpiroPeriodic (NazgandLean4/SymmetricSpirographs.lean)

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

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
⊢ f₀ (t + 2 * ↑π) = f₀ t
Tactic:
have h₁ := SpiroPseudoPeriodic k m h₀ k t
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₁ : f₀ (t + 2 * ↑↑↑k * ↑π / ↑↑k) = cexp (I * 2 * ↑↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π) = f₀ t

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₁ : f₀ (t + 2 * ↑↑↑k * ↑π / ↑↑k) = cexp (I * 2 * ↑↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π) = f₀ t
Tactic:
have h₂ : (2 : ℂ) * ↑↑↑k * ↑π / ↑↑k = 2 * ↑π := by
  field_simp
  ring
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₁ : f₀ (t + 2 * ↑↑↑k * ↑π / ↑↑k) = cexp (I * 2 * ↑↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
⊢ f₀ (t + 2 * ↑π) = f₀ t

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₁ : f₀ (t + 2 * ↑↑↑k * ↑π / ↑↑k) = cexp (I * 2 * ↑↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
⊢ f₀ (t + 2 * ↑π) = f₀ t
Tactic:
simp only [Int.cast_natCast] at *
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑↑k * ↑π / ↑↑k) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π) = f₀ t

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

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

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
⊢ cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t = f₀ t
Tactic:
have h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I := by
  field_simp
  ring
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
⊢ cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t = f₀ t

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

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
⊢ cexp (↑m * 2 * ↑π * I) * f₀ t = f₀ t
Tactic:
have h₄ : (↑m * 2 * ↑π * I).exp = 1 := by
  rw [Complex.exp_eq_one_iff]
  use m
  ring
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
h₄ : cexp (↑m * 2 * ↑π * I) = 1
⊢ cexp (↑m * 2 * ↑π * I) * f₀ t = f₀ t

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
h₄ : cexp (↑m * 2 * ↑π * I) = 1
⊢ cexp (↑m * 2 * ↑π * I) * f₀ t = f₀ t
Tactic:
rw [h₄]
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
h₄ : cexp (↑m * 2 * ↑π * I) = 1
⊢ 1 * f₀ t = f₀ t

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
h₄ : cexp (↑m * 2 * ↑π * I) = 1
⊢ 1 * f₀ t = f₀ t
Tactic:
simp only [one_mul]
State after:
no goals

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

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

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

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

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
⊢ cexp (↑m * 2 * ↑π * I) = 1
Tactic:
rw [Complex.exp_eq_one_iff]
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
⊢ ∃ n, ↑m * 2 * ↑π * I = ↑n * (2 * ↑π * I)

State before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
⊢ ∃ n, ↑m * 2 * ↑π * I = ↑n * (2 * ↑π * I)
Tactic:
use m
State after:
case h
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
h₁ : f₀ (t + 2 * ↑π) = cexp (I * 2 * ↑↑k * ↑m * ↑π / ↑↑k) * f₀ t
h₃ : I * 2 * ↑↑k * ↑m * ↑π / ↑↑k = ↑m * 2 * ↑π * I
⊢ ↑m * 2 * ↑π * I = ↑m * (2 * ↑π * I)

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