Theorem: SetSpiroRelated2 (NazgandLean4/SymmetricSpirographs.lean)

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

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

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

State before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * (cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Tactic:
ring_nf
State after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2)) *
        cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2) * cexp (I * t * ↑m₁ - I * t * ↑m₀)

State before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2)) *
        cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2) * cexp (I * t * ↑m₁ - I * t * ↑m₀)
Tactic:
rw [←Complex.exp_add, (show f₀ t * (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2).exp * (I * t * ↑m₁ - I * t * ↑m₀).exp =
  f₀ t * ((I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2).exp * (I * t * ↑m₁ - I * t * ↑m₀).exp) by ring), ←Complex.exp_add]
State after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp
        (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) +
          I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 + (I * t * ↑m₁ - I * t * ↑m₀))

State before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp
        (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) +
          I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 + (I * t * ↑m₁ - I * t * ↑m₀))
Tactic:
ring_nf
State after:
no goals

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