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 Set


namespace 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 declaration uses 'sorry'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α:Type u_1I:Type u_2⊢ ∀ (A : I → Set α), (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I A Aα:Type u_1I:Type u_2A:I → Set α⊢ (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I A hInfiniteα:Type u_1I:Type u_2A:I → Set αhInfinite:∀ (i : I), (A i).Infinite⊢ (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → HasPropertyB I A 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
    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
    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
    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
      apply Set.Infinite.nonemptyhα: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
      exact (hInfinite i).diff (Set.finite_singleton a)All goals completed! 🐙
    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
    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
    exact ⟨a, b, ha, hbA, fun h => hba h.symm⟩All goals completed! 🐙
  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
    intro i jα: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:I⊢ a_fn i ≠ b_fn 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
    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
    ·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 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; exact hab_ne i hajAll goals completed! 🐙
    ·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 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) := hDisjoint i j hij⊢ False
      rw [Set.disjoint_left] 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
      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 := hb_mem j⊢ False
      rw [← haj] 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
      exact hdisj (ha_mem i) hbjAll goals completed! 🐙
  -- 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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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
    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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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
    rw [if_neg]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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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
    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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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
    exact key i j hjAll goals completed! 🐙
  -- 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
    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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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 := id (Eq.mpr (id (congrArg (fun _a => _a = 0) (if_neg fun a => Exists.casesOn a fun j hj => key i j hj))) (Eq.refl 0))⊢ (if ∃ i_1, b_fn i = b_fn i_1 then 1 else 0) = 1
    rw [if_pos ⟨i, rfl⟩]All goals completed! 🐙
  -- 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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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 := id (Eq.mpr (id (congrArg (fun _a => _a = 0) (if_neg fun a => Exists.casesOn a fun j hj => key i j hj))) (Eq.refl 0))hfb:f (b_fn i) = 1 := id (Eq.mpr (id (congrArg (fun _a => _a = 1) (if_pos (Exists.intro i rfl)))) (Eq.refl 1))hne:f (a_fn i) = f (b_fn i) := hMono (a_fn i) (ha_mem i) (b_fn i) (hb_mem i)⊢ False
  rw [hfa, hfb] 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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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 := id (Eq.mpr (id (congrArg (fun _a => _a = 0) (if_neg fun a => Exists.casesOn a fun j hj => key i j hj))) (Eq.refl 0))hfb:f (b_fn i) = 1 := id (Eq.mpr (id (congrArg (fun _a => _a = 1) (if_pos (Exists.intro i rfl)))) (Eq.refl 1))hne: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 j := 
  fun i j haj =>
    if hij : i = j then Eq.ndrec (motive := fun j => a_fn i = b_fn j → False) (fun haj => hab_ne i haj) hij haj
    else
      have hdisj := hDisjoint i j hij;
      have hbj := hb_mem j;
      Eq.mp (congrArg (fun _a => _a) (propext disjoint_left)) hdisj (ha_mem i)
        (Eq.mp (congrArg (fun _a => _a ∈ A j) (Eq.symm haj)) hbj)f:α → 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 := id (Eq.mpr (id (congrArg (fun _a => _a = 0) (if_neg fun a => Exists.casesOn a fun j hj => key i j hj))) (Eq.refl 0))hfb:f (b_fn i) = 1 := id (Eq.mpr (id (congrArg (fun _a => _a = 1) (if_pos (Exists.intro i rfl)))) (Eq.refl 1))hne: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 declaration uses 'sorry'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
    apply Set.Infinite.nonemptyhα:Type u_1A:Set αhA:A.Infinitea:αha:a ∈ A⊢ (A \ {a}).Infinite
    exact hA.diff (Set.finite_singleton a)All goals completed! 🐙
  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_diff, 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
    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
    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
    exact absurd h (Ne.symm hba)All goals completed! 🐙
  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
    simpAll goals completed! 🐙
  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 = 0 := Eq.mpr (id single_set._simp_2) fun h => absurd h (Ne.symm hba)h1:(fun n => if n = b then 1 else 0) b = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self b))) (eq_self 1))this:(fun n => if n = b then 1 else 0) a = (fun n => if n = b then 1 else 0) b := hMono a ha b hbA⊢ False
  rw [h0, h1] 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 = 0 := Eq.mpr (id single_set._simp_2) fun h => absurd h (Ne.symm hba)h1:(fun n => if n = b then 1 else 0) b = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self b))) (eq_self 1))this: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 = 0 := Eq.mpr (id single_set._simp_2) fun h => absurd h (Ne.symm hba)h1:(fun n => if n = b then 1 else 0) b = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self b))) (eq_self 1))this: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)
  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α:Type u_1A:Fin 2 → Set α⊢ (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) A hInfiniteα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).Infinite⊢ (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) A hFinα:Type u_1A:Fin 2 → Set αhInfinite:∀ (i : Fin 2), (A i).InfinitehFin:(A 0 ∩ A 1).Finite⊢ (A 0 ∩ A 1).ncard ≠ 1 → HasPropertyB (Fin 2) A 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).diff (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 := Set.Infinite.nonempty (Infinite.diff (hInfinite 0) (finite_singleton a))⊢ 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).diff (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 := Set.Infinite.nonempty (Infinite.diff (hInfinite 1) (finite_singleton c))⊢ 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) A
      intro x hx0α: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 0⊢ x ∉ A 1 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⊢ False
      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 := ⟨hx0, hx1⟩⊢ False
      rw [hEmpty] 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 ∈ ∅⊢ False
      exact hmemAll goals completed! 🐙
    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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)⊢ 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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)⊢ 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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)⊢ 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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)i:Fin 2⊢ ¬IsMonochromatic (fun n => if n = b ∨ n = c then 1 else 0) (A i)
    fin_cases ipos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)⊢ ¬IsMonochromatic (fun n => if n = b ∨ n = c then 1 else 0) (A ((fun i => i) ⟨0, ⋯⟩))pos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)⊢ ¬IsMonochromatic (fun n => if n = b ∨ n = c then 1 else 0) (A ((fun i => i) ⟨1, ⋯⟩))
    ·pos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)⊢ ¬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.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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) A
        simp [show a ≠ b from fun h => hba h.symm, ha_ne_c]All goals completed! 🐙
      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) A simpAll goals completed! 🐙
      have := hMono a ha0 b hbA0pos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (Eq.trans
            (congr
              (congrArg Or
                (eq_false
                  (have this := fun h => hba (Eq.symm h);
                  this)))
              (eq_false ha_ne_c))
            (or_self False))))
      (eq_self 0))hfb:(fun n => if n = b ∨ n = c then 1 else 0) b = 1 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 1)
        (ite_cond_eq_true 1 0 (Eq.trans (congrArg (fun x => x ∨ b = c) (eq_self b)) (true_or (b = c)))))
      (eq_self 1))this:(fun n => if n = b ∨ n = c then 1 else 0) a = (fun n => if n = b ∨ n = c then 1 else 0) b := hMono a ha0 b hbA0⊢ False
      rw [hfa, hfb] at thispos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (Eq.trans
            (congr
              (congrArg Or
                (eq_false
                  (have this := fun h => hba (Eq.symm h);
                  this)))
              (eq_false ha_ne_c))
            (or_self False))))
      (eq_self 0))hfb:(fun n => if n = b ∨ n = c then 1 else 0) b = 1 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 1)
        (ite_cond_eq_true 1 0 (Eq.trans (congrArg (fun x => x ∨ b = c) (eq_self b)) (true_or (b = c)))))
      (eq_self 1))this: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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (Eq.trans
            (congr
              (congrArg Or
                (eq_false
                  (have this := fun h => hba (Eq.symm h);
                  this)))
              (eq_false ha_ne_c))
            (or_self False))))
      (eq_self 0))hfb:(fun n => if n = b ∨ n = c then 1 else 0) b = 1 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 1)
        (ite_cond_eq_true 1 0 (Eq.trans (congrArg (fun x => x ∨ b = c) (eq_self b)) (true_or (b = c)))))
      (eq_self 1))this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)
    ·pos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)⊢ ¬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.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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) A simpAll goals completed! 🐙
      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) A
        simp [hb_ne_d.symm, hdc]All goals completed! 🐙
      have := hMono c hc1 d hd1pos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (Eq.trans (congrArg (Or (c = b)) (eq_self c)) (or_true (c = b)))))
      (eq_self 1))hfd:(fun n => if n = b ∨ n = c then 1 else 0) d = 0 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (Eq.trans (congr (congrArg Or (eq_false (Ne.symm hb_ne_d))) (eq_false hdc)) (or_self False))))
      (eq_self 0))this:(fun n => if n = b ∨ n = c then 1 else 0) c = (fun n => if n = b ∨ n = c then 1 else 0) d := hMono c hc1 d hd1⊢ False
      rw [hfc, hfd] at thispos.«_@».3279824903._hygCtx._hyg.76.«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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (Eq.trans (congrArg (Or (c = b)) (eq_self c)) (or_true (c = b)))))
      (eq_self 1))hfd:(fun n => if n = b ∨ n = c then 1 else 0) d = 0 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (Eq.trans (congr (congrArg Or (eq_false (Ne.symm hb_ne_d))) (eq_false hdc)) (or_self False))))
      (eq_self 0))this: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 1 := 
  fun x hx0 hx1 =>
    have hmem := ⟨hx0, hx1⟩;
    Eq.mp (congrArg (fun _a => x ∈ _a) hEmpty) hmemhb_ne_c:b ≠ c := fun h => hDisj b hbA0 (Eq.symm h ▸ hc1)hb_ne_d:b ≠ d := fun h => hDisj b hbA0 (Eq.symm h ▸ hd1)ha_ne_c:a ≠ c := fun h => hDisj a ha0 (Eq.symm h ▸ hc1)hMono: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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (Eq.trans (congrArg (Or (c = b)) (eq_self c)) (or_true (c = b)))))
      (eq_self 1))hfd:(fun n => if n = b ∨ n = c then 1 else 0) d = 0 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (Eq.trans (congr (congrArg Or (eq_false (Ne.symm hb_ne_d))) (eq_false hdc)) (or_self False))))
      (eq_self 0))this: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) 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
        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
        exact Set.nonempty_iff_ne_empty.mpr hEmptyAll goals completed! 🐙
      omegaAll goals completed! 🐙
    -- 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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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) A
        simp [show x ≠ y from hxy]All goals completed! 🐙
      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) A simpAll goals completed! 🐙
      have := hMono x hxI.1 y hyI.1neg.«_@».3279824903._hygCtx._hyg.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (eq_false
            (have this := hxy;
            this))))
      (eq_self 0))hfy:(fun n => if n = y then 1 else 0) y = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self y))) (eq_self 1))this:(fun n => if n = y then 1 else 0) x = (fun n => if n = y then 1 else 0) y := hMono x hxI.left y hyI.left⊢ False
      rw [hfx, hfy] at thisneg.«_@».3279824903._hygCtx._hyg.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (eq_false
            (have this := hxy;
            this))))
      (eq_self 0))hfy:(fun n => if n = y then 1 else 0) y = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self y))) (eq_self 1))this: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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (eq_false
            (have this := hxy;
            this))))
      (eq_self 0))hfy:(fun n => if n = y then 1 else 0) y = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self y))) (eq_self 1))this:0 = 1⊢ ¬0 = 1 decideAll goals completed! 🐙)
    ·neg.«_@».3279824903._hygCtx._hyg.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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) A
        simp [show x ≠ y from hxy]All goals completed! 🐙
      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) A simpAll goals completed! 🐙
      have := hMono x hxI.2 y hyI.2neg.«_@».3279824903._hygCtx._hyg.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (eq_false
            (have this := hxy;
            this))))
      (eq_self 0))hfy:(fun n => if n = y then 1 else 0) y = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self y))) (eq_self 1))this:(fun n => if n = y then 1 else 0) x = (fun n => if n = y then 1 else 0) y := hMono x hxI.right y hyI.right⊢ False
      rw [hfx, hfy] at thisneg.«_@».3279824903._hygCtx._hyg.76.«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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (eq_false
            (have this := hxy;
            this))))
      (eq_self 0))hfy:(fun n => if n = y then 1 else 0) y = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self y))) (eq_self 1))this: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).ncard := 
  have hpos := Eq.mpr (id (congrArg (fun _a => _a) (propext (ncard_pos hFin)))) (nonempty_iff_ne_empty.mpr hEmpty);
  Decidable.byContradiction fun a => two_sets._proof_1 A hNcard hpos ax:α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 := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = 0)
        (ite_cond_eq_false 1 0
          (eq_false
            (have this := hxy;
            this))))
      (eq_self 0))hfy:(fun n => if n = y then 1 else 0) y = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 0 (eq_self y))) (eq_self 1))this: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 ba:ℕb:ℕ⊢ (fun n => 2 * n) a = (fun n => 2 * n) b → 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 : ℕ), (fun n => 2 * n) x ∈ {n | Even n} intro nn:ℕ⊢ (fun n => 2 * n) n ∈ {n | Even n}; simp only [Set.mem_setOf_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 ba:ℕb:ℕ⊢ (fun n => 2 * n + 1) a = (fun n => 2 * n + 1) b → 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 : ℕ), (fun n => 2 * n + 1) x ∈ {n | Odd n} intro nn:ℕ⊢ (fun n => 2 * n + 1) n ∈ {n | Odd n}; simp only [Set.mem_setOf_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 xhx:ℕ⊢ x ∈ {n | Even n} ∩ {n | Odd n} ↔ x ∈ ∅
  simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_and]hx:ℕ⊢ Even x → ¬Odd x
  intro ⟨k, hk⟩ ⟨m, hm⟩hx:ℕ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 jrefine_2i:Fin 2j:Fin 2⊢ i ≠ j → (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).Finite 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_empty]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, evens_inter_odds_empty]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 jrefine_3i:Fin 2j:Fin 2⊢ i ≠ j → (![{n | Even n}, {n | Odd n}] i ∩ ![{n | Even n}, {n | Odd n}] j).ncard ≠ 1 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, Set.ncard_empty]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, evens_inter_odds_empty, Set.ncard_empty]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}] decideAll goals completed! 🐙
    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}] decideAll goals completed! 🐙
    have hmem0 : (0 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 0 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]
      simp only [Matrix.cons_val_zero, Set.mem_setOf_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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))⊢ Even 0; 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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))⊢ 0 = 0 + 0 ringAll goals completed! 🐙⟩
    have hmem2 : (2 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 0 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]
      simp only [Matrix.cons_val_zero, Set.mem_setOf_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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.add_pf_zero_add 0))))⊢ Even 2; 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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.add_pf_zero_add 0))))⊢ 2 = 1 + 1 ringAll goals completed! 🐙⟩
    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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.add_pf_zero_add 0))))hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 1
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_add_overlap
            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
              (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1)
                (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2)))
            (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))this:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 0 = (fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 := hMono 0 hmem0 2 hmem2⊢ False
    rw [h0, h2] 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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.add_pf_zero_add 0))))hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 1
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_add_overlap
            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
              (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1)
                (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2)))
            (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))this: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 = 0 := of_decide_eq_true (id (Eq.refl true))h2:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 2 = 1 := of_decide_eq_true (id (Eq.refl true))hmem0:0 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
          (Mathlib.Tactic.Ring.add_pf_zero_add 0))))hmem2:2 ∈ ![{n | Even n}, {n | Odd n}] 0 := 
  id
    (Exists.intro 1
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
        (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_add_overlap
            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
              (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1)
                (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2)))
            (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))this: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}] decideAll goals completed! 🐙
    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}] decideAll goals completed! 🐙
    have hmem1 : (1 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 1 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]
      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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))⊢ 1 ∈ ![{n | Odd n}] 0; 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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))⊢ 1 = 2 * 0 + 1 ringAll goals completed! 🐙⟩
    have hmem3 : (3 : ℕ) ∈ (![{n : ℕ | Even n}, {n | Odd n}] : Fin 2 → Set ℕ) 1 := by⊢ HasPropertyB (Fin 2) ![{n | Even n}, {n | Odd n}]
      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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
            (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0)
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))))⊢ 3 ∈ ![{n | Odd n}] 0; 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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
            (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0)
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))))⊢ 3 = 2 * 1 + 1 ringAll goals completed! 🐙⟩
    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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
            (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0)
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))))hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 1
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + 0))))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_add_overlap
            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
              (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2)
                (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 3)))
            (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))this:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 1 = (fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 := hMono 1 hmem1 3 hmem3⊢ False
    rw [h1, h3] 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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
            (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0)
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))))hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 1
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + 0))))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_add_overlap
            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
              (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2)
                (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 3)))
            (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))this: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 = 1 := of_decide_eq_true (id (Eq.refl true))h3:(fun n => if n = 2 ∨ n = 1 then 1 else 0) 3 = 0 := of_decide_eq_true (id (Eq.refl true))hmem1:1 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 0
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))
            (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0)
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))))hmem3:3 ∈ ![{n | Even n}, {n | Odd n}] 1 := 
  id
    (Exists.intro 1
      (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
        (Mathlib.Tactic.Ring.add_congr
          (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
            (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + 0))))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
          (Mathlib.Tactic.Ring.add_pf_add_overlap
            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
              (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2)
                (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 3)))
            (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))this: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⊢ ({n | Even n} ∩ {n | n = 0 ∨ Odd n}).ncard = 1
    ext xhx:ℕ⊢ x ∈ {n | Even n} ∩ {n | n = 0 ∨ Odd n} ↔ x ∈ {0}
    simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_singleton_iff]hx:ℕ⊢ Even x ∧ (x = 0 ∨ Odd x) ↔ x = 0
    constructorh.mpx:ℕ⊢ Even x ∧ (x = 0 ∨ Odd x) → x = 0h.mprx:ℕ⊢ x = 0 → Even x ∧ (x = 0 ∨ Odd x)
    ·h.mpx:ℕ⊢ Even x ∧ (x = 0 ∨ Odd x) → x = 0 rintro ⟨⟨k, hk⟩, rfl | ⟨m, hm⟩⟩h.mp.inlk:ℕhk:0 = k + k⊢ 0 = 0h.mp.inrx:ℕk:ℕhk:x = k + km:ℕhm:x = 2 * m + 1⊢ x = 0 <;>h.mp.inlk:ℕhk:0 = k + k⊢ 0 = 0h.mp.inrx:ℕk:ℕhk:x = k + km:ℕhm:x = 2 * m + 1⊢ x = 0 omegaAll goals completed! 🐙
    ·h.mprx:ℕ⊢ x = 0 → Even x ∧ (x = 0 ∨ Odd x) rintro rflh.mpr⊢ Even 0 ∧ (0 = 0 ∨ Odd 0); exact ⟨⟨0, by⊢ 0 = 0 + 0 ringAll goals completed! 🐙⟩, Or.inl rfl⟩
  rw [heq, Set.ncard_singleton]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 ((fun k => if k = 0 then {0} else {1}) i) ((fun k => if k = 0 then {0} else {1}) j)
      intro i jh:disjoint_without_infinite_claimi:Fin 2j:Fin 2⊢ i ≠ j → Disjoint ((fun k => if k = 0 then {0} else {1}) i) ((fun k => if k = 0 then {0} else {1}) j) hijh:disjoint_without_infinite_claimi:Fin 2j:Fin 2hij:i ≠ j⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) i) ((fun k => if k = 0 then {0} else {1}) j)
      fin_cases i«0»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i => i) ⟨0, ⋯⟩ ≠ j⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩)) ((fun k => if k = 0 then {0} else {1}) j)«1»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i => i) ⟨1, ⋯⟩ ≠ j⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩)) ((fun k => if k = 0 then {0} else {1}) j) <;>«0»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i => i) ⟨0, ⋯⟩ ≠ j⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩)) ((fun k => if k = 0 then {0} else {1}) j)«1»h:disjoint_without_infinite_claimj:Fin 2hij:(fun i => i) ⟨1, ⋯⟩ ≠ j⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩)) ((fun k => if k = 0 then {0} else {1}) j) fin_cases j«1».«0»h:disjoint_without_infinite_claimhij:(fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩))
  ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩))«1».«1»h:disjoint_without_infinite_claimhij:(fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩))
  ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩)) <;>«0».«0»h:disjoint_without_infinite_claimhij:(fun i => i) ⟨0, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩))
  ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩))«0».«1»h:disjoint_without_infinite_claimhij:(fun i => i) ⟨0, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩))
  ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩))«1».«0»h:disjoint_without_infinite_claimhij:(fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩))
  ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨0, ⋯⟩))«1».«1»h:disjoint_without_infinite_claimhij:(fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩⊢ Disjoint ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩))
  ((fun k => if k = 0 then {0} else {1}) ((fun i => i) ⟨1, ⋯⟩)) simp_allAll goals completed! 🐙)
  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 hxh: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 ∈ {0}, f x = f y yh: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:ℕ⊢ y ∈ {0} → f x = f 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, hy]All goals completed! 🐙


end Erdos602