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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
x1 : S
hx1 : x1 ∈ x
hx1n : x1 = s
⊢ False
Tactic:
rw [hx1n] at hx1
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
x1 : S
hx1 : s ∈ x
hx1n : x1 = s
⊢ False
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
x1 : S
hx1 : s ∈ x
hx1n : x1 = s
⊢ False
Tactic:
exact h3 hx1
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
⊢ ∀ y1 ∈ y, y1 ≠ s
Tactic:
intro y1 hy1 hy1n
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
y1 : S
hy1 : y1 ∈ y
hy1n : y1 = s
⊢ False
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
y1 : S
hy1 : y1 ∈ y
hy1n : y1 = s
⊢ False
Tactic:
rw [hy1n] at hy1
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
y1 : S
hy1 : s ∈ y
hy1n : y1 = s
⊢ False
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
y1 : S
hy1 : s ∈ y
hy1n : y1 = s
⊢ False
Tactic:
exact h4 hy1
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
⊢ Function.Surjective b
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case right.mk
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ ∃ a, b a = ⟨x, hx⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case right.mk
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ ∃ a, b a = ⟨x, hx⟩
Tactic:
use ⟨Finset.map (Function.Embedding.subtype _) x,
     by simp [Finset.subtype_map_subtype, hx, 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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ b ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) x, ⋯⟩ = ⟨x, hx⟩
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ b ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) x, ⋯⟩ = ⟨x, hx⟩
Tactic:
unfold_let b
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ (fun x =>
        match x with
        | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩)
      ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) x, ⋯⟩ =
    ⟨x, hx⟩
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ (fun x =>
        match x with
        | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩)
      ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) x, ⋯⟩ =
    ⟨x, hx⟩
Tactic:
simp only [Subtype.mk.injEq]
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ Finset.subtype (fun a => a ≠ s) (Finset.map (Function.Embedding.subtype fun a => a ≠ s) x) = x
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ Finset.subtype (fun a => a ≠ s) (Finset.map (Function.Embedding.subtype fun a => a ≠ s) x) = x
Tactic:
exact Finset.subtype_map_subtype x
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
hl : N ≤ 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
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
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 // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S'
hx : f' x = Color.red
⊢ f (Finset.map (Function.Embedding.subtype fun a => a ≠ s) x) = Color.red
Tactic:
simp [Finset.subtype_map_subtype, hx, f]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ.inr
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
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
have hl : N - 2^k ≤ 2^k := by
  rw [pow_succ', two_mul] at hN
  exact Nat.sub_le_of_le_add hN
Proof state after:
case succ.inr
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, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N