internlm/Lean-Github huggingface dataset:
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.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
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
s1 s2 : Finset S
hs12 : f s1 = f s2
⊢ f (s1 ∪ s2) = f s1
Tactic:
obtain ⟨h4, _⟩ := h2 s1
Proof state after:
case h.left.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
⊢ f (s1 ∪ s2) = f s1
Tactic:
obtain ⟨h4', _⟩ := h2 s2
Proof state after:
case h.left.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inl
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
⊢ f (s1 ∪ s2) = f s1
Tactic:
obtain ⟨h6, h7⟩ := h4 hfs1
Proof state after:
case h.left.intro.intro.inl.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inl.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
⊢ f (s1 ∪ s2) = f s1
Tactic:
have hfs2 : f s2 = Color.blue := by rwa [hs12] at hfs1
Proof state after:
case h.left.intro.intro.inl.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inl.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
⊢ f (s1 ∪ s2) = f s1
Tactic:
obtain ⟨h6', h7'⟩ := h4' hfs2
Proof state after:
case h.left.intro.intro.inl.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
h6' : s ∉ s2
h7' : f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inl.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
h6' : s ∉ s2
h7' : f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
⊢ f (s1 ∪ s2) = f s1
Tactic:
rw [←h7] at h7'
Proof state after:
case h.left.intro.intro.inl.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
h6' : s ∉ s2
h7' : f' (Finset.subtype (fun a => a ≠ s) s2) = f' (Finset.subtype (fun a => a ≠ s) s1)
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inl.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
h6' : s ∉ s2
h7' : f' (Finset.subtype (fun a => a ≠ s) s2) = f' (Finset.subtype (fun a => a ≠ s) s1)
⊢ f (s1 ∪ s2) = f s1
Tactic:
have h8 := hf1' _ _ h7'
Proof state after:
case h.left.intro.intro.inl.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
h6' : s ∉ s2
h7' : f' (Finset.subtype (fun a => a ≠ s) s2) = f' (Finset.subtype (fun a => a ≠ s) s1)
h8 :
  f' (Finset.subtype (fun a => a ≠ s) s2 ∪ Finset.subtype (fun a => a ≠ s) s1) = f' (Finset.subtype (fun a => a ≠ s) s2)
⊢ f (s1 ∪ s2) = f s1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h.left.intro.intro.inl.intro.intro
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
hfs2 : f s2 = Color.blue
h6' : s ∉ s2
h7' : f' (Finset.subtype (fun a => a ≠ s) s2) = f' (Finset.subtype (fun a => a ≠ s) s1)
h8 :
  f' (Finset.subtype (fun a => a ≠ s) s2 ∪ Finset.subtype (fun a => a ≠ s) s1) = f' (Finset.subtype (fun a => a ≠ s) s1)
⊢ f' (Finset.subtype (fun a => ¬a = s) s2 ∪ Finset.subtype (fun a => ¬a = s) s1) =
    f' (Finset.subtype (fun a => ¬a = s) s1)
Tactic:
exact h8
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
s1 s2 : Finset S
hs12 : f s1 = f s2
h4 : f s1 = Color.blue → s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
mpr✝¹ : s ∉ s1 ∧ f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue → f s1 = Color.blue
h4' : f s2 = Color.blue → s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue
mpr✝ : s ∉ s2 ∧ f' (Finset.subtype (fun a => a ≠ s) s2) = Color.blue → f s2 = Color.blue
hfs1 : f s1 = Color.blue
h6 : s ∉ s1
h7 : f' (Finset.subtype (fun a => a ≠ s) s1) = Color.blue
⊢ f s2 = Color.blue
Tactic:
rwa [hs12] at hfs1
Proof state after:
no goals