Theorem: SpiroPeriodic2 (NazgandLean4/SymmetricSpirographs.lean)

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
State after:
f₀ : ℂ → ℂ
k : ℕ+
m : ℤ
h₀ : f₀ ∈ SetSpiro k m
h₂ : ↑(m.gcd ↑↑k) ∣ ↑↑k
⊢ ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑(m.gcd ↑↑k)) = f₀ t

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

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

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

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

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₁₂
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

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

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

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

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

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

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

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

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₆]
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

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

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

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₂]
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

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

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₈]
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

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

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₉]
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

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

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

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

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

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₁₀
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

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₁₀
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

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₁₀
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

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₁₀
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

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

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

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

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

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

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

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

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

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

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