sorry
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 }
cs : S
g1 : Fin k → Fin (2 * n) :=
  fun i =>
    let y := ↑f ⟨↑i, ⋯⟩;
    let y' := ⟨↑y, ⋯⟩;
    let ys := cs y';
    if ?m.29421 i y y' ys ∈ ↑ys then ?m.29425 i y y' ys else y
hg1 : NSequence n k g1 := sorryAx (NSequence n k g1)
⊢ ⟨g1, hg1⟩ ∈ {g | ψ n k g = f}
no goals