internlm/Lean-Github huggingface dataset:
Theorem: SpiroPeriodic
Proof 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 *
Proof 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
Theorem: SpiroPeriodic
Proof 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₁
Proof 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
Theorem: SpiroPeriodic
Proof 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₁]
Proof 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
Theorem: SpiroPeriodic
Proof 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
Proof 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
Theorem: SpiroPeriodic
Proof 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₃]
Proof 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
Theorem: SpiroPeriodic
Proof 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
Proof 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
Theorem: SpiroPeriodic
Proof 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₄]
Proof 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
Theorem: SpiroPeriodic
Proof 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]
Proof state after:
no goals
Theorem: SpiroPeriodic
Proof 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
Proof 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
Theorem: SpiroPeriodic
Proof 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
Proof state after:
no goals
Theorem: SpiroPeriodic
Proof 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
Proof 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
Theorem: SpiroPeriodic
Proof 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
Proof state after:
no goals
Theorem: SpiroPeriodic
Proof 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]
Proof 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)
Theorem: SpiroPeriodic
Proof 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
Proof 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)
Theorem: SpiroPeriodic
Proof 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
Proof state after:
no goals
Theorem: SpiroPeriodic2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
have h₂ : ↑(Int.gcd m k) ∣ (k : ℤ) := Int.gcd_dvd_right
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
h₂ : ↑(m.gcd ↑↑k) ∣ ↑↑k
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
h₂ : ↑(m.gcd ↑↑k) ∣ ↑↑k
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
obtain ⟨w, hw⟩ := h₂
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
have h₁ := SpiroPseudoPeriodic k m h₀ w
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
intros t
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
specialize h₁ t
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
have h₄ : (m.gcd ↑↑k : ℂ) ≠ 0 := by
  by_contra h₁₀
  simp only [Nat.cast_eq_zero] at h₁₀
  rw [Int.gcd_eq_zero_iff] at h₁₀
  obtain ⟨_, h₁₂⟩ := h₁₀
  simp only [Nat.cast_eq_zero, PNat.ne_zero] at h₁₂
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
h₄ : ↑(m.gcd ↑↑k) ≠ 0
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
h₄ : ↑(m.gcd ↑↑k) ≠ 0
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
have h₃ : (w : ℂ) = ↑(k : ℤ) / ↑(m.gcd ↑↑k) := by
  nth_rw 1 [hw]
  simp only [Int.cast_mul, Int.cast_natCast]
  field_simp
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * ↑w * ↑π / ↑↑k) = cexp (I * 2 * ↑w * ↑m * ↑π / ↑↑k) * f₀ t
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
rw [h₃] at h₁
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * (↑↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k) = cexp (I * 2 * (↑↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₁ : f₀ (t + 2 * (↑↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k) = cexp (I * 2 * (↑↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
simp only [Int.cast_natCast] at h₁
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
have h₅ : (2 : ℂ) * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k) := by
  field_simp
  ring_nf
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
rw [h₅] at h₁
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
⊢ f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t
Tactic:
rw [h₁]
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
⊢ cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
⊢ cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t = f₀ t
Tactic:
have h₆ : (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) = (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) := by
  field_simp
  ring_nf
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
⊢ cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
⊢ cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t = f₀ t
Tactic:
rw [h₆]
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Tactic:
have h₇ : ↑(Int.gcd m k) ∣ m := Int.gcd_dvd_left
Proof state after:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
h₇ : ↑(m.gcd ↑↑k) ∣ m
⊢ cexp (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
h₇ : ↑(m.gcd ↑↑k) ∣ m
⊢ cexp (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Tactic:
obtain ⟨w₂, hw₂⟩ := h₇
Proof state after:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
⊢ cexp (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
⊢ cexp (I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Tactic:
nth_rw 1 [hw₂]
Proof state after:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
⊢ cexp (I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
⊢ cexp (I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Tactic:
have h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂ := by
  field_simp
  ring_nf
Proof state after:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
⊢ cexp (I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
⊢ cexp (I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k)) * f₀ t = f₀ t
Tactic:
rw [h₈]
Proof state after:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
⊢ cexp (I * 2 * ↑π * ↑w₂) * f₀ t = f₀ t
Theorem: SpiroPeriodic2
Proof state before:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
⊢ cexp (I * 2 * ↑π * ↑w₂) * f₀ t = f₀ t
Tactic:
suffices h₉ : (I * 2 * ↑π * ↑w₂).exp = 1
Proof state after:
case intro.intro
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
h₉ : cexp (I * 2 * ↑π * ↑w₂) = 1
⊢ cexp (I * 2 * ↑π * ↑w₂) * f₀ t = f₀ t

case h₉
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
w : ℤ
hw : ↑↑k = ↑(m.gcd ↑↑k) * w
t : ℂ
h₄ : ↑(m.gcd ↑↑k) ≠ 0
h₃ : ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
h₁ : f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = cexp (I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k) * f₀ t
h₅ : 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
h₆ : I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
w₂ : ℤ
hw₂ : m = ↑(m.gcd ↑↑k) * w₂
h₈ : I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
⊢ cexp (I * 2 * ↑π * ↑w₂) = 1