internlm/Lean-Github huggingface dataset:
Theorem: WavelengthGcd
Proof state before:
case mp.right
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
h₁ : ↑(k₀.gcd k₁) ∣ k₁
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
obtain ⟨w, hw⟩ := h₁
Proof state after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)
Theorem: WavelengthGcd
Proof state before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
rw [WavelengthRestate]
Proof state after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
Theorem: WavelengthGcd
Proof state before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
Tactic:
intros m k
Proof state after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p m ↔ p (m + k * k₁)
Theorem: WavelengthGcd
Proof state before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p m ↔ p (m + k * k₁)
Tactic:
rw [h₀ m (w * k)]
Proof state after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * k₁)
Theorem: WavelengthGcd
Proof state before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * k₁)
Tactic:
nth_rw 2 [hw]
Proof state after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * (↑(k₀.gcd k₁) * w))
Theorem: WavelengthGcd
Proof state before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * (↑(k₀.gcd k₁) * w))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: WavelengthGcd
Proof state before:
case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
⊢ ((∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)) → ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Tactic:
intros h₀
Proof state after:
case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Theorem: WavelengthGcd
Proof state before:
case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Tactic:
obtain ⟨h₁, h₂⟩ := h₀
Proof state after:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m : ℤ), p m ↔ p (m + k₀)
h₂ : ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Theorem: WavelengthGcd
Proof state before:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m : ℤ), p m ↔ p (m + k₀)
h₂ : ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Tactic:
rw [WavelengthRestate] at *
Proof state after:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
Theorem: WavelengthGcd
Proof state before:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
Tactic:
intros m j
Proof state after:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j : ℤ
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))
Theorem: WavelengthGcd
Proof state before:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j : ℤ
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))
Tactic:
obtain ⟨w₀, w₁, h₃⟩ := GcdLinearCombination k₀ k₁
Proof state after:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))
Theorem: WavelengthGcd
Proof state before:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))
Tactic:
rw [h₃, h₁ m (j * w₀), h₂ (m + j * w₀ * k₀) (j * w₁)]
Proof state after:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p (m + j * w₀ * k₀ + j * w₁ * k₁) ↔ p (m + j * (w₀ * k₀ + w₁ * k₁))
Theorem: WavelengthGcd
Proof state before:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p (m + j * w₀ * k₀ + j * w₁ * k₁) ↔ p (m + j * (w₀ * k₀ + w₁ * k₁))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroLinearCombination
Proof state before:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
h₁ : f₁ ∈ SetSpiro k m
w₀ w₁ : ℂ
⊢ (fun t => w₀ * f₀ t + w₁ * f₁ t) ∈ SetSpiro k m
Tactic:
simp [SetSpiro] at *
Proof state after:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
h₁ : ∀ (t : ℂ), f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t
w₀ w₁ : ℂ
⊢ ∀ (t : ℂ),
    w₀ * f₀ (t + 2 * ↑π / ↑↑k) + w₁ * f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * (w₀ * f₀ t + w₁ * f₁ t)
Theorem: SpiroLinearCombination
Proof state before:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
h₁ : ∀ (t : ℂ), f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t
w₀ w₁ : ℂ
⊢ ∀ (t : ℂ),
    w₀ * f₀ (t + 2 * ↑π / ↑↑k) + w₁ * f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * (w₀ * f₀ t + w₁ * f₁ t)
Tactic:
intros t
Proof state after:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
h₁ : ∀ (t : ℂ), f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t
w₀ w₁ t : ℂ
⊢ w₀ * f₀ (t + 2 * ↑π / ↑↑k) + w₁ * f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * (w₀ * f₀ t + w₁ * f₁ t)
Theorem: SpiroLinearCombination
Proof state before:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
h₁ : ∀ (t : ℂ), f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t
w₀ w₁ t : ℂ
⊢ w₀ * f₀ (t + 2 * ↑π / ↑↑k) + w₁ * f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * (w₀ * f₀ t + w₁ * f₁ t)
Tactic:
simp only [h₀, h₁]
Proof state after:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
h₁ : ∀ (t : ℂ), f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t
w₀ w₁ t : ℂ
⊢ w₀ * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t) + w₁ * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (w₀ * f₀ t + w₁ * f₁ t)
Theorem: SpiroLinearCombination
Proof state before:
f₀ f₁ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
h₁ : ∀ (t : ℂ), f₁ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t
w₀ w₁ t : ℂ
⊢ w₀ * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t) + w₁ * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₁ t) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * (w₀ * f₀ t + w₁ * f₁ t)
Tactic:
ring
Proof state after:
no goals
Theorem: SpiroOffset
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
o : ℂ
⊢ (fun t => f₀ (t + o)) ∈ SetSpiro k m
Tactic:
simp [SetSpiro] at *
Proof 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)
Theorem: SpiroOffset
Proof 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
Proof 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)
Theorem: SpiroOffset
Proof 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₀]
Proof state after:
no goals
Theorem: SpiroOffset
Proof 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
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ ∀ (n : ℤ) (t : ℂ), f₀ (t + 2 * ↑n * ↑π / ↑↑k) = cexp (I * 2 * ↑n * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [IntegerInduction]
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * ↑(m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * ↑(m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * ↑(m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * ↑(m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
simp [SetSpiro] at *
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ (∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t) ∧
    ∀ (m_1 : ℤ),
      (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
        ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
constructor
Proof state after:
case left
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t

case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (m_1 : ℤ),
    (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
      ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case left
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∃ k_1, ∀ (t : ℂ), f₀ (t + 2 * ↑k_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑k_1 * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
use 0
Proof state after:
case h
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑0 * ↑π / ↑↑k) = cexp (I * 2 * ↑0 * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case h
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑0 * ↑π / ↑↑k) = cexp (I * 2 * ↑0 * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
simp only [Int.cast_zero, mul_zero, zero_mul, zero_div, add_zero, Complex.exp_zero, one_mul,
  implies_true]
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
⊢ ∀ (m_1 : ℤ),
    (∀ (t : ℂ), f₀ (t + 2 * ↑m_1 * ↑π / ↑↑k) = cexp (I * 2 * ↑m_1 * ↑m * ↑π / ↑↑k) * f₀ t) ↔
      ∀ (t : ℂ), f₀ (t + 2 * (↑m_1 + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m_1 + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
intros m₁
Proof state after:
case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) ↔
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) ↔
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
constructor
Proof state after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t

case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
intros h₁ t
Proof state after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show t + 2 * (↑m₁ + 1) * ↑π / ↑↑k = t + 2 * ↑m₁ * ↑π / ↑↑k + 2 * ↑π / ↑↑k by ring), h₀, h₁]
Proof state after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show (I * 2 * ↑m * ↑π / ↑↑k).exp * ((I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * f₀ t) =
  (I * 2 * ↑m * ↑π / ↑↑k).exp * (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * f₀ t by ring), ←Complex.exp_add]
Proof state after:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k + I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mp
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k + I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ t + 2 * (↑m₁ + 1) * ↑π / ↑↑k = t + 2 * ↑m₁ * ↑π / ↑↑k + 2 * ↑π / ↑↑k
Tactic:
ring
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * ↑m * ↑π / ↑↑k) * cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
ring
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
⊢ (∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t) →
    ∀ (t : ℂ), f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
intros h₁ t
Proof state after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ (t + 2 * ↑m₁ * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show t + 2 * ↑m₁ * ↑π / ↑↑k = (t - 2 * ↑π / ↑↑k) + 2 * (↑m₁ + 1) * ↑π / ↑↑k by ring), h₁]
Proof state after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * f₀ t
Tactic:
rw [(show f₀ t = f₀ ((t - 2 * ↑π / ↑↑k) + 2 * ↑π / ↑↑k) by ring_nf), h₀]
Proof state after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k))
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k))
Tactic:
rw [(show (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * ((I * 2 * ↑m * ↑π / ↑↑k).exp * f₀ (t - 2 * ↑π / ↑↑k)) =
  (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k).exp * (I * 2 * ↑m * ↑π / ↑↑k).exp * f₀ (t - 2 * ↑π / ↑↑k) by ring_nf), ←Complex.exp_add]
Proof state after:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k + I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)
Theorem: SpiroPseudoPeriodic
Proof state before:
case right.mpr
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k + I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ t + 2 * ↑m₁ * ↑π / ↑↑k = t - 2 * ↑π / ↑↑k + 2 * (↑m₁ + 1) * ↑π / ↑↑k
Tactic:
ring
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ t = f₀ (t - 2 * ↑π / ↑↑k + 2 * ↑π / ↑↑k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPseudoPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ t
m₁ : ℤ
h₁ : ∀ (t : ℂ), f₀ (t + 2 * (↑m₁ + 1) * ↑π / ↑↑k) = cexp (I * 2 * (↑m₁ + 1) * ↑m * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * (cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)) =
    cexp (I * 2 * ↑m₁ * ↑m * ↑π / ↑↑k) * cexp (I * 2 * ↑m * ↑π / ↑↑k) * f₀ (t - 2 * ↑π / ↑↑k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SpiroPeriodic
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π) = f₀ t
Tactic:
intros t
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
t : ℂ
⊢ f₀ (t + 2 * ↑π) = f₀ t
Theorem: SpiroPeriodic
Proof 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
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
⊢ f₀ (t + 2 * ↑π) = f₀ t
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
⊢ f₀ (t + 2 * ↑π) = f₀ t
Tactic:
have h₂ : (2 : ℂ) * ↑↑↑k * ↑π / ↑↑k = 2 * ↑π := by
  field_simp
  ring
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
h₂ : 2 * ↑↑k * ↑π / ↑↑k = 2 * ↑π
⊢ f₀ (t + 2 * ↑π) = f₀ t