exact hc
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
hc : ∑ i : Fin n, c i = k
S : Type := (i : Fin n) → { s // Even s.card }
p : S → ↑{g | ψ n k g = f} :=
  fun cs =>
    let g1 := fun i =>
      let y := ↑f ⟨↑i, ⋯⟩;
      let y' := ⟨↑y, ⋯⟩;
      let ys := cs y';
      if ⟨i, ⋯⟩ ∈ ↑ys then ⟨↑y + n, ⋯⟩ else y;
    let hg1 := ⋯;
    let hgg := ⋯;
    ⟨⟨g1, hg1⟩, hgg⟩
Scard : Fintype.card S = ∏ i : Fin n, 2 ^ (c i - 1)
h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ ∑ i : Fin n, (c i - 1)
h2 : n = ∑ i : Fin n, 1
h3 : ∀ x ∈ Finset.univ, c x - 1 + 1 = c x
⊢ ∑ x : Fin n, c x = k
no goals