English
Let m1, m2 ∈ ℤ and y1, y2 ∈ ℕ with m1 · 2^{y1} = m2 · 2^{y2}. Then m1 · powHalf(y2) = m2 · powHalf(y1).
Русский
Пусть m1, m2 ∈ ℤ и y1, y2 ∈ ℕ так, что m1 · 2^{y1} = m2 · 2^{y2}. Тогда m1 · powHalf(y2) = m2 · powHalf(y1).
LaTeX
$$$$ m_1 \cdot 2^{y_1} = m_2 \cdot 2^{y_2} \Rightarrow m_1 \cdot powHalf(y_2) = m_2 \cdot powHalf(y_1). $$$$
Lean4
theorem dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) : m₁ * powHalf y₂ = m₂ * powHalf y₁ :=
by
revert m₁ m₂
wlog h : y₁ ≤ y₂
· intro m₁ m₂ aux; exact (this (le_of_not_ge h) aux.symm).symm
intro m₁ m₂ h₂
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h
rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂
rcases h₂ with h₂ | h₂
· rw [h₂, add_comm]
simp_rw [Int.cast_mul, Int.cast_pow, Int.cast_ofNat, zsmul_pow_two_powHalf m₂ c y₁]
· have := Nat.one_le_pow y₁ 2 Nat.succ_pos'
norm_cast at h₂; cutsat
