1. FormalConjectures
  2. ErdosProblems
  3. «1167»
/- 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 1167

Reference: erdosproblems.com/1167

The original Erdős–Hajnal problem list gives the additional conditions $\gamma \geq 2$, $r < \omega$, and $\kappa_\alpha > r$. Without $\gamma \geq 2$, the statement is false: taking $\gamma = 1$ and $\kappa_0 = \aleph_1$ with $\lambda = \aleph_0$ gives a counterexample, since the partition relation with one color degenerates to a cardinality comparison (see erdos_1167.unrestricted_is_false).

open Cardinal Ordinal Combinatorics namespace Erdos1167 universe u

Erdős Problem 1167. Let $r \geq 2$ be finite, $\gamma \geq 2$, and $\lambda$ be an infinite cardinal. Let $\kappa_\alpha$ be cardinals for all $\alpha < \gamma$. Is it true that $$2^\lambda \to (\kappa_\alpha + 1){\alpha < \gamma}^{r+1}$$ implies $$\lambda \to (\kappa\alpha){\alpha < \gamma}^r?$$ Here $+$ means cardinal addition, so that $\kappa\alpha + 1 = \kappa_\alpha$ if $\kappa_\alpha$ is infinite.

A problem of Erdős, Hajnal, and Rado.

@[category research open, AMS 5] theorem declaration uses 'sorry'erdos_1167 : answer(sorry) ↔ ∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}), 2 ≤ γ → ∀ (κ : γ.ToType → Cardinal.{u}), cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) → cardinalPartitionRel lam r γ κ := ⊢ True ↔ ∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}), 2 ≤ γ → ∀ (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κ All goals completed! 🐙 namespace erdos_1167.variants

Finite-target case. When all $\kappa_\alpha$ are finite, $\kappa_\alpha + 1$ is the ordinary natural-number successor. Special case of erdos_1167.

@[category research open, AMS 5] theorem declaration uses 'sorry'finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => (n α : Cardinal.{u}) + 1) → cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u})) := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γn:γ.ToType → ℕ⊢ (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => ↑(n α) + 1) → cardinalPartitionRel lam r γ fun α => ↑(n α) All goals completed! 🐙

Binary-color case. The $\gamma = 2$ specialization (two color classes).

@[category research open, AMS 5] theorem declaration uses 'sorry'binary_colors (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (κ : (2 : Ordinal.{u}).ToType → Cardinal.{u}) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) 2 (fun α => κ α + 1) → cardinalPartitionRel lam r 2 κ := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamκ:ToType 2 → Cardinal.{u}⊢ (cardinalPartitionRel (2 ^ lam) (r + 1) 2 fun α => κ α + 1) → cardinalPartitionRel lam r 2 κ All goals completed! 🐙

Infinite-target case. When all $\kappa_\alpha \geq \aleph_0$ are infinite and bounded by $\lambda$, $\kappa_\alpha + 1 = \kappa_\alpha$, so the hypothesis simplifies to a "pure" stepping-down lemma: $$2^\lambda \to (\kappa_\alpha){\alpha<\gamma}^{r+1} \implies \lambda \to (\kappa\alpha){\alpha<\gamma}^r.$$ The condition $\kappa\alpha \leq \lambda$ is needed to avoid a size obstruction: without it, the conclusion would require a subset of $\lambda$ of size $\kappa_\alpha > \lambda$, which is impossible (see infinite_targets_needs_bound).

@[category research open, AMS 5] theorem declaration uses 'sorry'infinite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ i, ℵ₀ ≤ κ i) (hκ_le : ∀ i, κ i ≤ lam) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γκ:γ.ToType → Cardinal.{u}hκ:∀ (i : γ.ToType), ℵ₀ ≤ κ ihκ_le:∀ (i : γ.ToType), κ i ≤ lam⊢ cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ All goals completed! 🐙

$r = 2$ case. The stepping-down from 3-uniform to 2-uniform partition relations: $2^\lambda \to (\kappa_\alpha + 1){\alpha<\gamma}^3$ implies $\lambda \to (\kappa\alpha)_{\alpha<\gamma}^2$. Generalises the classical Erdős–Rado stepping-up/down theorem for pairs.

@[category research open, AMS 5] theorem declaration uses 'sorry'r_eq_two (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) 3 γ (fun α => κ α + 1) → cardinalPartitionRel lam 2 γ κ := lam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γκ:γ.ToType → Cardinal.{u}⊢ (cardinalPartitionRel (2 ^ lam) 3 γ fun α => κ α + 1) → cardinalPartitionRel lam 2 γ κ All goals completed! 🐙 end erdos_1167.variants

A canonical element of the type (1 : Ordinal).ToType.

noncomputable def i0 : (1 : Ordinal.{u}).ToType := default

The partition relation $\mu \to (\nu)^r_1$ with a single color is equivalent to $\nu \le \mu$.

@[category API, AMS 5] lemma cardinalPartitionRel_one (μ : Cardinal.{u}) (r : ℕ) (ν : (1 : Ordinal.{u}).ToType → Cardinal.{u}) : cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν i0 := μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ (∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i) ↔ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ (∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i) → μ ≥ ν i0μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ μ ≥ ν i0 → ∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ (∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i) → μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i⊢ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = ihA:#(Quotient.out μ) = μ := mk_out μ⊢ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = ihA:#(Quotient.out μ) = μ := mk_out μi:ToType 1H:Set (Quotient.out μ)hH:#↑H = ν iright✝:∀ (s : Finset (Quotient.out μ)), s.card = r → ↑s ⊆ H → i0 = i⊢ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = ihA:#(Quotient.out μ) = μ := mk_out μi:ToType 1H:Set (Quotient.out μ)hH:#↑H = ν iright✝:∀ (s : Finset (Quotient.out μ)), s.card = r → ↑s ⊆ H → i0 = ihi:i = i0 := Subsingleton.elim i i0⊢ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = ihA:#(Quotient.out μ) = μ := mk_out μH:Set (Quotient.out μ)hH:#↑H = ν i0right✝:∀ (s : Finset (Quotient.out μ)), s.card = r → ↑s ⊆ H → i0 = i0⊢ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = ihA:#(Quotient.out μ) = μ := mk_out μH:Set (Quotient.out μ)hH:#↑H = ν i0right✝:∀ (s : Finset (Quotient.out μ)), s.card = r → ↑s ⊆ H → i0 = i0hle:#↑H ≤ #(Quotient.out μ) := mk_set_le H⊢ μ ≥ ν i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = ihA:#(Quotient.out μ) = μ := mk_out μH:Set (Quotient.out μ)hH:#↑H = ν i0right✝:∀ (s : Finset (Quotient.out μ)), s.card = r → ↑s ⊆ H → i0 = i0hle:ν i0 ≤ μ⊢ μ ≥ ν i0 All goals completed! 🐙 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ μ ≥ ν i0 → ∀ (A : Type u), #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i intro h μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type u⊢ #A = μ → ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μ⊢ ∀ (col : { s // s.card = r } → ToType 1), ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1⊢ ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i have hle : ν i0 ≤ #A := μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}⊢ cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν i0 rwa [hAμ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1⊢ ν i0 ≤ μ μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #A := Eq.mpr (id (congrArg (fun _a => ν i0 ≤ _a) hA)) hH:Set AhH:#↑H = ν i0⊢ ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #A := Eq.mpr (id (congrArg (fun _a => ν i0 ≤ _a) hA)) hH:Set AhH:#↑H = ν i0⊢ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i0 intro s μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #A := Eq.mpr (id (congrArg (fun _a => ν i0 ≤ _a) hA)) hH:Set AhH:#↑H = ν i0s:Finset Ahs:s.card = r⊢ ↑s ⊆ H → col ⟨s, hs⟩ = i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #A := Eq.mpr (id (congrArg (fun _a => ν i0 ≤ _a) hA)) hH:Set AhH:#↑H = ν i0s:Finset Ahs:s.card = rhsH:↑s ⊆ H⊢ col ⟨s, hs⟩ = i0 All goals completed! 🐙

The unrestricted version of Erdős Problem 1167 (without the condition $\gamma \geq 2$ from the original Erdős–Hajnal list) is false. Taking $\gamma = 1$, $\kappa_0 = \aleph_1$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (\aleph_1 + 1)^3_1$ holds since $2^{\aleph_0} \geq \aleph_1$, but the conclusion $\aleph_0 \to (\aleph_1)^2_1$ fails since $\aleph_0 < \aleph_1$.

@[category test, AMS 5] theorem erdos_1167.unrestricted_is_false : ¬ (∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) → cardinalPartitionRel lam r γ κ) := ⊢ ¬∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κ h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κ⊢ False h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1⊢ False have h2 : cardinalPartitionRel ((2 : Cardinal.{u}) ^ ℵ₀) 3 1 (fun _ => ℵ₁ + 1) := ⊢ ¬∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κ h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1⊢ 2 ^ ℵ₀ ≥ ℵ_ 1 + 1 h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1h3:ℵ_ 1 + 1 = ℵ_ 1 := add_one_of_aleph0_le (aleph0_le_aleph 1)⊢ 2 ^ ℵ₀ ≥ ℵ_ 1 + 1 h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1h3:ℵ_ 1 + 1 = ℵ_ 1 := add_one_of_aleph0_le (aleph0_le_aleph 1)⊢ 2 ^ ℵ₀ ≥ ℵ_ 1 All goals completed! 🐙 h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x => ℵ_ 1 + 1 := Eq.mpr (id (congrArg (fun _a => _a) (propext (cardinalPartitionRel_one (2 ^ ℵ₀) 3 fun x => ℵ_ 1 + 1)))) (have h3 := add_one_of_aleph0_le (aleph0_le_aleph 1); Eq.mpr (id (congrArg (fun _a => 2 ^ ℵ₀ ≥ _a) h3)) aleph_one_le_continuum)h3:cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h1 h2⊢ False h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x => ℵ_ 1 + 1 := Eq.mpr (id (congrArg (fun _a => _a) (propext (cardinalPartitionRel_one (2 ^ ℵ₀) 3 fun x => ℵ_ 1 + 1)))) (have h3 := add_one_of_aleph0_le (aleph0_le_aleph 1); Eq.mpr (id (congrArg (fun _a => 2 ^ ℵ₀ ≥ _a) h3)) aleph_one_le_continuum)h3:ℵ₀ ≥ ℵ_ 1⊢ False h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α => κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α => ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x => ℵ_ 1 := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 fun x => ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x => ℵ_ 1 + 1 := Eq.mpr (id (congrArg (fun _a => _a) (propext (cardinalPartitionRel_one (2 ^ ℵ₀) 3 fun x => ℵ_ 1 + 1)))) (have h3 := add_one_of_aleph0_le (aleph0_le_aleph 1); Eq.mpr (id (congrArg (fun _a => 2 ^ ℵ₀ ≥ _a) h3)) aleph_one_le_continuum)h3:ℵ₀ ≥ ℵ_ 1h4:ℵ₀ < ℵ_ 1 := aleph0_lt_aleph_one⊢ False All goals completed! 🐙

The infinite_targets variant without the bound $\kappa_\alpha \leq \lambda$ is false. Taking $\gamma = 1$, $\kappa_0 = 2^{\aleph_0}$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (2^{\aleph_0})^3_1$ holds since $2^{\aleph_0} \leq 2^{\aleph_0}$, but the conclusion $\aleph_0 \to (2^{\aleph_0})^2_1$ fails by Cantor's theorem.

@[category test, AMS 5] theorem erdos_1167.variants.infinite_targets_needs_bound : ¬ (∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ i, ℵ₀ ≤ κ i) → cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ) := ⊢ ¬∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ⊢ False h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun x => 2 ^ ℵ₀) → cardinalPartitionRel ℵ₀ 2 1 fun x => 2 ^ ℵ₀ := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 (fun x => 2 ^ ℵ₀) fun x => LT.lt.le (cantor ℵ₀)⊢ False have h2 : cardinalPartitionRel ((2 : Cardinal.{u}) ^ ℵ₀) 3 1 (fun _ => (2 : Cardinal.{u}) ^ ℵ₀) := ⊢ ¬∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ All goals completed! 🐙 h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun x => 2 ^ ℵ₀) → cardinalPartitionRel ℵ₀ 2 1 fun x => 2 ^ ℵ₀ := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 (fun x => 2 ^ ℵ₀) fun x => LT.lt.le (cantor ℵ₀)h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x => 2 ^ ℵ₀ := Eq.mpr (id (congrArg (fun _a => _a) (propext (cardinalPartitionRel_one (2 ^ ℵ₀) 3 fun x => 2 ^ ℵ₀)))) (le_refl (2 ^ ℵ₀))h3:cardinalPartitionRel ℵ₀ 2 1 fun x => 2 ^ ℵ₀ := h1 h2⊢ False h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun x => 2 ^ ℵ₀) → cardinalPartitionRel ℵ₀ 2 1 fun x => 2 ^ ℵ₀ := h 2 (le_refl 2) ℵ₀ (le_refl ℵ₀) 1 (fun x => 2 ^ ℵ₀) fun x => LT.lt.le (cantor ℵ₀)h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x => 2 ^ ℵ₀ := Eq.mpr (id (congrArg (fun _a => _a) (propext (cardinalPartitionRel_one (2 ^ ℵ₀) 3 fun x => 2 ^ ℵ₀)))) (le_refl (2 ^ ℵ₀))h3:ℵ₀ ≥ 2 ^ ℵ₀⊢ False All goals completed! 🐙 end Erdos1167