internlm/Lean-Github huggingface dataset:
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S
hy : s ∈ y
h5 : f y = Color.red
⊢ ∃ a, b a = Sum.inl ⟨y, hy⟩
Tactic:
use ⟨y, h5⟩
Proof state after:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S
hy : s ∈ y
h5 : f y = Color.red
⊢ b ⟨y, h5⟩ = Sum.inl ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S
hy : s ∈ y
h5 : f y = Color.red
⊢ b ⟨y, h5⟩ = Sum.inl ⟨y, hy⟩
Tactic:
simp only [ne_eq, dite_eq_ite, hy, dite_true, b]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S'
hy : f' y = Color.red
⊢ ∃ a, b a = Sum.inr ⟨y, hy⟩
Tactic:
use ⟨Finset.map (Function.Embedding.subtype _) y,
    by simp [Finset.subtype_map_subtype, hy, b, f]⟩
Proof state after:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S'
hy : f' y = Color.red
⊢ b ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) y, ⋯⟩ = Sum.inr ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S'
hy : f' y = Color.red
⊢ b ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) y, ⋯⟩ = Sum.inr ⟨y, hy⟩
Tactic:
simp [Finset.subtype_map_subtype, b, f]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : { a // s ∈ a } ⊕ { a' // f' a' = Color.red }
y : Finset S'
hy : f' y = Color.red
⊢ f (Finset.map (Function.Embedding.subtype fun a => a ≠ s) y) = Color.red
Tactic:
simp [Finset.subtype_map_subtype, hy, b, f]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N - 2 ^ k
f : Finset S → Color := fun x => if s ∈ x then Color.red else f' (Finset.subtype (fun a => a ≠ s) x)
h2 : ∀ (a : Finset S), f a = Color.blue ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.blue
h2' : ∀ (a : Finset S), f a = Color.red ↔ s ∈ a ∨ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // s ∈ a } ⊕ { a' // f' a' = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => if h : s ∈ a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
h3 : Function.Bijective b
⊢ Fintype.card { a // s ∈ a } = 2 ^ k
Tactic:
clear h3 b h2' h2 f hf2' hf1'
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
⊢ Fintype.card { a // s ∈ a } = 2 ^ k
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
⊢ Fintype.card { a // s ∈ a } = 2 ^ k
Tactic:
have h5 : Fintype.card (Finset S') = 2 ^ k := by rw [Fintype.card_finset, hs']
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
⊢ Fintype.card { a // s ∈ a } = 2 ^ k
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
⊢ Fintype.card { a // s ∈ a } = 2 ^ k
Tactic:
rw [lemma1]
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
⊢ Fintype.card { a // s ∉ a } = 2 ^ k
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
⊢ Fintype.card { a // s ∉ a } = 2 ^ k
Tactic:
let b : Finset S' → { a : Finset S // s ∉ a } :=
  fun a ↦ ⟨Finset.map (Function.Embedding.subtype _) a, by simp⟩
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
⊢ Fintype.card { a // s ∉ a } = 2 ^ k
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card { a // s ∉ a } = 2 ^ k
Tactic:
rw [←Fintype.card_of_bijective hb]
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card (Finset S') = 2 ^ k
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card (Finset S') = 2 ^ k
Tactic:
exact h5
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
⊢ Fintype.card (Finset S') = 2 ^ k
Tactic:
rw [Fintype.card_finset, hs']
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
a : Finset S'
⊢ s ∉ Finset.map (Function.Embedding.subtype fun a => a ≠ s) a
Tactic:
simp
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
⊢ Function.Bijective b
Tactic:
constructor
Proof state after:
case left
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
⊢ Function.Injective b

case right
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
⊢ Function.Surjective b
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
⊢ Function.Injective b
Tactic:
rintro x y hxy
Proof state after:
case left
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x y : Finset S'
hxy : b x = b y
⊢ x = y
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x y : Finset S'
hxy : b x = b y
⊢ x = y
Tactic:
simp only [Subtype.mk.injEq, Finset.map_inj, b] at hxy
Proof state after:
case left
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x y : Finset S'
hxy : x = y
⊢ x = y
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x y : Finset S'
hxy : x = y
⊢ x = y
Tactic:
exact hxy
Proof state after:
no goals