Theorem: Imo2008P5.claim (Compfiles/Imo2008P5.lean)

State before:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
let c : Fin n → ℕ := fun i ↦ Nat.card { j | f.val j = ⟨i, by omega⟩ }
State after:
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, ⋯⟩}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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, ⋯⟩}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have hcp : ∀ i : Fin n, 0 < c i := by sorry
State after:
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
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have hc : ∑ i : Fin n, c i = k := by sorry
State after:
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
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
let S : Type :=
  (i : Fin n) →
    {s : Finset { j : Fin k | f.val j = ⟨i, by omega⟩} // Even (Finset.card s) }
State after:
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 }
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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 }
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
let p : S → {g | ψ n k g = f} :=
  fun cs ↦
     let g1 :=
       fun (i : Fin k) ↦
         let y : Fin (2 * n) := f.val ⟨i, by omega⟩
         let y' : Fin n := ⟨y.val, by sorry⟩
         let ys : { s : Finset _ // Even s.card } := cs y'
         if ⟨i, by sorry⟩ ∈ ys.val then ⟨y.val + n, by sorry⟩ else y
     let hg1 := by sorry
     let hgg := by sorry
     ⟨⟨g1, hg1⟩, hgg⟩
State after:
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⟩
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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⟩
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have Scard : Fintype.card S = ∏ i : Fin n, 2 ^ (c i - 1) := by
  unfold_let S
  rw [Fintype.card_pi]
  apply Fintype.prod_congr
  intro a
  rw [even_subsets_card]
  norm_num
  congr
  sorry
State after:
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)
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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)
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have Scard' : Fintype.card S = 2^(k-n) := by
  rw [Scard]
  have h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ (∑ i : Fin n, (c i - 1)) :=
    Finset.prod_pow_eq_pow_sum _ _ _
  rw [h1, pow_right_inj zero_lt_two (by norm_num)]
  suffices ∑ i : Fin n, (c i - 1) + n = k - n + n by omega
  rw [Nat.sub_add_cancel hnk]
  have h2 : n = ∑ i : Fin n, 1 := by simp
  simp_rw [h2]
  rw [←Finset.sum_add_distrib]
  have h3 : ∀ x ∈ Finset.univ (α := Fin n), c x - 1 + 1 = c x := by
    intro x hx
    exact Nat.sub_add_cancel (hcp x)
  rw [Finset.sum_congr rfl h3]
  exact hc
State after:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have h2 : Fintype.card S = Fintype.card {g | ψ n k g = f} :=
  Fintype.card_of_bijective h1
State after:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
h2 : Fintype.card S = Fintype.card ↑{g | ψ n k g = f}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
h2 : Fintype.card S = Fintype.card ↑{g | ψ n k g = f}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
nth_rewrite 2 [←Nat.card_eq_fintype_card] at h2
State after:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
h2 : Fintype.card S = Nat.card ↑{g | ψ n k g = f}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
h2 : Fintype.card S = Nat.card ↑{g | ψ n k g = f}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
rw [Set.Nat.card_coe_set_eq] at h2
State after:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
h2 : Fintype.card S = {g | ψ n k g = f}.ncard
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)

State before:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
h1 : Function.Bijective p
h2 : Fintype.card S = {g | ψ n k g = f}.ncard
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
rw [←h2, Scard']
State after:
no goals

State before:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
i : Fin n
j : Fin k
⊢ ↑i < 2 * n
Tactic:
omega
State after:
no goals

State before:
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, ⋯⟩}
⊢ ∀ (i : Fin n), 0 < c i
Tactic:
sorry
State after:
no goals

State before:
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
⊢ ∑ i : Fin n, c i = k
Tactic:
sorry
State after:
no goals

State before:
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
i : Fin n
j : Fin k
⊢ ↑i < 2 * n
Tactic:
omega
State after:
no goals

State before:
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
i : Fin k
⊢ ↑i < k
Tactic:
omega
State after:
no goals

State before:
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
i : Fin k
y : Fin (2 * n) := ↑f ⟨↑i, ⋯⟩
⊢ ↑y < n
Tactic:
sorry
State after:
no goals

State before:
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
i : Fin k
y : Fin (2 * n) := ↑f ⟨↑i, ⋯⟩
y' : Fin n := ⟨↑y, ⋯⟩
ys : { s // Even s.card } := cs y'
⊢ i ∈ {j | ↑f j = ⟨↑y', ⋯⟩}
Tactic:
sorry
State after:
no goals

State before:
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
i : Fin k
y : Fin (2 * n) := ↑f ⟨↑i, ⋯⟩
y' : Fin n := ⟨↑y, ⋯⟩
ys : { s // Even s.card } := cs y'
⊢ ↑y + n < 2 * n
Tactic:
sorry
State after:
no goals

State before:
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
⊢ NSequence n k g1
Tactic:
sorry
State after:
no goals

State before:
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}
Tactic:
sorry
State after:
no goals

State before:
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⟩
⊢ Fintype.card S = ∏ i : Fin n, 2 ^ (c i - 1)
Tactic:
unfold_let S
State after:
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⟩
⊢ Fintype.card ((i : Fin n) → { s // Even s.card }) = ∏ i : Fin n, 2 ^ (c i - 1)

State before:
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⟩
⊢ Fintype.card ((i : Fin n) → { s // Even s.card }) = ∏ i : Fin n, 2 ^ (c i - 1)
Tactic:
rw [Fintype.card_pi]
State after:
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⟩
⊢ ∏ i : Fin n, Fintype.card { s // Even s.card } = ∏ i : Fin n, 2 ^ (c i - 1)

State before:
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⟩
⊢ ∏ i : Fin n, Fintype.card { s // Even s.card } = ∏ i : Fin n, 2 ^ (c i - 1)
Tactic:
apply Fintype.prod_congr
State after:
case h
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⟩
⊢ ∀ (a : Fin n), Fintype.card { s // Even s.card } = 2 ^ (c a - 1)

State before:
case h
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⟩
⊢ ∀ (a : Fin n), Fintype.card { s // Even s.card } = 2 ^ (c a - 1)
Tactic:
intro a
State after:
case h
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⟩
a : Fin n
⊢ Fintype.card { s // Even s.card } = 2 ^ (c a - 1)

State before:
case h
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⟩
a : Fin n
⊢ Fintype.card { s // Even s.card } = 2 ^ (c a - 1)
Tactic:
rw [even_subsets_card]
State after:
case h
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⟩
a : Fin n
⊢ 2 ^ (Fintype.card ↑{j | ↑f j = ⟨↑a, ⋯⟩} - 1) = 2 ^ (c a - 1)

State before:
case h
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⟩
a : Fin n
⊢ 2 ^ (Fintype.card ↑{j | ↑f j = ⟨↑a, ⋯⟩} - 1) = 2 ^ (c a - 1)
Tactic:
norm_num
State after:
case h
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⟩
a : Fin n
⊢ (Finset.filter (fun x => ↑f x = ⟨↑a, ⋯⟩) Finset.univ).card - 1 = c a - 1

State before:
case h
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⟩
a : Fin n
⊢ (Finset.filter (fun x => ↑f x = ⟨↑a, ⋯⟩) Finset.univ).card - 1 = c a - 1
Tactic:
congr
State after:
case h.e_a
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⟩
a : Fin n
⊢ (Finset.filter (fun x => ↑f x = ⟨↑a, ⋯⟩) Finset.univ).card = c a

State before:
case h.e_a
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⟩
a : Fin n
⊢ (Finset.filter (fun x => ↑f x = ⟨↑a, ⋯⟩) Finset.univ).card = c a
Tactic:
sorry
State after:
no goals

State before:
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)
⊢ Fintype.card S = 2 ^ (k - n)
Tactic:
rw [Scard]
State after:
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)
⊢ ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ (k - n)

State before:
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)
⊢ ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ (k - n)
Tactic:
have h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ (∑ i : Fin n, (c i - 1)) :=
  Finset.prod_pow_eq_pow_sum _ _ _
State after:
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)
⊢ ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ (k - n)

State before:
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)
⊢ ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ (k - n)
Tactic:
rw [h1, pow_right_inj zero_lt_two (by norm_num)]
State after:
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)
⊢ ∑ i : Fin n, (c i - 1) = k - n

State before:
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)
⊢ ∑ i : Fin n, (c i - 1) = k - n
Tactic:
suffices ∑ i : Fin n, (c i - 1) + n = k - n + n by omega
State after:
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)
⊢ ∑ i : Fin n, (c i - 1) + n = k - n + n

State before:
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)
⊢ ∑ i : Fin n, (c i - 1) + n = k - n + n
Tactic:
rw [Nat.sub_add_cancel hnk]
State after:
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)
⊢ ∑ i : Fin n, (c i - 1) + n = k

State before:
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)
⊢ ∑ i : Fin n, (c i - 1) + n = k
Tactic:
have h2 : n = ∑ i : Fin n, 1 := by simp
State after:
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
⊢ ∑ i : Fin n, (c i - 1) + n = k

State before:
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
⊢ ∑ i : Fin n, (c i - 1) + n = k
Tactic:
simp_rw [h2]
State after:
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
⊢ ∑ i : Fin n, (c i - 1) + ∑ i : Fin n, 1 = k

State before:
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
⊢ ∑ i : Fin n, (c i - 1) + ∑ i : Fin n, 1 = k
Tactic:
rw [←Finset.sum_add_distrib]
State after:
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
⊢ ∑ x : Fin n, (c x - 1 + 1) = k

State before:
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
⊢ ∑ x : Fin n, (c x - 1 + 1) = k
Tactic:
have h3 : ∀ x ∈ Finset.univ (α := Fin n), c x - 1 + 1 = c x := by
  intro x hx
  exact Nat.sub_add_cancel (hcp x)
State after:
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 - 1 + 1) = k

State before:
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 - 1 + 1) = k
Tactic:
rw [Finset.sum_congr rfl h3]
State after:
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

State before:
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
Tactic:
exact hc
State after:
no goals

State before:
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)
⊢ 2 ≠ 1
Tactic:
norm_num
State after:
no goals

State before:
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)
this : ∑ i : Fin n, (c i - 1) + n = k - n + n
⊢ ∑ i : Fin n, (c i - 1) = k - n
Tactic:
omega
State after:
no goals

State before:
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)
⊢ n = ∑ i : Fin n, 1
Tactic:
simp
State after:
no goals

State before:
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
⊢ ∀ x ∈ Finset.univ, c x - 1 + 1 = c x
Tactic:
intro x hx
State after:
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
x : Fin n
hx : x ∈ Finset.univ
⊢ c x - 1 + 1 = c x

State before:
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
x : Fin n
hx : x ∈ Finset.univ
⊢ c x - 1 + 1 = c x
Tactic:
exact Nat.sub_add_cancel (hcp x)
State after:
no goals

State before:
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ Function.Bijective p
Tactic:
constructor
State after:
case left
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ Function.Injective p

case right
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ Function.Surjective p

State before:
case left
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ Function.Injective p
Tactic:
intro x y hxy
State after:
case left
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)
Scard' : Fintype.card S = 2 ^ (k - n)
x y : S
hxy : p x = p y
⊢ x = y

State before:
case left
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)
Scard' : Fintype.card S = 2 ^ (k - n)
x y : S
hxy : p x = p y
⊢ x = y
Tactic:
sorry
State after:
no goals

State before:
case right
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ Function.Surjective p
Tactic:
rintro ⟨g, hg⟩
State after:
case right.mk
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)
Scard' : Fintype.card S = 2 ^ (k - n)
g : { f // NSequence n k f }
hg : g ∈ {g | ψ n k g = f}
⊢ ∃ a, p a = ⟨g, hg⟩

State before:
case right.mk
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)
Scard' : Fintype.card S = 2 ^ (k - n)
g : { f // NSequence n k f }
hg : g ∈ {g | ψ n k g = f}
⊢ ∃ a, p a = ⟨g, hg⟩
Tactic:
sorry
State after:
no goals