internlm/Lean-Github huggingface dataset:
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₂
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
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₂
h₉ : cexp (I * 2 * ↑π * ↑w₂) = 1
⊢ 1 * 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
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₂
h₉ : cexp (I * 2 * ↑π * ↑w₂) = 1
⊢ 1 * 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
Tactic:
simp only [one_mul]
Proof state after:
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
Theorem: SpiroPeriodic2
Proof state before:
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
Tactic:
rw [Complex.exp_eq_one_iff]
Proof state after:
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₂
⊢ ∃ n, I * 2 * ↑π * ↑w₂ = ↑n * (2 * ↑π * I)
Theorem: SpiroPeriodic2
Proof state before:
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₂
⊢ ∃ n, I * 2 * ↑π * ↑w₂ = ↑n * (2 * ↑π * I)
Tactic:
use w₂
Proof state after:
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₂
⊢ I * 2 * ↑π * ↑w₂ = ↑w₂ * (2 * ↑π * I)
Theorem: SpiroPeriodic2
Proof state before:
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₂
⊢ I * 2 * ↑π * ↑w₂ = ↑w₂ * (2 * ↑π * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ ↑(m.gcd ↑↑k) ≠ 0
Tactic:
by_contra h₁₀
Proof state after:
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
⊢ False
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ False
Tactic:
simp only [Nat.cast_eq_zero] at h₁₀
Proof state after:
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
⊢ False
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ False
Tactic:
rw [Int.gcd_eq_zero_iff] at h₁₀
Proof state after:
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 = 0 ∧ ↑↑k = 0
⊢ False
Theorem: SpiroPeriodic2
Proof state before:
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 = 0 ∧ ↑↑k = 0
⊢ False
Tactic:
obtain ⟨_, h₁₂⟩ := 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
left✝ : m = 0
h₁₂ : ↑↑k = 0
⊢ False
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
left✝ : m = 0
h₁₂ : ↑↑k = 0
⊢ False
Tactic:
simp only [Nat.cast_eq_zero, PNat.ne_zero] at h₁₂
Proof state after:
no goals
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ ↑w = ↑↑↑k / ↑(m.gcd ↑↑k)
Tactic:
nth_rw 1 [hw]
Proof state after:
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
⊢ ↑w = ↑(↑(m.gcd ↑↑k) * w) / ↑(m.gcd ↑↑k)
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ ↑w = ↑(↑(m.gcd ↑↑k) * w) / ↑(m.gcd ↑↑k)
Tactic:
simp only [Int.cast_mul, Int.cast_natCast]
Proof state after:
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
⊢ ↑w = ↑(m.gcd ↑↑k) * ↑w / ↑(m.gcd ↑↑k)
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ ↑w = ↑(m.gcd ↑↑k) * ↑w / ↑(m.gcd ↑↑k)
Tactic:
field_simp
Proof state after:
no goals
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑π / ↑↑k = 2 * ↑π / ↑(m.gcd ↑↑k)
Tactic:
field_simp
Proof state after:
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
⊢ 2 * ↑↑k * ↑π * ↑(m.gcd ↑↑k) = 2 * ↑π * (↑(m.gcd ↑↑k) * ↑↑k)
Theorem: SpiroPeriodic2
Proof state before:
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
⊢ 2 * ↑↑k * ↑π * ↑(m.gcd ↑↑k) = 2 * ↑π * (↑(m.gcd ↑↑k) * ↑↑k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPeriodic2
Proof state before:
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)
⊢ I * 2 * (↑↑k / ↑(m.gcd ↑↑k)) * ↑m * ↑π / ↑↑k = I * 2 * ↑m * ↑π / ↑(m.gcd ↑↑k)
Tactic:
field_simp
Proof state after:
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)
⊢ I * 2 * ↑↑k * ↑m * ↑π * ↑(m.gcd ↑↑k) = I * 2 * ↑m * ↑π * (↑(m.gcd ↑↑k) * ↑↑k)
Theorem: SpiroPeriodic2
Proof state before:
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)
⊢ I * 2 * ↑↑k * ↑m * ↑π * ↑(m.gcd ↑↑k) = I * 2 * ↑m * ↑π * (↑(m.gcd ↑↑k) * ↑↑k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPeriodic2
Proof state before:
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₂
⊢ I * 2 * ↑(↑(m.gcd ↑↑k) * w₂) * ↑π / ↑(m.gcd ↑↑k) = I * 2 * ↑π * ↑w₂
Tactic:
field_simp
Proof state after:
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₂
⊢ I * 2 * (↑(m.gcd ↑↑k) * ↑w₂) * ↑π = I * 2 * ↑π * ↑w₂ * ↑(m.gcd ↑↑k)
Theorem: SpiroPeriodic2
Proof state before:
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₂
⊢ I * 2 * (↑(m.gcd ↑↑k) * ↑w₂) * ↑π = I * 2 * ↑π * ↑w₂ * ↑(m.gcd ↑↑k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
⊢ (fun t => cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k))) ∈ SetSpiro k m
Tactic:
simp [SetSpiro] at *
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
⊢ ∀ (t : ℂ),
    cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
      cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
⊢ ∀ (t : ℂ),
    cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
      cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
intros t
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
rw [(show I * (t + 2 * ↑π / ↑↑k) * ↑m = (I * 2 * ↑m * ↑π / ↑↑k) + (I * t * ↑m) by ring), Complex.exp_add]
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t + 2 * ↑π / ↑↑k) * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
field_simp
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
have h₀ : (I * (t * ↑↑k + 2 * ↑π)).exp = (I * t * ↑↑k).exp := by
  rw [(show I * (t * ↑↑k + 2 * ↑π) = I * t * ↑↑k + 2 * ↑π * I by ring), Complex.exp_add, Complex.exp_two_pi_mul_I]
  simp only [mul_one]
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * (t * ↑↑k + 2 * ↑π))) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
rw [h₀]
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
h₀ : cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * t * ↑m) * g (cexp (I * t * ↑↑k)))
Tactic:
ring
Proof state after:
no goals
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ I * (t + 2 * ↑π / ↑↑k) * ↑m = I * 2 * ↑m * ↑π / ↑↑k + I * t * ↑m
Tactic:
ring
Proof state after:
no goals
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * (t * ↑↑k + 2 * ↑π)) = cexp (I * t * ↑↑k)
Tactic:
rw [(show I * (t * ↑↑k + 2 * ↑π) = I * t * ↑↑k + 2 * ↑π * I by ring), Complex.exp_add, Complex.exp_two_pi_mul_I]
Proof state after:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * t * ↑↑k) * 1 = cexp (I * t * ↑↑k)
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ cexp (I * t * ↑↑k) * 1 = cexp (I * t * ↑↑k)
Tactic:
simp only [mul_one]
Proof state after:
no goals
Theorem: SimpleGeneralSpiro
Proof state before:
k : ℕ+
m : ℤ
g : ℂ → ℂ
t : ℂ
⊢ I * (t * ↑↑k + 2 * ↑π) = I * t * ↑↑k + 2 * ↑π * I
Tactic:
ring
Proof state after:
no goals
Theorem: SetSpiroRelated
Proof 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 *
Proof 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₀
Theorem: SetSpiroRelated
Proof 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
Proof 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₀
Theorem: SetSpiroRelated
Proof 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
Proof 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₀
Theorem: SetSpiroRelated
Proof 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]
Proof 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₀
Theorem: SetSpiroRelated
Proof 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
Proof 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₁)
Theorem: SetSpiroRelated
Proof 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
Proof 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₁
Theorem: SetSpiroRelated
Proof 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
Proof 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
Theorem: SetSpiroRelated
Proof 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
Proof 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₁)⁻¹
Theorem: SetSpiroRelated
Proof 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
Proof 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₀
Theorem: SetSpiroRelated
Proof 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
Proof state after:
no goals
Theorem: SetSpiroRelated
Proof 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
Proof state after:
no goals