internlm/Lean-Github huggingface dataset:
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inr.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
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
⊢ (if False then Color.blue else f' (Finset.subtype (fun a => a ≠ s) (s1 ∪ s2))) =
    if False then Color.blue else f' (Finset.subtype (fun a => a ≠ s) s1)
Tactic:
rw [Finset.subtype_union]
Proof state after:
case h.left.intro.intro.inr.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
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
⊢ (if False then Color.blue else f' (Finset.subtype (fun a => a ≠ s) s1 ∪ Finset.subtype (fun a => a ≠ s) s2)) =
    if False then Color.blue else f' (Finset.subtype (fun a => a ≠ s) s1)
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inr.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
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
⊢ (if False then Color.blue else f' (Finset.subtype (fun a => a ≠ s) s1 ∪ Finset.subtype (fun a => a ≠ s) s2)) =
    if False then Color.blue else f' (Finset.subtype (fun a => a ≠ s) s1)
Tactic:
apply hf1'
Proof state after:
case h.left.intro.intro.inr.inr.a
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
⊢ f' (Finset.subtype (fun a => a ≠ s) s1) = f' (Finset.subtype (fun a => a ≠ s) s2)
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inr.inr.a
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
⊢ f' (Finset.subtype (fun a => a ≠ s) s1) = f' (Finset.subtype (fun a => a ≠ s) s2)
Tactic:
simp [hss.1, hss.2, f] at hs12
Proof state after:
case h.left.intro.intro.inr.inr.a
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
s1 s2 : Finset S
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
hs12 : f' (Finset.subtype (fun a => ¬a = s) s1) = f' (Finset.subtype (fun a => ¬a = s) s2)
⊢ f' (Finset.subtype (fun a => a ≠ s) s1) = f' (Finset.subtype (fun a => a ≠ s) s2)
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inr.inr.a
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
s1 s2 : Finset S
h4 : f s1 = Color.red → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.red → f s1 = Color.red
h4' : f s2 = Color.red → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.red → f s2 = Color.red
hfs1 : ¬f s1 = Color.red
hss : s ∉ s1 ∧ s ∉ s2
hs12 : f' (Finset.subtype (fun a => ¬a = s) s1) = f' (Finset.subtype (fun a => ¬a = s) s2)
⊢ f' (Finset.subtype (fun a => a ≠ s) s1) = f' (Finset.subtype (fun a => a ≠ s) s2)
Tactic:
exact hs12
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.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
⊢ Fintype.card { a // f a = Color.red } = N
Tactic:
let b : { a : Finset S // f a = Color.red } → { a : Finset S' // f' a = Color.red } :=
    fun ⟨a, ha⟩ ↦ ⟨Finset.subtype _ a, by
       simp only [f] at ha
       split_ifs at ha
       exact ha
      ⟩
Proof state after:
case h.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, ⋯⟩
⊢ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.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, ⋯⟩
h3 : Function.Bijective b
⊢ Fintype.card { a // f a = Color.red } = N
Tactic:
rw [Fintype.card_of_bijective h3]
Proof state after:
case h.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, ⋯⟩
h3 : Function.Bijective b
⊢ Fintype.card { a // f' a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.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, ⋯⟩
h3 : Function.Bijective b
⊢ Fintype.card { a // f' a = Color.red } = N
Tactic:
exact hf2'
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
x✝ : { a // f a = Color.red }
a : Finset S
ha : f a = Color.red
⊢ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
Tactic:
simp only [f] at ha
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
x✝ : { a // f a = Color.red }
a : Finset S
ha : (if s ∈ a then Color.blue else f' (Finset.subtype (fun a => a ≠ s) a)) = Color.red
⊢ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
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
x✝ : { a // f a = Color.red }
a : Finset S
ha : (if s ∈ a then Color.blue else f' (Finset.subtype (fun a => a ≠ s) a)) = Color.red
⊢ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
Tactic:
split_ifs at ha
Proof state after:
case neg
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
x✝ : { a // f a = Color.red }
a : Finset S
h✝ : s ∉ a
ha : f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
⊢ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case neg
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
x✝ : { a // f a = Color.red }
a : Finset S
h✝ : s ∉ a
ha : f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
⊢ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
Tactic:
exact ha
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, ⋯⟩
⊢ 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
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.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
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