intro i hi
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∀ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ↑x
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ n - 2 ^ i) = ↑i