Theorem: SpiroLinearCombination (NazgandLean4/SymmetricSpirographs.lean)

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 *
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)

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
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)

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₁]
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)

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
State after:
no goals