FormalConjectures.ErdosProblems.«595»

/-
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 595

References:

erdosproblems.com/595

[Er87] Erdős, Paul, Problems and results on set systems and hypergraphs. Extremal problems for finite sets (Visegrád, 1991), Bolyai Soc. Math. Stud. (1994), 217-227.

[Fo70] Folkman, Jon, Graphs with monochromatic complete subgraphs in every edge coloring. SIAM J. Appl. Math. (1970), 19:340-345.

[NeRo75] Nešetřil, Jaroslav and Rödl, Vojtěch, Type theory of partition problems of graphs. Recent advances in graph theory (Proc. Second Czechoslovak Sympos., Prague, 1974), Academia, Prague (1975), 405-412.


open SimpleGraph Set


namespace Erdos595


def IsCountableUnionOfTriangleFree {V : Type*} (G : SimpleGraph V) : Prop :=
  ∃ H : ℕ → SimpleGraph V, (∀ i, (H i).CliqueFree 3) ∧ G = ⨆ i, H i

Erdős Problem 595 ($250): Is there an infinite graph $G$ which contains no $K_4$ and is not the union of countably many triangle-free graphs?

A problem of Erdős and Hajnal [Er87].

@[category research open, AMS 5]
theorem declaration uses 'sorry'erdos_595 : answer(sorry) ↔
    ∃ (V : Type*) (_ : Infinite V) (G : SimpleGraph V),
      G.CliqueFree 4 ∧ ¬IsCountableUnionOfTriangleFree G := by⊢ True ↔ ∃ V, ∃ (_ : Infinite V), ∃ G, G.CliqueFree 4 ∧ ¬IsCountableUnionOfTriangleFree G
  sorryAll goals completed! 🐙

Folkman–Nešetřil–Rödl (finite version) [Fo70, NeRo75]: For every n ≥ 1, there exists a graph G (on a finite vertex set) that contains no $K_4$ and whose edges cannot be covered by n triangle-free graphs.

More precisely: for every n : ℕ with 1 ≤ n, there exist a finite type V and a graph G : SimpleGraph V with:

G.CliqueFree 4 (no $K_4$), and

For every family H : Fin n → SimpleGraph V of triangle-free graphs, G ≠ ⨆ i, H i.

This is the finite analogue of Problem 595. The proofs of Folkman [Fo70] and Nešetřil–Rödl [NeRo75] give different explicit constructions.

@[category research solved, AMS 5]
theorem declaration uses 'sorry'erdos_595.variants.folkman_finite : answer(True) ↔
    ∀ n : ℕ, 1 ≤ n →
    ∃ (V : Type*) (_ : Fintype V) (G : SimpleGraph V),
      G.CliqueFree 4 ∧
      ∀ (H : Fin n → SimpleGraph V), (∀ i, (H i).CliqueFree 3) → G ≠ ⨆ i, H i := by⊢ True ↔
  ∀ (n : ℕ),
    1 ≤ n → ∃ V x G, G.CliqueFree 4 ∧ ∀ (H : Fin n → SimpleGraph V), (∀ (i : Fin n), (H i).CliqueFree 3) → G ≠ ⨆ i, H i
  -- Folkman [Fo70] and Nešetřil–Rödl [NeRo75]: explicit construction exists.
  sorryAll goals completed! 🐙

Monotonicity: If G is a countable union of triangle-free graphs and H ≤ G (i.e., H is a subgraph of G), then H is also a countable union of triangle-free graphs.

Proof: If G = ⨆ i, G_i with each G_i triangle-free, then H = ⨆ i, H ⊓ G_i. Each H ⊓ G_i is triangle-free because it is a subgraph of G_i.

@[category textbook, AMS 5]
theorem erdos_595.variants.subgraph_of_countable_union
    {V : Type*} {G H : SimpleGraph V}
    (hH : H ≤ G) (hG : IsCountableUnionOfTriangleFree G) :
    IsCountableUnionOfTriangleFree H := byV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ GhG:IsCountableUnionOfTriangleFree G⊢ IsCountableUnionOfTriangleFree H
  obtain ⟨f, hf_free, hf_eq⟩ := hGV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f i⊢ IsCountableUnionOfTriangleFree H
  refine ⟨fun i => H ⊓ f i, fun i => (hf_free i).anti inf_le_right, ?_⟩V:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f i⊢ H = ⨆ i, (fun i => H ⊓ f i) i
  ext a bAdj.h.h.aV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ H.Adj a b ↔ (⨆ i, (fun i => H ⊓ f i) i).Adj a b
  simp only [iSup_adj, inf_adj]Adj.h.h.aV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ H.Adj a b ↔ ∃ i, H.Adj a b ∧ (f i).Adj a b
  constructorAdj.h.h.a.mpV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ H.Adj a b → ∃ i, H.Adj a b ∧ (f i).Adj a bAdj.h.h.a.mprV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ (∃ i, H.Adj a b ∧ (f i).Adj a b) → H.Adj a b
  ·Adj.h.h.a.mpV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ H.Adj a b → ∃ i, H.Adj a b ∧ (f i).Adj a b intro habAdj.h.h.a.mpV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vhab:H.Adj a b⊢ ∃ i, H.Adj a b ∧ (f i).Adj a b
    have habG : G.Adj a b := hH habAdj.h.h.a.mpV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vhab:H.Adj a bhabG:G.Adj a b := hH hab⊢ ∃ i, H.Adj a b ∧ (f i).Adj a b
    rw [hf_eq, iSup_adj] at habGAdj.h.h.a.mpV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vhab:H.Adj a bhabG:∃ i, (f i).Adj a b⊢ ∃ i, H.Adj a b ∧ (f i).Adj a b
    obtain ⟨i, hi⟩ := habGAdj.h.h.a.mpV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vhab:H.Adj a bi:ℕhi:(f i).Adj a b⊢ ∃ i, H.Adj a b ∧ (f i).Adj a b
    exact ⟨i, hab, hi⟩All goals completed! 🐙
  ·Adj.h.h.a.mprV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ (∃ i, H.Adj a b ∧ (f i).Adj a b) → H.Adj a b rintro ⟨i, hHab, _⟩Adj.h.h.a.mprV:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vi:ℕhHab:H.Adj a bright✝:(f i).Adj a b⊢ H.Adj a b
    exact hHabAll goals completed! 🐙

Triangle-free graphs are trivially countable unions of triangle-free graphs: if G is already triangle-free, then G = ⨆ i : ℕ, G_i where G_0 = G and G_i = ⊥ for i ≥ 1.

@[category textbook, AMS 5]
theorem erdos_595.variants.triangle_free_is_union
    {V : Type*} (G : SimpleGraph V) (hG : G.CliqueFree 3) :
    IsCountableUnionOfTriangleFree G := byV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3⊢ IsCountableUnionOfTriangleFree G
  refine ⟨fun i => if i = 0 then G else ⊥, fun i => ?_, ?_⟩refine_1V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕ⊢ ((fun i => if i = 0 then G else ⊥) i).CliqueFree 3refine_2V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3⊢ G = ⨆ i, (fun i => if i = 0 then G else ⊥) i
  ·refine_1V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕ⊢ ((fun i => if i = 0 then G else ⊥) i).CliqueFree 3 by_cases h : i = 0posV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:i = 0⊢ ((fun i => if i = 0 then G else ⊥) i).CliqueFree 3negV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:¬i = 0⊢ ((fun i => if i = 0 then G else ⊥) i).CliqueFree 3
    ·posV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:i = 0⊢ ((fun i => if i = 0 then G else ⊥) i).CliqueFree 3 simp [h, hG]All goals completed! 🐙
    ·negV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:¬i = 0⊢ ((fun i => if i = 0 then G else ⊥) i).CliqueFree 3 simp [h, cliqueFree_bot (by norm_num : 2 ≤ 3)]All goals completed! 🐙
  ·refine_2V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3⊢ G = ⨆ i, (fun i => if i = 0 then G else ⊥) i ext a brefine_2.Adj.h.h.aV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b ↔ (⨆ i, (fun i => if i = 0 then G else ⊥) i).Adj a b
    simp only [iSup_adj]refine_2.Adj.h.h.aV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b ↔ ∃ i, (if i = 0 then G else ⊥).Adj a b
    constructorrefine_2.Adj.h.h.a.mpV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b → ∃ i, (if i = 0 then G else ⊥).Adj a brefine_2.Adj.h.h.a.mprV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ (∃ i, (if i = 0 then G else ⊥).Adj a b) → G.Adj a b
    ·refine_2.Adj.h.h.a.mpV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b → ∃ i, (if i = 0 then G else ⊥).Adj a b intro habrefine_2.Adj.h.h.a.mpV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vhab:G.Adj a b⊢ ∃ i, (if i = 0 then G else ⊥).Adj a b
      exact ⟨0, byV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vhab:G.Adj a b⊢ (if 0 = 0 then G else ⊥).Adj a b simp [hab]All goals completed! 🐙⟩
    ·refine_2.Adj.h.h.a.mprV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ (∃ i, (if i = 0 then G else ⊥).Adj a b) → G.Adj a b rintro ⟨i, hi⟩refine_2.Adj.h.h.a.mprV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a b⊢ G.Adj a b
      by_cases h : i = 0posV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:i = 0⊢ G.Adj a bnegV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:¬i = 0⊢ G.Adj a b
      ·posV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:i = 0⊢ G.Adj a b simp [h] at hiposV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕh:i = 0hi:G.Adj a b⊢ G.Adj a b; exact hiAll goals completed! 🐙
      ·negV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:¬i = 0⊢ G.Adj a b simp [h] at hiAll goals completed! 🐙

The complete graph ⊤ on ℕ is a countable union of triangle-free graphs: we decompose it into the family of star graphs {H_m}_{m : ℕ}, where H_m is the graph with edges {m, n} for all n ≠ m. Each star is triangle-free (any two non-center vertices share no edge within the star), and their union covers all edges of ⊤.

Proof sketch (star triangle-free): If {a, b, c} were a triangle in H_m, then each of the three edges {a, b}, {a, c}, {b, c} would pass through m. In particular, from {a, b} we get a = m or b = m; from {b, c} we get b = m or c = m. Case analysis shows that two vertices must equal m, contradicting the triangle having three distinct vertices.

@[category textbook, AMS 5]
theorem erdos_595.variants.complete_nat_is_union :
    IsCountableUnionOfTriangleFree (⊤ : SimpleGraph ℕ) := by⊢ IsCountableUnionOfTriangleFree ⊤
  -- Star at m: edges are all {a, b} where a = m or b = m (and a ≠ b, by SimpleGraph.fromRel).
  refine ⟨fun m => SimpleGraph.fromRel (fun (a b : ℕ) => a = m ∨ b = m),
          fun m => ?_, ?_⟩refine_1m:ℕ⊢ ((fun m => fromRel fun a b => a = m ∨ b = m) m).CliqueFree 3refine_2⊢ ⊤ = ⨆ i, (fun m => fromRel fun a b => a = m ∨ b = m) i
  ·refine_1m:ℕ⊢ ((fun m => fromRel fun a b => a = m ∨ b = m) m).CliqueFree 3 -- Each star H_m is triangle-free.
    rw [CliqueFree]refine_1m:ℕ⊢ ∀ (t : Finset ℕ), ¬((fun m => fromRel fun a b => a = m ∨ b = m) m).IsNClique 3 t
    intro s hsrefine_1m:ℕs:Finset ℕhs:((fun m => fromRel fun a b => a = m ∨ b = m) m).IsNClique 3 s⊢ False
    simp only [isNClique_iff] at hsrefine_1m:ℕs:Finset ℕhs:(fromRel fun a b => a = m ∨ b = m).IsClique ↑s ∧ s.card = 3⊢ False
    obtain ⟨hs_clique, hs_card⟩ := hsrefine_1m:ℕs:Finset ℕhs_clique:(fromRel fun a b => a = m ∨ b = m).IsClique ↑shs_card:s.card = 3⊢ False
    rw [isClique_iff] at hs_cliquerefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3⊢ False
    obtain ⟨a, b, c, hab, hac, hbc, hs_eq⟩ := Finset.card_eq_three.mp hs_cardrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}⊢ False
    -- Extract membership in s.
    have ha : a ∈ s := hs_eq ▸ Finset.mem_insert_self a _refine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}⊢ False
    have hb : b ∈ s := hs_eq ▸ Finset.mem_insert.mpr
                        (Or.inr (Finset.mem_insert_self b _))refine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))⊢ False
    have hc : c ∈ s := hs_eq ▸ Finset.mem_insert.mpr
                        (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))refine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))⊢ False
    -- Each pair is adjacent in H_m.
    have hab_adj := hs_clique ha hb habrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:(fromRel fun a b => a = m ∨ b = m).Adj a b := hs_clique ha hb hab⊢ False
    have hac_adj := hs_clique ha hc hacrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:(fromRel fun a b => a = m ∨ b = m).Adj a b := hs_clique ha hb habhac_adj:(fromRel fun a b => a = m ∨ b = m).Adj a c := hs_clique ha hc hac⊢ False
    have hbc_adj := hs_clique hb hc hbcrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:(fromRel fun a b => a = m ∨ b = m).Adj a b := hs_clique ha hb habhac_adj:(fromRel fun a b => a = m ∨ b = m).Adj a c := hs_clique ha hc hachbc_adj:(fromRel fun a b => a = m ∨ b = m).Adj b c := hs_clique hb hc hbc⊢ False
    -- fromRel_adj: (fromRel r).Adj x y ↔ x ≠ y ∧ (r x y ∨ r y x)
    -- For r x y = (x = m ∨ y = m): r x y ∨ r y x simplifies to x = m ∨ y = m.
    simp only [fromRel_adj] at hab_adj hac_adj hbc_adjrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)⊢ False
    -- Extract "a = m or b = m", "a = m or c = m", "b = m or c = m".
    have ham_or_bm : a = m ∨ b = m := hab_adj.2.elim id Or.symmrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)ham_or_bm:a = m ∨ b = m := Or.elim hab_adj.right id Or.symm⊢ False
    have ham_or_cm : a = m ∨ c = m := hac_adj.2.elim id Or.symmrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)ham_or_bm:a = m ∨ b = m := Or.elim hab_adj.right id Or.symmham_or_cm:a = m ∨ c = m := Or.elim hac_adj.right id Or.symm⊢ False
    have hbm_or_cm : b = m ∨ c = m := hbc_adj.2.elim id Or.symmrefine_1m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b => a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)ham_or_bm:a = m ∨ b = m := Or.elim hab_adj.right id Or.symmham_or_cm:a = m ∨ c = m := Or.elim hac_adj.right id Or.symmhbm_or_cm:b = m ∨ c = m := Or.elim hbc_adj.right id Or.symm⊢ False
    -- Case analysis: whichever vertex equals m forces another to equal m as well,
    -- contradicting distinctness.
    rcases ham_or_bm with rfl | rflrefine_1.inls:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hs_clique:(↑s).Pairwise (fromRel fun a_1 b => a_1 = a ∨ b = a).Adjhab_adj:a ≠ b ∧ ((a = a ∨ b = a) ∨ b = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:b ≠ c ∧ ((b = a ∨ c = a) ∨ c = a ∨ b = a)ham_or_cm:a = a ∨ c = ahbm_or_cm:b = a ∨ c = a⊢ Falserefine_1.inrs:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hs_clique:(↑s).Pairwise (fromRel fun a b_1 => a = b ∨ b_1 = b).Adjhab_adj:a ≠ b ∧ ((a = b ∨ b = b) ∨ b = b ∨ a = b)hac_adj:a ≠ c ∧ ((a = b ∨ c = b) ∨ c = b ∨ a = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:a = b ∨ c = bhbm_or_cm:b = b ∨ c = b⊢ False
    ·refine_1.inls:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hs_clique:(↑s).Pairwise (fromRel fun a_1 b => a_1 = a ∨ b = a).Adjhab_adj:a ≠ b ∧ ((a = a ∨ b = a) ∨ b = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:b ≠ c ∧ ((b = a ∨ c = a) ∨ c = a ∨ b = a)ham_or_cm:a = a ∨ c = ahbm_or_cm:b = a ∨ c = a⊢ False -- a = m
      rcases hbm_or_cm with rfl | rflrefine_1.inl.inls:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:b ≠ bhac:b ≠ chs_eq:s = {b, b, c}ha:b ∈ shs_clique:(↑s).Pairwise (fromRel fun a b_1 => a = b ∨ b_1 = b).Adjhab_adj:b ≠ b ∧ ((b = b ∨ b = b) ∨ b = b ∨ b = b)hac_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:b = b ∨ c = b⊢ Falserefine_1.inl.inrs:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:c ≠ bhac:c ≠ chs_eq:s = {c, b, c}ha:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b => a = c ∨ b = c).Adjhab_adj:c ≠ b ∧ ((c = c ∨ b = c) ∨ b = c ∨ c = c)hac_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbc_adj:b ≠ c ∧ ((b = c ∨ c = c) ∨ c = c ∨ b = c)ham_or_cm:c = c ∨ c = c⊢ False
      ·refine_1.inl.inls:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:b ≠ bhac:b ≠ chs_eq:s = {b, b, c}ha:b ∈ shs_clique:(↑s).Pairwise (fromRel fun a b_1 => a = b ∨ b_1 = b).Adjhab_adj:b ≠ b ∧ ((b = b ∨ b = b) ∨ b = b ∨ b = b)hac_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:b = b ∨ c = b⊢ False exact absurd rfl habAll goals completed! 🐙   -- b = a = m
      ·refine_1.inl.inrs:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:c ≠ bhac:c ≠ chs_eq:s = {c, b, c}ha:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b => a = c ∨ b = c).Adjhab_adj:c ≠ b ∧ ((c = c ∨ b = c) ∨ b = c ∨ c = c)hac_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbc_adj:b ≠ c ∧ ((b = c ∨ c = c) ∨ c = c ∨ b = c)ham_or_cm:c = c ∨ c = c⊢ False exact absurd rfl hacAll goals completed! 🐙   -- c = a = m
    ·refine_1.inrs:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hb:b ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self b {c}))hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hs_clique:(↑s).Pairwise (fromRel fun a b_1 => a = b ∨ b_1 = b).Adjhab_adj:a ≠ b ∧ ((a = b ∨ b = b) ∨ b = b ∨ a = b)hac_adj:a ≠ c ∧ ((a = b ∨ c = b) ∨ c = b ∨ a = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:a = b ∨ c = bhbm_or_cm:b = b ∨ c = b⊢ False -- b = m
      rcases ham_or_cm with rfl | rflrefine_1.inr.inls:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:a ≠ ahbc:a ≠ chs_eq:s = {a, a, c}hb:a ∈ shs_clique:(↑s).Pairwise (fromRel fun a_1 b => a_1 = a ∨ b = a).Adjhab_adj:a ≠ a ∧ ((a = a ∨ a = a) ∨ a = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbm_or_cm:a = a ∨ c = a⊢ Falserefine_1.inr.inrs:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:a ≠ chbc:c ≠ chs_eq:s = {a, c, c}hb:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b => a = c ∨ b = c).Adjhab_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hac_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hbc_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbm_or_cm:c = c ∨ c = c⊢ False
      ·refine_1.inr.inls:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:a ≠ ahbc:a ≠ chs_eq:s = {a, a, c}hb:a ∈ shs_clique:(↑s).Pairwise (fromRel fun a_1 b => a_1 = a ∨ b = a).Adjhab_adj:a ≠ a ∧ ((a = a ∨ a = a) ∨ a = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbm_or_cm:a = a ∨ c = a⊢ False exact hab.symm rflAll goals completed! 🐙  -- a = b = m, so a = m and b = m, contradiction
      ·refine_1.inr.inrs:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert_self a {b, c}hc:c ∈ s := Eq.symm hs_eq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton_self c))))hab:a ≠ chbc:c ≠ chs_eq:s = {a, c, c}hb:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b => a = c ∨ b = c).Adjhab_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hac_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hbc_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbm_or_cm:c = c ∨ c = c⊢ False exact hbc rflAll goals completed! 🐙       -- c = b = m, so b = c, contradiction
  ·refine_2⊢ ⊤ = ⨆ i, (fun m => fromRel fun a b => a = m ∨ b = m) i -- The union ⨆ m, H_m equals ⊤.
    ext a brefine_2.Adj.h.h.aa:ℕb:ℕ⊢ ⊤.Adj a b ↔ (⨆ i, (fun m => fromRel fun a b => a = m ∨ b = m) i).Adj a b
    simp only [iSup_adj, fromRel_adj, top_adj]refine_2.Adj.h.h.aa:ℕb:ℕ⊢ a ≠ b ↔ ∃ i, a ≠ b ∧ ((a = i ∨ b = i) ∨ b = i ∨ a = i)
    -- Goal: a ≠ b ↔ ∃ m, a ≠ b ∧ ((a = m ∨ b = m) ∨ (b = m ∨ a = m))
    exact ⟨fun hab => ⟨a, hab, Or.inl (Or.inl rfl)⟩,
           fun ⟨_, hne, _⟩ => hne⟩All goals completed! 🐙

The complete graph ⊤ on Fin 4 is not $K_4$-free: ⊤ on Fin 4 equals the complete graph $K_4$, so it contains $K_4$ as a subgraph and is not $K_4$-free.

This sanity check confirms the $K_4$-free hypothesis of Problem 595 is non-trivial.

@[category textbook, AMS 5]
theorem erdos_595.variants.K4_not_cliqueFree :
    ¬ (⊤ : SimpleGraph (Fin 4)).CliqueFree 4 := by⊢ ¬⊤.CliqueFree 4
  rw [not_cliqueFree_iff]⊢ Nonempty (completeGraph (Fin 4) ↪g ⊤)
  exact ⟨(Iso.completeGraph (Fintype.equivFin (Fin 4))).symm.toEmbedding⟩All goals completed! 🐙

Reformulation via edge colourings: A graph G is a countable union of triangle-free graphs if and only if there is a colouring of the edges of G by ℕ such that no monochromatic triangle exists.

More precisely: IsCountableUnionOfTriangleFree G is equivalent to the existence of a map c : G.edgeSet → ℕ such that for each n : ℕ, the subgraph of edges coloured n is triangle-free.

@[category test, AMS 5]
theorem erdos_595.variants.reformulation_edge_colouring {V : Type*} (G : SimpleGraph V) :
    IsCountableUnionOfTriangleFree G ↔
    ∃ c : G.edgeSet → ℕ,
      ∀ n : ℕ,
        (SimpleGraph.fromEdgeSet {e | ∃ h : e ∈ G.edgeSet, c ⟨e, h⟩ = n}).CliqueFree 3 := byV:Type u_1G:SimpleGraph V⊢ IsCountableUnionOfTriangleFree G ↔ ∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3
  -- Note: `c : G.edgeSet → ℕ` is exactly `EdgeLabeling G ℕ`, and the `fromEdgeSet` expression
  -- is exactly `EdgeLabeling.labelGraph c n`. We use `EdgeLabeling.iSup_labelGraph` for (←).
  constructormpV:Type u_1G:SimpleGraph V⊢ IsCountableUnionOfTriangleFree G → ∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3mprV:Type u_1G:SimpleGraph V⊢ (∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3) →
  IsCountableUnionOfTriangleFree G
  ·mpV:Type u_1G:SimpleGraph V⊢ IsCountableUnionOfTriangleFree G → ∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3 -- (→): Given H : ℕ → SimpleGraph V with G = ⨆ H i and each H i triangle-free,
    -- construct c : G.edgeSet → ℕ by choosing some i containing each edge classically.
    rintro ⟨H, hH_free, hH_eq⟩mpV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H i⊢ ∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3
    -- For each edge e = s(a,b) of G, use iSup_adj to find some H i containing it.
    -- We use Sym2.ind to destructure e into s(a,b) form and then apply mem_edgeSet + iSup_adj.
    have hcov : ∀ e : G.edgeSet, ∃ i, (e : Sym2 V) ∈ (H i).edgeSet :=
      fun ⟨e, he⟩ => Sym2.ind (fun a b he => byV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ix✝:↑G.edgeSete:Sym2 Vhe✝:e ∈ G.edgeSeta:Vb:Vhe:s(a, b) ∈ G.edgeSet⊢ ∃ i, ↑⟨s(a, b), he⟩ ∈ (H i).edgeSet
        rw [hH_eq, mem_edgeSet, iSup_adj] at heV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ix✝:↑G.edgeSete:Sym2 Vhe✝¹:e ∈ G.edgeSeta:Vb:Vhe✝:s(a, b) ∈ G.edgeSethe:∃ i, (H i).Adj a b⊢ ∃ i, ↑⟨s(a, b), he⟩ ∈ (H i).edgeSet
        exact he.imp fun i hi => hiAll goals completed! 🐙) e he
    -- Define c by classical choice of the covering index.
    refine ⟨fun e => (hcov e).choose, fun n => ?_⟩mpV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕ⊢ (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), (fun e => ⋯.choose) ⟨e, h⟩ = n}).CliqueFree 3
    -- Show the subgraph of edges coloured n is a subgraph of H n, hence triangle-free.
    apply (hH_free n).antimpV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕ⊢ fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), (fun e => ⋯.choose) ⟨e, h⟩ = n} ≤ H n
    intro x ympV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕx:Vy:V⊢ (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), (fun e => ⋯.choose) ⟨e, h⟩ = n}).Adj x y → (H n).Adj x y hxympV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕx:Vy:Vhxy:(fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), (fun e => ⋯.choose) ⟨e, h⟩ = n}).Adj x y⊢ (H n).Adj x y
    rw [fromEdgeSet_adj] at hxympV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕx:Vy:Vhxy:s(x, y) ∈ {e | ∃ (h : e ∈ G.edgeSet), (fun e => ⋯.choose) ⟨e, h⟩ = n} ∧ x ≠ y⊢ (H n).Adj x y
    obtain ⟨⟨h_mem, h_eq⟩, _⟩ := hxympV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕx:Vy:Vright✝:x ≠ yh_mem:s(x, y) ∈ G.edgeSeth_eq:(fun e => ⋯.choose) ⟨s(x, y), h_mem⟩ = n⊢ (H n).Adj x y
    -- h_eq : (hcov ⟨s(x,y), h_mem⟩).choose = n
    -- choose_spec gives s(x,y) ∈ (H (choose)).edgeSet; after rewriting with h_eq, in H n.
    have hspec := (hcov ⟨s(x, y), h_mem⟩).choose_specmpV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕx:Vy:Vright✝:x ≠ yh_mem:s(x, y) ∈ G.edgeSeth_eq:(fun e => ⋯.choose) ⟨s(x, y), h_mem⟩ = nhspec:↑⟨s(x, y), h_mem⟩ ∈ (H ⋯.choose).edgeSet := Exists.choose_spec (hcov ⟨s(x, y), h_mem⟩)⊢ (H n).Adj x y
    simp only [h_eq] at hspecmpV:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSet := 
  fun x =>
    match x with
    | ⟨e, he⟩ =>
      Sym2.ind
        (fun a b he =>
          Exists.imp (fun i hi => hi)
            (Eq.mp (congrArg (fun _a => _a) (propext iSup_adj))
              (Eq.mp (congrArg (fun _a => _a) (propext (mem_edgeSet (⨆ i, H i))))
                (Eq.mp (congrArg (fun _a => s(a, b) ∈ _a.edgeSet) hH_eq) he))))
        e hen:ℕx:Vy:Vright✝:x ≠ yh_mem:s(x, y) ∈ G.edgeSeth_eq:(fun e => ⋯.choose) ⟨s(x, y), h_mem⟩ = nhspec:s(x, y) ∈ (H n).edgeSet⊢ (H n).Adj x y
    exact hspecAll goals completed! 🐙
  ·mprV:Type u_1G:SimpleGraph V⊢ (∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3) →
  IsCountableUnionOfTriangleFree G -- (←): Given c : G.edgeSet → ℕ, define H n = fromEdgeSet {e | ∃ h, c ⟨e,h⟩ = n}.
    -- This is EdgeLabeling.labelGraph c n, so ⨆ n, H n = G by iSup_labelGraph.
    rintro ⟨c, hc⟩mprV:Type u_1G:SimpleGraph Vc:↑G.edgeSet → ℕhc:∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3⊢ IsCountableUnionOfTriangleFree G
    refine ⟨fun n => SimpleGraph.fromEdgeSet {e | ∃ h : e ∈ G.edgeSet, c ⟨e, h⟩ = n},
            hc, ?_⟩mprV:Type u_1G:SimpleGraph Vc:↑G.edgeSet → ℕhc:∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3⊢ G = ⨆ i, (fun n => fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}) i
    -- G = ⨆ n, (labelGraph c n) follows from EdgeLabeling.iSup_labelGraph.
    exact (EdgeLabeling.iSup_labelGraph (G := G) c).symmAll goals completed! 🐙


end Erdos595