FormalConjectures.ErdosProblems.«602»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 602

Reference: erdosproblems.com/602

open Setnamespace Erdos602

A set A ⊆ α is monochromatic under a 2-colouring f : α → Fin 2 if all elements of A receive the same colour.

def IsMonochromatic {α : Type*} (f : α → Fin 2) (A : Set α) : Prop :=
  ∀ x ∈ A, ∀ y ∈ A, f x = f y

A family (A_i)_{i ∈ I} of subsets of α has Property B if there exists a 2-colouring f : α → Fin 2 such that no A_i is monochromatic.

def HasPropertyB {α : Type*} (I : Type*) (A : I → Set α) : Prop :=
  ∃ f : α → Fin 2, ∀ i, ¬IsMonochromatic f (A i)

Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?

Formally: let α be any type, let (A_i)_{i ∈ I} be a family of countably infinite subsets of α such that for all i ≠ j, the intersection A_i ∩ A_j is finite and |A_i ∩ A_j| ≠ 1. Does there exist a 2-colouring f : α → Fin 2 such that no A_i is monochromatic?

This is an open question about Property B for almost-disjoint families with a forbidden intersection size of 1.

Note: This generalises the formulation in which the ground set is ℕ. Since every countably infinite set is in bijection with ℕ, the two formulations are equivalent, but working over an arbitrary ground type makes the statement apply immediately to, e.g., almost-disjoint families of countable subsets of an uncountable space.

@[category research open, AMS 3 5]
theorem erdos_602 : answer(sorry) ↔
    ∀ {α : Type*} {I : Type*} (A : I → Set α),
      (∀ i, (A i).Countable ∧ (A i).Infinite) →
      (∀ i j, i ≠ j → (A i ∩ A j).Finite) →
      (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) →
      HasPropertyB I A := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Countable ∧ (A i).Infinite) →
      (∀ (i j : I), i ≠ j → (A i ∩ A j).Finite) → (∀ (i j : I), i ≠ j → (A i ∩ A j).ncard ≠ 1) → HasPropertyB I A
  sorryAll goals completed! 🐙

Trivial case: pairwise disjoint families.

If the A_i are pairwise disjoint (all intersections are empty, which in particular satisfies |A_i ∩ A_j| ≠ 1), then Property B holds trivially.

Proof sketch: Since each A_i is infinite, it has (at least) two distinct elements a_i and b_i. We can define a colouring that assigns colour 0 to a_i and colour 1 to b_i for each i (using disjointness, these choices don't conflict), and extend arbitrarily elsewhere. Then no A_i is monochromatic.


@[category research solved, AMS 3 5]
theorem erdos_602.variants.disjoint : answer(True) ↔
    ∀ {α : Type*} {I : Type*} (A : I → Set α),
      (∀ i, (A i).Infinite) →
      (∀ i j, i ≠ j → Disjoint (A i) (A j)) →
      HasPropertyB I A := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I A
  show True ↔ _⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I A
  simp only [true_iff]⊢ ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
  (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I A
  intro α I A hInfinite hDisjointα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)⊢ HasPropertyB I A
  -- For each i, pick two distinct elements a_fn i, b_fn i ∈ A i.
  have ha_b : ∀ i, ∃ a b : α, a ∈ A i ∧ b ∈ A i ∧ a ≠ b := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
    intro iα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:I⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
    obtain ⟨a, ha⟩ := (hInfinite i).nonemptyα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A i⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
    have hA2 : (A i \ {a}).Nonempty := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A ihA2:(A i \ {a}).Nonempty⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
      apply Set.Infinite.nonemptyα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A i⊢ (A i \ {a}).Infiniteα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A ihA2:(A i \ {a}).Nonempty⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
      exact (hInfinite i).sdiff (Set.finite_singleton a)α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A ihA2:(A i \ {a}).Nonempty⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A ihA2:(A i \ {a}).Nonempty⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
    obtain ⟨b, hbA, hba⟩ := hA2α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A ib:αhbA:b ∈ A ihba:b ∉ {a}⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
    simp only [Set.mem_singleton_iff] at hbaα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)i:Ia:αha:a ∈ A ib:αhbA:b ∈ A ihba:¬b = a⊢ ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
    exact ⟨a, b, ha, hbA, fun h => hba h.symm⟩α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)ha_b:∀ (i : I), ∃ a b, a ∈ A i ∧ b ∈ A i ∧ a ≠ b⊢ HasPropertyB I A
  choose a_fn b_fn ha_mem hb_mem hab_ne using ha_bα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn i⊢ HasPropertyB I A
  -- Key property: a_fn i ≠ b_fn j for any j.
  have key : ∀ i j, a_fn i ≠ b_fn j := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
    intro i j hajα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
    by_cases hij : i = jposα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:i = j⊢ Falsenegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
    ·posα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:i = j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A subst hijposα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ihaj:a_fn i = b_fn i⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A; exact hab_ne i hajAll goals completed! 🐙α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
    ·negα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A have hdisj := hDisjoint i j hijnegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:Disjoint (A i) (A j)⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
      rw [Set.disjoint_leftnegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A j⊢ Falsenegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A] at hdisjnegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
      have hbj : b_fn j ∈ A j := hb_mem jnegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A jhbj:b_fn j ∈ A j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
      rw [← hajnegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A jhbj:a_fn i ∈ A j⊢ Falsenegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A jhbj:a_fn i ∈ A j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A] at hbjnegα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ii:Ij:Ihaj:a_fn i = b_fn jhij:¬i = jhdisj:∀ ⦃a : α⦄, a ∈ A i → a ∉ A jhbj:a_fn i ∈ A j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
      exact hdisj (ha_mem i) hbjα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn j⊢ HasPropertyB I A
  -- Define colouring: f n = 1 iff n = b_fn i for some i, else 0.
  -- Use Classical.propDecidable for the existential over I.
  classical
  let f : α → Fin 2 := fun n => if ∃ i, n = b_fn i then 1 else 0α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0⊢ HasPropertyB I A
  refine ⟨f, fun i => ?_⟩α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:I⊢ ¬IsMonochromatic f (A i)
  -- Show A i is not monochromatic under f.
  intro hMonoα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)⊢ False
  -- f (a_fn i) = 0: ¬ ∃ j, a_fn i = b_fn j.
  have hfa : f (a_fn i) = 0 := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ False
    simp only [f]α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)⊢ (if ∃ i_1, a_fn i = b_fn i_1 then 1 else 0) = 0α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ False
    rw [if_negα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)⊢ 0 = 0hncα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)⊢ ¬∃ i_1, a_fn i = b_fn i_1hncα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)⊢ ¬∃ i_1, a_fn i = b_fn i_1α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ False]hncα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)⊢ ¬∃ i_1, a_fn i = b_fn i_1α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ False
    rintro ⟨j, hj⟩hncα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)j:Ihj:a_fn i = b_fn j⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ False
    exact key i j hjα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ False
  -- f (b_fn i) = 1: witnessed by i itself.
  have hfb : f (b_fn i) = 1 := by⊢ True ↔
  ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α),
    (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I Aα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1⊢ False
    simp only [f]α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ (if ∃ i_1, b_fn i = b_fn i_1 then 1 else 0) = 1α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1⊢ False
    rw [if_pos ⟨i, rfl⟩α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0⊢ 1 = 1α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1⊢ False]α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1⊢ False
  -- hMono says f is constant on A i, but f (a_fn i) = 0 ≠ 1 = f (b_fn i).
  have hne := hMono (a_fn i) (ha_mem i) (b_fn i) (hb_mem i)α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:f (a_fn i) = f (b_fn i)⊢ False
  rw [hfa,α:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:0 = f (b_fn i)⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:0 = 1⊢ False hfbα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:0 = 1⊢ Falseα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:0 = 1⊢ False] at hneα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:0 = 1⊢ False
  exact absurd hne (byα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).InfinitehDisjoint:∀ (i j : I), i ≠ j → Disjoint (A i) (A j)a_fn:I → αb_fn:I → αha_mem:∀ (i : I), a_fn i ∈ A ihb_mem:∀ (i : I), b_fn i ∈ A ihab_ne:∀ (i : I), a_fn i ≠ b_fn ikey:∀ (i j : I), a_fn i ≠ b_fn jf:α → Fin 2 := fun n ↦ if ∃ i, n = b_fn i then 1 else 0i:IhMono:IsMonochromatic f (A i)hfa:f (a_fn i) = 0hfb:f (b_fn i) = 1hne:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)

Countable index set case.

If the index set is countable, the answer is yes, and the intersection condition is unnecessary. This is Bernstein's Lemma: every countable system of infinite sets has Property B.

@[category research solved, AMS 3 5]
theorem erdos_602.variants.countable_index : answer(True) ↔
    ∀ {α : Type*} (A : ℕ → Set α),
      (∀ i, (A i).Countable ∧ (A i).Infinite) →
      (∀ i j, i ≠ j → (A i ∩ A j).Finite) →
      (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) →
      HasPropertyB ℕ A := by⊢ True ↔
  ∀ {α : Type u_1} (A : ℕ → Set α),
    (∀ (i : ℕ), (A i).Countable ∧ (A i).Infinite) →
      (∀ (i j : ℕ), i ≠ j → (A i ∩ A j).Finite) → (∀ (i j : ℕ), i ≠ j → (A i ∩ A j).ncard ≠ 1) → HasPropertyB ℕ A
  sorryAll goals completed! 🐙

Intersections of size ≥ 2 suffice.

For a single countably infinite set A ⊆ α, there trivially exists a 2-colouring of α that makes A non-monochromatic: since A is infinite, it has two distinct elements, so any colouring that assigns them different colours works.


@[category textbook, AMS 3]
theorem erdos_602.variants.single_set {α : Type*} (A : Set α) (hA : A.Infinite) :
    ∃ f : α → Fin 2, ¬IsMonochromatic f A := byα:Type u_1A:Set αhA:A.Infinite⊢ ∃ f, ¬IsMonochromatic f A
  classical
  -- A is infinite, so it has at least two distinct elements.
  obtain ⟨a, ha⟩ := hA.nonemptyα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ A⊢ ∃ f, ¬IsMonochromatic f A
  -- Pick a second element different from a.
  have hA2 : (A \ {a}).Nonempty := byα:Type u_1A:Set αhA:A.Infinite⊢ ∃ f, ¬IsMonochromatic f Aα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ AhA2:(A \ {a}).Nonempty⊢ ∃ f, ¬IsMonochromatic f A
    apply Set.Infinite.nonemptyα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ A⊢ (A \ {a}).Infiniteα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ AhA2:(A \ {a}).Nonempty⊢ ∃ f, ¬IsMonochromatic f A
    exact hA.sdiff (Set.finite_singleton a)α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ AhA2:(A \ {a}).Nonempty⊢ ∃ f, ¬IsMonochromatic f Aα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ AhA2:(A \ {a}).Nonempty⊢ ∃ f, ¬IsMonochromatic f A
  obtain ⟨b, hbA⟩ := hA2α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ A \ {a}⊢ ∃ f, ¬IsMonochromatic f A
  simp only [Set.mem_sdiff, Set.mem_singleton_iff] at hbAα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ A ∧ ¬b = a⊢ ∃ f, ¬IsMonochromatic f A
  obtain ⟨hbA, hba⟩ := hbAα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = a⊢ ∃ f, ¬IsMonochromatic f A
  -- Colour a with 0, b with 1, everything else with 0.
  refine ⟨fun n => if n = b then 1 else 0, ?_⟩α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = a⊢ ¬IsMonochromatic (fun n ↦ if n = b then 1 else 0) A
  -- The colouring is not monochromatic on A since f(a) = 0 ≠ 1 = f(b).
  intro hMonoα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) A⊢ False
  have h0 : (fun n => if n = b then (1 : Fin 2) else 0) a = 0 := byα:Type u_1A:Set αhA:A.Infinite⊢ ∃ f, ¬IsMonochromatic f Aα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0⊢ False
    simp only [ite_eq_right_iff]α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) A⊢ a = b → 1 = 0α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0⊢ False
    intro hα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah:a = b⊢ 1 = 0α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0⊢ False
    exact absurd h (Ne.symm hba)α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0⊢ Falseα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0⊢ False
  have h1 : (fun n => if n = b then (1 : Fin 2) else 0) b = 1 := byα:Type u_1A:Set αhA:A.Infinite⊢ ∃ f, ¬IsMonochromatic f Aα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1⊢ False
    simpα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1⊢ Falseα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1⊢ False
  have := hMono a ha b hbAα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:(fun n ↦ if n = b then 1 else 0) a = (fun n ↦ if n = b then 1 else 0) b⊢ False
  rw [h0,α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:0 = (fun n ↦ if n = b then 1 else 0) b⊢ Falseα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:0 = 1⊢ False h1α:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:0 = 1⊢ Falseα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:0 = 1⊢ False] at thisα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:0 = 1⊢ False
  exact absurd this (byα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ Ab:αhbA:b ∈ Ahba:¬b = ahMono:IsMonochromatic (fun n ↦ if n = b then 1 else 0) Ah0:(fun n ↦ if n = b then 1 else 0) a = 0h1:(fun n ↦ if n = b then 1 else 0) b = 1this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)

Empty index set.

If the index set I is empty (has no elements), then Property B holds vacuously: any 2-colouring works, since there are no sets to be made non-monochromatic.

@[category textbook, AMS 3]
theorem erdos_602.variants.empty_index {α : Type*} :
    ∀ (A : PEmpty → Set α),
      (∀ i, (A i).Infinite) →
      HasPropertyB PEmpty A := byα:Type u_1⊢ ∀ (A : PEmpty.{u_2 + 1} → Set α), (∀ (i : PEmpty.{u_2 + 1}), (A i).Infinite) → HasPropertyB PEmpty.{u_2 + 1} A
  intro A _hInfiniteα:Type u_1A:PEmpty.{u_2 + 1} → Set α_hInfinite:∀ (i : PEmpty.{u_2 + 1}), (A i).Infinite⊢ HasPropertyB PEmpty.{u_2 + 1} A
  exact ⟨fun _ => 0, fun i => i.elim⟩All goals completed! 🐙

Unique index set.

If the index set has exactly one element (i.e., [Unique I]), then Property B holds: any 2-colouring that makes the single set A (default : I) non-monochromatic works. This follows from the single-set case.


@[category textbook, AMS 3]
theorem erdos_602.variants.unique_index {α : Type*} (I : Type*) [Unique I]
    (A : I → Set α) (hInfinite : ∀ i, (A i).Infinite) :
    HasPropertyB I A := byα:Type u_1I:Type u_2inst✝:Unique IA:I → Set αhInfinite:∀ (i : I), (A i).Infinite⊢ HasPropertyB I A
  -- Use single_set to get a colouring making A (default) non-monochromatic.
  obtain ⟨f, hf⟩ := erdos_602.variants.single_set (A default) (hInfinite default)α:Type u_1I:Type u_2inst✝:Unique IA:I → Set αhInfinite:∀ (i : I), (A i).Infinitef:α → Fin 2hf:¬IsMonochromatic f (A default)⊢ HasPropertyB I A
  refine ⟨f, fun i => ?_⟩α:Type u_1I:Type u_2inst✝:Unique IA:I → Set αhInfinite:∀ (i : I), (A i).Infinitef:α → Fin 2hf:¬IsMonochromatic f (A default)i:I⊢ ¬IsMonochromatic f (A i)
  -- Every i equals default by uniqueness.
  rw [Unique.eq_default iα:Type u_1I:Type u_2inst✝:Unique IA:I → Set αhInfinite:∀ (i : I), (A i).Infinitef:α → Fin 2hf:¬IsMonochromatic f (A default)i:I⊢ ¬IsMonochromatic f (A default)α:Type u_1I:Type u_2inst✝:Unique IA:I → Set αhInfinite:∀ (i : I), (A i).Infinitef:α → Fin 2hf:¬IsMonochromatic f (A default)i:I⊢ ¬IsMonochromatic f (A default)]α:Type u_1I:Type u_2inst✝:Unique IA:I → Set αhInfinite:∀ (i : I), (A i).Infinitef:α → Fin 2hf:¬IsMonochromatic f (A default)i:I⊢ ¬IsMonochromatic f (A default)
  exact hfAll goals completed! 🐙

Two infinite sets with pairwise intersection of size ≠ 1.

If the family consists of exactly two countably infinite sets A₀ and A₁ with |A₀ ∩ A₁| ≠ 1 (and finite), then Property B holds.

Proof sketch:

If A₀ ∩ A₁ = ∅: the sets are disjoint. Pick distinct a, b ∈ A₀ and distinct c, d ∈ A₁. Colour b and c with 1, everything else with 0. Then A₀ has a (colour 0) and b (colour 1), and A₁ has c (colour 1) and d (colour 0), so neither is monochromatic.

If |A₀ ∩ A₁| ≥ 2: the intersection contains two distinct points x and y. Assign x colour 0 and y colour 1. Both A₀ and A₁ contain x and y, so neither is monochromatic.


@[category research solved, AMS 3 5]
theorem erdos_602.variants.two_sets : answer(True) ↔
    ∀ {α : Type*} (A : Fin 2 → Set α),
      (∀ i, (A i).Infinite) →
      (A 0 ∩ A 1).Finite →
      Set.ncard (A 0 ∩ A 1) ≠ 1 →
      HasPropertyB (Fin 2) A := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) A
  show True ↔ _⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) A
  simp only [true_iff]⊢ ∀ {α : Type u_1} (A : Fin 2 → Set α),
  (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) A
  intro α A hInfinite hFin hNcardα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1⊢ HasPropertyB (Fin 2) A
  classical
  -- Case split: intersection empty or size ≥ 2.
  by_cases hEmpty : (A 0 ∩ A 1) = ∅posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅⊢ HasPropertyB (Fin 2) Anegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅⊢ HasPropertyB (Fin 2) A
  ·posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅⊢ HasPropertyB (Fin 2) A -- Disjoint case: A 0 and A 1 are disjoint.
    -- Pick distinct a, b from A 0.
    obtain ⟨a, ha0⟩ := (hInfinite 0).nonemptyposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0⊢ HasPropertyB (Fin 2) A
    have hA0' : (A 0 \ {a}).Nonempty :=
      Set.Infinite.nonempty ((hInfinite 0).sdiff (Set.finite_singleton a))posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0hA0':(A 0 \ {a}).Nonempty⊢ HasPropertyB (Fin 2) A
    obtain ⟨b, hbA0, hba⟩ := hA0'posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:b ∉ {a}⊢ HasPropertyB (Fin 2) A
    simp only [Set.mem_singleton_iff] at hbaposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = a⊢ HasPropertyB (Fin 2) A
    -- Pick distinct c, d from A 1.
    obtain ⟨c, hc1⟩ := (hInfinite 1).nonemptyposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1⊢ HasPropertyB (Fin 2) A
    have hA1' : (A 1 \ {c}).Nonempty :=
      Set.Infinite.nonempty ((hInfinite 1).sdiff (Set.finite_singleton c))posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1hA1':(A 1 \ {c}).Nonempty⊢ HasPropertyB (Fin 2) A
    obtain ⟨d, hd1, hdc⟩ := hA1'posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:d ∉ {c}⊢ HasPropertyB (Fin 2) A
    simp only [Set.mem_singleton_iff] at hdcposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = c⊢ HasPropertyB (Fin 2) A
    -- Disjointness facts: A 0 and A 1 are disjoint.
    have hDisj : ∀ x, x ∈ A 0 → x ∉ A 1 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Aposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) A
      intro x hx0 hx1α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = cx:αhx0:x ∈ A 0hx1:x ∈ A 1⊢ Falseposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) A
      have hmem : x ∈ A 0 ∩ A 1 := ⟨hx0, hx1⟩α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = cx:αhx0:x ∈ A 0hx1:x ∈ A 1hmem:x ∈ A 0 ∩ A 1⊢ Falseposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) A
      rw [hEmptyα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = cx:αhx0:x ∈ A 0hx1:x ∈ A 1hmem:x ∈ ∅⊢ Falseα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = cx:αhx0:x ∈ A 0hx1:x ∈ A 1hmem:x ∈ ∅⊢ Falseposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) A] at hmemα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = cx:αhx0:x ∈ A 0hx1:x ∈ A 1hmem:x ∈ ∅⊢ Falseposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) A
      exact hmemposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) Aposα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1⊢ HasPropertyB (Fin 2) A
    have hb_ne_c : b ≠ c := fun h => hDisj b hbA0 (h ▸ hc1)posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ c⊢ HasPropertyB (Fin 2) A
    have hb_ne_d : b ≠ d := fun h => hDisj b hbA0 (h ▸ hd1)posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ d⊢ HasPropertyB (Fin 2) A
    have ha_ne_c : a ≠ c := fun h => hDisj a ha0 (h ▸ hc1)posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ c⊢ HasPropertyB (Fin 2) A
    -- Colour b with 1, c with 1, everything else with 0.
    -- A 0: f(a) = 0 (a ≠ b, a ≠ c), f(b) = 1. Non-mono.
    -- A 1: f(c) = 1, f(d) = 0 (d ≠ b, d ≠ c). Non-mono.
    refine ⟨fun n => if n = b ∨ n = c then 1 else 0, fun i => ?_⟩posα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ ci:Fin 2⊢ ¬IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A i)
    fin_cases ipos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ c⊢ ¬IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))pos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ c⊢ ¬IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))
    ·pos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ c⊢ ¬IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩)) -- A 0 is not monochromatic: f(a) = 0 ≠ 1 = f(b).
      intro hMonopos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))⊢ False
      have hfa : (fun n => if n = b ∨ n = c then (1 : Fin 2) else 0) a = 0 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Apos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0⊢ False
        simp [show a ≠ b from fun h => hba h.symm, ha_ne_c]pos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0⊢ False
      have hfb : (fun n => if n = b ∨ n = c then (1 : Fin 2) else 0) b = 1 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Apos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1⊢ False simppos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1⊢ False
      have := hMono a ha0 b hbA0pos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = (fun n ↦ if n = b ∨ n = c then 1 else 0) b⊢ False
      rw [hfa,pos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:0 = (fun n ↦ if n = b ∨ n = c then 1 else 0) b⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:0 = 1⊢ False hfbpos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:0 = 1⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:0 = 1⊢ False] at thispos.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:0 = 1⊢ False; exact absurd this (byα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfa:(fun n ↦ if n = b ∨ n = c then 1 else 0) a = 0hfb:(fun n ↦ if n = b ∨ n = c then 1 else 0) b = 1this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)
    ·pos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ c⊢ ¬IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩)) -- A 1 is not monochromatic: f(c) = 1 ≠ 0 = f(d).
      intro hMonopos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))⊢ False
      have hfc : (fun n => if n = b ∨ n = c then (1 : Fin 2) else 0) c = 1 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Apos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1⊢ False simppos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1⊢ False
      have hfd : (fun n => if n = b ∨ n = c then (1 : Fin 2) else 0) d = 0 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Apos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0⊢ False
        simp [hb_ne_d.symm, hdc]pos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0⊢ False
      have := hMono c hc1 d hd1pos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = (fun n ↦ if n = b ∨ n = c then 1 else 0) d⊢ False
      rw [hfc,pos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:1 = (fun n ↦ if n = b ∨ n = c then 1 else 0) d⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:1 = 0⊢ False hfdpos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:1 = 0⊢ Falsepos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:1 = 0⊢ False] at thispos.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:1 = 0⊢ False; exact absurd this (byα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:A 0 ∩ A 1 = ∅a:αha0:a ∈ A 0b:αhbA0:b ∈ A 0hba:¬b = ac:αhc1:c ∈ A 1d:αhd1:d ∈ A 1hdc:¬d = chDisj:∀ x ∈ A 0, x ∉ A 1hb_ne_c:b ≠ chb_ne_d:b ≠ dha_ne_c:a ≠ chMono:IsMonochromatic (fun n ↦ if n = b ∨ n = c then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfc:(fun n ↦ if n = b ∨ n = c then 1 else 0) c = 1hfd:(fun n ↦ if n = b ∨ n = c then 1 else 0) d = 0this:1 = 0⊢ ¬1 = 0 decideAll goals completed! 🐙)
  ·negα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅⊢ HasPropertyB (Fin 2) A -- Intersection has size ≥ 2.
    have hge2 : 1 < Set.ncard (A 0 ∩ A 1) := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Anegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) A
      have hpos : 0 < Set.ncard (A 0 ∩ A 1) := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Aα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hpos:0 < (A 0 ∩ A 1).ncard⊢ 1 < (A 0 ∩ A 1).ncardnegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) A
        rw [Set.ncard_pos hFinα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅⊢ (A 0 ∩ A 1).Nonemptyα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅⊢ (A 0 ∩ A 1).Nonemptyα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hpos:0 < (A 0 ∩ A 1).ncard⊢ 1 < (A 0 ∩ A 1).ncardnegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) A]α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅⊢ (A 0 ∩ A 1).Nonemptyα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hpos:0 < (A 0 ∩ A 1).ncard⊢ 1 < (A 0 ∩ A 1).ncardnegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) A
        exact Set.nonempty_iff_ne_empty.mpr hEmptyα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hpos:0 < (A 0 ∩ A 1).ncard⊢ 1 < (A 0 ∩ A 1).ncardnegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) Aα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hpos:0 < (A 0 ∩ A 1).ncard⊢ 1 < (A 0 ∩ A 1).ncardnegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) A
      omeganegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) Anegα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncard⊢ HasPropertyB (Fin 2) A
    -- Get two distinct elements x, y in the intersection.
    obtain ⟨x, hxI, y, hyI, hxy⟩ := (Set.one_lt_ncard hFin).mp hge2negα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ y⊢ HasPropertyB (Fin 2) A
    -- Colour y with 1, everything else with 0.
    -- x ∈ A 0 ∩ A 1, y ∈ A 0 ∩ A 1, x ≠ y.
    refine ⟨fun n => if n = y then 1 else 0, fun i => ?_⟩negα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yi:Fin 2⊢ ¬IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A i)
    fin_cases ineg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ y⊢ ¬IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))neg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ y⊢ ¬IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))
    ·neg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ y⊢ ¬IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩)) -- A 0: f(x) = 0 ≠ 1 = f(y), x ≠ y, both in A 0.
      intro hMononeg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))⊢ False
      have hfx : (fun n => if n = y then (1 : Fin 2) else 0) x = 0 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Aneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0⊢ False
        simp [show x ≠ y from hxy]neg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0⊢ False
      have hfy : (fun n => if n = y then (1 : Fin 2) else 0) y = 1 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Aneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1⊢ False simpneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1⊢ False
      have := hMono x hxI.1 y hyI.1neg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:(fun n ↦ if n = y then 1 else 0) x = (fun n ↦ if n = y then 1 else 0) y⊢ False
      rw [hfx,neg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = (fun n ↦ if n = y then 1 else 0) y⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ False hfyneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ False] at thisneg.«_@».3279824903._hygCtx._hyg.77.«0»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ False; exact absurd this (byα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨0, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)
    ·neg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ y⊢ ¬IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩)) -- A 1: f(x) = 0 ≠ 1 = f(y), both in A 1.
      intro hMononeg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))⊢ False
      have hfx : (fun n => if n = y then (1 : Fin 2) else 0) x = 0 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Aneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0⊢ False
        simp [show x ≠ y from hxy]neg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0⊢ False
      have hfy : (fun n => if n = y then (1 : Fin 2) else 0) y = 1 := by⊢ True ↔
  ∀ {α : Type u_1} (A : Fin 2 → Set α),
    (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) Aneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1⊢ False simpneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1⊢ False
      have := hMono x hxI.2 y hyI.2neg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:(fun n ↦ if n = y then 1 else 0) x = (fun n ↦ if n = y then 1 else 0) y⊢ False
      rw [hfx,neg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = (fun n ↦ if n = y then 1 else 0) y⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ False hfyneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ Falseneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ False] at thisneg.«_@».3279824903._hygCtx._hyg.77.«1»α:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ False; exact absurd this (byα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).FinitehNcard:(A 0 ∩ A 1).ncard ≠ 1hEmpty:¬A 0 ∩ A 1 = ∅hge2:1 < (A 0 ∩ A 1).ncardx:αhxI:x ∈ A 0 ∩ A 1y:αhyI:y ∈ A 0 ∩ A 1hxy:x ≠ yhMono:IsMonochromatic (fun n ↦ if n = y then 1 else 0) (A ((fun i ↦ i) ⟨1, ⋯⟩))hfx:(fun n ↦ if n = y then 1 else 0) x = 0hfy:(fun n ↦ if n = y then 1 else 0) y = 1this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)

/- ## Sanity checks and examples

The following `example` declarations exercise the proved variants and demonstrate that
the hypotheses of the main theorem are non-vacuous. All goals are fully closed: no `sorry`. -/

/- ### Auxiliary lemmas used by the examples below -/

@[category test, AMS 3 5]
private lemma evens_infinite : Set.Infinite {n : ℕ | Even n} :=
  Set.infinite_of_injective_forall_mem (f := fun n : ℕ => 2 * n)
    (by⊢ Function.Injective fun n ↦ 2 * n intro a b ha:ℕb:ℕh:(fun n ↦ 2 * n) a = (fun n ↦ 2 * n) b⊢ a = b; simp only at ha:ℕb:ℕh:2 * a = 2 * b⊢ a = b; omegaAll goals completed! 🐙)
    (by⊢ ∀ (x : ℕ), 2 * x ∈ {n | Even n} intro nn:ℕ⊢ 2 * n ∈ {n | Even n}; simp only [Set.mem_ofPred_eq]n:ℕ⊢ Even (2 * n); exact ⟨n, byn:ℕ⊢ 2 * n = n + n ringAll goals completed! 🐙⟩)

@[category test, AMS 3 5]
private lemma odds_infinite : Set.Infinite {n : ℕ | Odd n} :=
  Set.infinite_of_injective_forall_mem (f := fun n : ℕ => 2 * n + 1)
    (by⊢ Function.Injective fun n ↦ 2 * n + 1 intro a b ha:ℕb:ℕh:(fun n ↦ 2 * n + 1) a = (fun n ↦ 2 * n + 1) b⊢ a = b; simp only at ha:ℕb:ℕh:2 * a + 1 = 2 * b + 1⊢ a = b; omegaAll goals completed! 🐙)
    (by⊢ ∀ (x : ℕ), 2 * x + 1 ∈ {n | Odd n} intro nn:ℕ⊢ 2 * n + 1 ∈ {n | Odd n}; simp only [Set.mem_ofPred_eq]n:ℕ⊢ Odd (2 * n + 1); exact ⟨n, byn:ℕ⊢ 2 * n + 1 = 2 * n + 1 ringAll goals completed! 🐙⟩)

@[category test, AMS 3 5]
private lemma evens_inter_odds_empty : {n : ℕ | Even n} ∩ {n : ℕ | Odd n} = ∅ := by⊢ {n | Even n} ∩ {n | Odd n} = ∅
  ext xx:ℕ⊢ x ∈ {n | Even n} ∩ {n | Odd n} ↔ x ∈ ∅
  simp only [Set.mem_inter_iff, Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false, not_and]x:ℕ⊢ Even x → ¬Odd x
  intro ⟨k, hk⟩ ⟨m, hm⟩x:ℕk:ℕhk:x = k + km:ℕhm:x = 2 * m + 1⊢ False; omegaAll goals completed! 🐙

The empty family vacuously has Property B, exercising erdos_602.variants.empty_index.

@[category test, AMS 3 5]
example : HasPropertyB PEmpty (fun (_ : PEmpty) => (Set.univ : Set ℕ)) :=
  erdos_602.variants.empty_index _ (fun _ => Set.infinite_univ)

Any infinite set, viewed as a singleton family, has Property B, exercising erdos_602.variants.unique_index.

@[category test, AMS 3 5]
example (A : Set ℕ) (hA : A.Infinite) :
    HasPropertyB Unit (fun _ => A) :=
  erdos_602.variants.unique_index Unit (fun _ => A) (fun _ => hA)



/-- The evens/odds family on ℕ satisfies all three hypotheses of the main theorem:
countably infinite sets, pairwise finite (in fact empty) intersection, and
intersection size ≠ 1 (it equals 0). This shows the hypotheses are non-vacuous. -/
@[category test, AMS 3 5]
example :
    let A : Fin 2 → Set ℕ := ![{n | Even n}, {n | Odd n}]
    (∀ i, (A i).Countable ∧ (A i).Infinite) ∧
    (∀ i j, i ≠ j → (A i ∩ A j).Finite) ∧
    (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) := by⊢ let A := ![{n | Even n}, {n | Odd n}];
(∀ (i : Fin 2), (A i).Countable ∧ (A i).Infinite) ∧
  (∀ (i j : Fin 2), i ≠ j → (A i ∩ A j).Finite) ∧ ∀ (i j : Fin 2), i ≠ j → (A i ∩ A j).ncard ≠ 1
  refine ⟨?_, ?_, ?_⟩refine_1⊢ ∀ (i : Fin 2), (![{n | Even n}, {n | Odd n}] i).Countable ∧ (![{n | Even n}, {n | Odd n}] i).Infiniterefine_2⊢ ∀ (i j : Fin 2), i ≠ j → (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).Finiterefine_3⊢ ∀ (i j : Fin 2), i ≠ j → (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1
  ·refine_1⊢ ∀ (i : Fin 2), (![{n | Even n}, {n | Odd n}] i).Countable ∧ (![{n | Even n}, {n | Odd n}] i).Infinite intro irefine_1i:Fin 2⊢ (![{n | Even n}, {n | Odd n}] i).Countable ∧ (![{n | Even n}, {n | Odd n}] i).Infinite; fin_cases irefine_1.«0»⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Countable ∧
  (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Infiniterefine_1.«1»⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).Countable ∧
  (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).Infinite
    ·refine_1.«0»⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Countable ∧
  (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Infinite exact ⟨(Set.countable_univ).mono (Set.subset_univ _), evens_infinite⟩All goals completed! 🐙
    ·refine_1.«1»⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).Countable ∧
  (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).Infinite exact ⟨(Set.countable_univ).mono (Set.subset_univ _), odds_infinite⟩All goals completed! 🐙
  ·refine_2⊢ ∀ (i j : Fin 2), i ≠ j → (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).Finite intro i j hijrefine_2i:Fin 2j:Fin 2hij:i ≠ j⊢ (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).Finite
    fin_cases irefine_2.«0»j:Fin 2hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).Finiterefine_2.«1»j:Fin 2hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).Finite <;>refine_2.«0»j:Fin 2hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).Finiterefine_2.«1»j:Fin 2hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).Finite fin_cases jrefine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Finiterefine_2.«1».«1»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).Finite
    all_goals first | exact absurd rfl hijAll goals completed! 🐙 | skiprefine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Finite
    ·refine_2.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).Finite show ({n : ℕ | Even n} ∩ {n | Odd n}).Finiterefine_2.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ ({n | Even n} ∩ {n | Odd n}).Finite
      rw [evens_inter_odds_emptyrefine_2.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ ∅.Finiterefine_2.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ ∅.Finite]refine_2.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ ∅.Finite; exact Set.finite_emptyAll goals completed! 🐙
    ·refine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).Finite show ({n : ℕ | Odd n} ∩ {n | Even n}).Finiterefine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ({n | Odd n} ∩ {n | Even n}).Finite
      rw [Set.inter_comm,refine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ({n | Even n} ∩ {n | Odd n}).Finiterefine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ∅.Finite evens_inter_odds_emptyrefine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ∅.Finiterefine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ∅.Finite]refine_2.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ∅.Finite; exact Set.finite_emptyAll goals completed! 🐙
  ·refine_3⊢ ∀ (i j : Fin 2), i ≠ j → (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1 intro i j hijrefine_3i:Fin 2j:Fin 2hij:i ≠ j⊢ (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1
    fin_cases irefine_3.«0»j:Fin 2hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1refine_3.«1»j:Fin 2hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1 <;>refine_3.«0»j:Fin 2hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1refine_3.«1»j:Fin 2hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ j⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1 fin_cases jrefine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).ncard ≠ 1refine_3.«1».«1»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).ncard ≠ 1
    all_goals first | exact absurd rfl hijAll goals completed! 🐙 | skiprefine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).ncard ≠ 1
    ·refine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩)).ncard ≠ 1 show Set.ncard ({n : ℕ | Even n} ∩ {n | Odd n}) ≠ 1refine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ ({n | Even n} ∩ {n | Odd n}).ncard ≠ 1
      rw [evens_inter_odds_empty,refine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ ∅.ncard ≠ 1refine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ 0 ≠ 1 Set.ncard_emptyrefine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ 0 ≠ 1refine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ 0 ≠ 1]refine_3.«0».«1»hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ 0 ≠ 1; decideAll goals completed! 🐙
    ·refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩) ∩ ![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩)).ncard ≠ 1 show Set.ncard ({n : ℕ | Odd n} ∩ {n | Even n}) ≠ 1refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ({n | Odd n} ∩ {n | Even n}).ncard ≠ 1
      rw [Set.inter_comm,refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ({n | Even n} ∩ {n | Odd n}).ncard ≠ 1refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ 0 ≠ 1 evens_inter_odds_empty,refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ ∅.ncard ≠ 1refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ 0 ≠ 1 Set.ncard_emptyrefine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ 0 ≠ 1refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ 0 ≠ 1]refine_3.«1».«0»hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ 0 ≠ 1; decideAll goals completed! 🐙



/-- The evens/odds family on ℕ has Property B, witnessed by the colouring
`f(n) = 1` if `n ∈ {1, 2}`, else `f(n) = 0`. Concretely:
`f(0) = 0 ≠ 1 = f(2)` shows evens are not monochromatic, and
`f(1) = 1 ≠ 0 = f(3)` shows odds are not monochromatic. -/
@[category test, AMS 3 5]
example : HasPropertyB (Fin 2) (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]
  classical
  refine ⟨fun n => if n = 2 ∨ n = 1 then 1 else 0, fun i hMono => ?_⟩i:Fin 2hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] i)⊢ False
  fin_cases i«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))⊢ False«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))⊢ False
  ·«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))⊢ False -- A 0 = evens: f(0) = 0 ≠ 1 = f(2)
    have h0 : (fun n : ℕ => if n = 2 ∨ n = 1 then (1 : Fin 2) else 0) 0 = 0 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0⊢ False decide«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0⊢ False«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0⊢ False
    have h2 : (fun n : ℕ => if n = 2 ∨ n = 1 then (1 : Fin 2) else 0) 2 = 1 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1⊢ False decide«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1⊢ False«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1⊢ False
    have hmem0 : (0 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 0 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False
      simp only [Matrix.cons_val_zero, Set.mem_ofPred_eq]hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1⊢ Even 0«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False; exact ⟨0, byhMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1⊢ 0 = 0 + 0«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False ringAll goals completed! 🐙«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False⟩«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False
    have hmem2 : (2 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 0 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False
      simp only [Matrix.cons_val_zero, Set.mem_ofPred_eq]hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ Even 2«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False; exact ⟨1, byhMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ 2 = 1 + 1«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False ringAll goals completed! 🐙«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False⟩«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0⊢ False
    have := hMono 0 hmem0 2 hmem2«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2⊢ False
    rw [h0,«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:0 = (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2⊢ False«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:0 = 1⊢ False h2«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:0 = 1⊢ False«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:0 = 1⊢ False] at this«0»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:0 = 1⊢ False; exact absurd this (byhMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨0, ⋯⟩))h0:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 0 = 0h2:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 2 = 1hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)
  ·«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))⊢ False -- A 1 = odds: f(1) = 1 ≠ 0 = f(3)
    have h1 : (fun n : ℕ => if n = 2 ∨ n = 1 then (1 : Fin 2) else 0) 1 = 1 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1⊢ False decide«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1⊢ False«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1⊢ False
    have h3 : (fun n : ℕ => if n = 2 ∨ n = 1 then (1 : Fin 2) else 0) 3 = 0 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0⊢ False decide«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0⊢ False«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0⊢ False
    have hmem1 : (1 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 1 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False
      simp only [Matrix.cons_val_one]hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0⊢ 1 ∈ ![{n | Odd n}] 0«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False; exact ⟨0, byhMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0⊢ 1 = 2 * 0 + 1«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False ringAll goals completed! 🐙«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False⟩«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False
    have hmem3 : (3 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 1 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False
      simp only [Matrix.cons_val_one]hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ 3 ∈ ![{n | Odd n}] 0«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False; exact ⟨1, byhMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ 3 = 2 * 1 + 1«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False ringAll goals completed! 🐙«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False⟩«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1⊢ False
    have := hMono 1 hmem1 3 hmem3«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3⊢ False
    rw [h1,«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:1 = (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3⊢ False«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:1 = 0⊢ False h3«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:1 = 0⊢ False«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:1 = 0⊢ False] at this«1»hMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:1 = 0⊢ False; exact absurd this (byhMono:IsMonochromatic (fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) (![{n | Even n}, {n | Odd n}] ((fun i ↦ i) ⟨1, ⋯⟩))h1:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 1 = 1h3:(fun n ↦ if n = 2 ∨ n = 1 then 1 else 0) 3 = 0hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1this:1 = 0⊢ ¬1 = 0 decideAll goals completed! 🐙)



/-- The intersection `{0, 2, 4, …} ∩ {0, 1, 3, 5, …} = {0}` has size 1, showing
the hypothesis `Set.ncard (A i ∩ A j) ≠ 1` correctly excludes this family.
This confirms the boundary condition is faithfully encoded. -/
@[category test, AMS 3 5]
example : Set.ncard ({n : ℕ | Even n} ∩ {n : ℕ | n = 0 ∨ Odd n}) = 1 := by⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
  have heq : {n : ℕ | Even n} ∩ {n : ℕ | n = 0 ∨ Odd n} = {0} := by
    ext xx:ℕ⊢ x ∈ {n | Even n} ∩ {n | n = 0 ∨ Odd n} ↔ x ∈ {0}heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
    simp only [Set.mem_inter_iff, Set.mem_ofPred_eq, Set.mem_singleton_iff]x:ℕ⊢ Even x ∧ (x = 0 ∨ Odd x) ↔ x = 0heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
    constructormpx:ℕ⊢ Even x ∧ (x = 0 ∨ Odd x) → x = 0mprx:ℕ⊢ x = 0 → Even x ∧ (x = 0 ∨ Odd x)heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
    ·mpx:ℕ⊢ Even x ∧ (x = 0 ∨ Odd x) → x = 0heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1 rintro ⟨⟨k, hk⟩, rfl | ⟨m, hm⟩⟩mp.inlk:ℕhk:0 = k + k⊢ 0 = 0mp.inrx:ℕk:ℕhk:x = k + km:ℕhm:x = 2 * m + 1⊢ x = 0heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1 <;>mp.inlk:ℕhk:0 = k + k⊢ 0 = 0mp.inrx:ℕk:ℕhk:x = k + km:ℕhm:x = 2 * m + 1⊢ x = 0heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1 omegaAll goals completed! 🐙heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
    ·mprx:ℕ⊢ x = 0 → Even x ∧ (x = 0 ∨ Odd x)heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1 rintro rflmpr⊢ Even 0 ∧ (0 = 0 ∨ Odd 0)heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1; exact ⟨⟨0, by⊢ 0 = 0 + 0heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1 ringAll goals completed! 🐙heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1⟩, Or.inl rfl⟩heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
  rw [heq,heq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ {0}.ncard = 1All goals completed! 🐙 Set.ncard_singletonheq:{n | Even n} ∩ {n | n = 0 ∨ Odd n} = {0}⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

A natural but FALSE relaxation of erdos_602.variants.disjoint: drop the hypothesis that each A i is infinite. The original disjoint variant requires (∀ i, (A i).Infinite). Without it, the claim is false.

def disjoint_without_infinite_claim : Prop :=
  ∀ {α : Type} {I : Type} (A : I → Set α),
    (∀ i j, i ≠ j → Disjoint (A i) (A j)) →
    HasPropertyB I A

Formal disproof of disjoint_without_infinite_claim.

Counterexample: Take α = ℕ, I = Fin 2, with A 0 = {0} and A 1 = {1}. These are pairwise disjoint, satisfying the only hypothesis. But singleton sets are vacuously monochromatic under any colouring: the only pair (x, y) ∈ {0} × {0} is (0, 0), and f 0 = f 0 trivially. So any colouring makes A 0 monochromatic, meaning HasPropertyB fails.


@[category research solved, AMS 3]
theorem disjoint_without_infinite_claim.disproof :
    ¬ disjoint_without_infinite_claim := by⊢ ¬disjoint_without_infinite_claim
  -- We prove the negation by constructing an explicit counterexample.
  -- Specialize directly to α = ℕ, I = Fin 2, A k = if k = 0 then {0} else {1}.
  intro hh:disjoint_without_infinite_claim⊢ False
  -- Obtain a colouring from h applied to the concrete family.
  -- We need h to see it as a universally quantified statement.
  have hApp : HasPropertyB (Fin 2) (fun k : Fin 2 => if k = 0 then ({0} : Set ℕ) else {1}) :=
    h (fun k : Fin 2 => if k = 0 then ({0} : Set ℕ) else {1}) (byh:disjoint_without_infinite_claim⊢ ∀ (i j : Fin 2), i ≠ j → Disjoint (if i = 0 then {0} else {1}) (if j = 0 then {0} else {1})h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False
      intro i j hijh:disjoint_without_infinite_claimi:Fin 2j:Fin 2hij:i ≠ j⊢ Disjoint (if i = 0 then {0} else {1}) (if j = 0 then {0} else {1})h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False
      fin_cases i«0»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ j⊢ Disjoint (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1}) (if j = 0 then {0} else {1})«1»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ j⊢ Disjoint (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1}) (if j = 0 then {0} else {1})h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False <;>«0»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ j⊢ Disjoint (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1}) (if j = 0 then {0} else {1})«1»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ j⊢ Disjoint (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1}) (if j = 0 then {0} else {1})h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False fin_cases j«1».«0»h:disjoint_without_infinite_claimhij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ Disjoint (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1}) (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1})«1».«1»h:disjoint_without_infinite_claimhij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ Disjoint (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1}) (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1})h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False <;>«0».«0»h:disjoint_without_infinite_claimhij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ Disjoint (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1}) (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1})«0».«1»h:disjoint_without_infinite_claimhij:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ Disjoint (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1}) (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1})«1».«0»h:disjoint_without_infinite_claimhij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ Disjoint (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1}) (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then {0} else {1})«1».«1»h:disjoint_without_infinite_claimhij:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ Disjoint (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1}) (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then {0} else {1})h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False simp_allAll goals completed! 🐙h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False)h:disjoint_without_infinite_claimhApp:HasPropertyB (Fin 2) fun k ↦ if k = 0 then {0} else {1}⊢ False
  obtain ⟨f, hf⟩ := hApph:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)⊢ False
  -- hf 0 : ¬ IsMonochromatic f ((fun k => if k = 0 then {0} else {1}) 0)
  -- (fun k => if k = 0 then {0} else {1}) 0 = {0}, a singleton.
  -- A singleton is monochromatic under any colouring. Contradiction.
  apply hf 0h:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)⊢ IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) 0)
  -- Goal: IsMonochromatic f ((fun k => if k = 0 then {0} else {1}) 0)
  -- which reduces to: IsMonochromatic f {0}
  simp only [Fin.isValue, ↓reduceIte]h:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)⊢ IsMonochromatic f {0}
  intro x hx y hyh:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)x:ℕhx:x ∈ {0}y:ℕhy:y ∈ {0}⊢ f x = f y
  simp only [Set.mem_singleton_iff] at hx hyh:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)x:ℕy:ℕhx:x = 0hy:y = 0⊢ f x = f y
  rw [hx,h:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)x:ℕy:ℕhx:x = 0hy:y = 0⊢ f 0 = f yAll goals completed! 🐙 hyh:disjoint_without_infinite_claimf:ℕ → Fin 2hf:∀ (i : Fin 2), ¬IsMonochromatic f ((fun k ↦ if k = 0 then {0} else {1}) i)x:ℕy:ℕhx:x = 0hy:y = 0⊢ f 0 = f 0All goals completed! 🐙]All goals completed! 🐙

end Erdos602