internlm/Lean-Github huggingface dataset:
Theorem: Imo2008P5.claim
Proof 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⟩
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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']
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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]
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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)
Theorem: Imo2008P5.claim
Proof 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]
Proof 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)
Theorem: Imo2008P5.claim
Proof 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
Proof 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
Theorem: Imo2008P5.claim
Proof 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
Proof 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
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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]
Proof 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)