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 }
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 _ _ _
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)
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)
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)
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)]
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)
h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ ∑ i : Fin n, (c i - 1)
⊢ ∑ i : Fin n, (c i - 1) = 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)
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
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)
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
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)
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]
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)
h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ ∑ i : Fin n, (c i - 1)
⊢ ∑ i : Fin n, (c i - 1) + n = k
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)
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
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)
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
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)
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]
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)
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
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)
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]
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)
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
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)
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)
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)
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
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)
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]
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)
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
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)
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
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)
h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ ∑ i : Fin n, (c i - 1)
⊢ 2 ≠ 1
Tactic:
norm_num
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)
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
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)
h1 : ∏ i : Fin n, 2 ^ (c i - 1) = 2 ^ ∑ i : Fin n, (c i - 1)
⊢ n = ∑ i : Fin n, 1
Tactic:
simp
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)
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
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)
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
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)
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)
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)
Scard' : Fintype.card S = 2 ^ (k - n)
⊢ Function.Bijective p
Tactic:
constructor
Proof 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
Theorem: Imo2008P5.claim
Proof 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
Proof 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
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof 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⟩
Proof 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⟩
Theorem: Imo2008P5.claim
Proof 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
Proof state after:
no goals
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
⊢ B.ncard * n = A.ncard
Tactic:
haveI hfa : Fintype ↑A := Set.Finite.fintype hA
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
⊢ B.ncard * n = A.ncard