a construction of the Mycielskian (https://en.wikipedia.org/wiki/Mycielskian)

mycielskian.lean

import data.fintype tactic.ring

structure graph :=
(vertex : Type*)
(edge   : vertex → vertex → bool)

namespace graph

class undirected (G : graph) :=
(symm : ∀ x y : G.vertex, G.edge x y = G.edge y x)

protected def symm {G  : graph} [undirected G] : ∀ x y, G.edge x y = G.edge y x :=
undirected.symm

structure coloring (G : graph) (α : Type*) :=
(func  : G.vertex → α)
(nonadj : ∀ {x y : G.vertex}, G.edge x y = tt → func x ≠ func y)

instance {G : graph} {α : Type*} : has_coe_to_fun (coloring G α) :=
⟨λ c, G.vertex → α, λ c, c.func⟩

def colorable (G : graph) (k : nat) := 
  ∃ (α : Type*) [h : fintype α] [decidable_eq α] (c : coloring G α), @fintype.card α h = k 

def is_triangle {G : graph} (x y z : G.vertex) : bool :=
G.edge x y && G.edge y z && G.edge z x

end graph

section

inductive mvertex (α : Type*)
| orig   : α → mvertex
| copy   : α → mvertex
| hub {} : mvertex

open graph mvertex fintype

def mvertex_equiv (α : Type*) : mvertex α ≃ (α ⊕ α ⊕ unit) :=
{ to_fun    := λ v, match v with
               | (orig x) := sum.inl x
               | (copy x) := sum.inr (sum.inl x)
               | hub      := sum.inr (sum.inr ())
               end,
  inv_fun   := λ v, match v with 
              | (sum.inl x)           := orig x
              | (sum.inr (sum.inl x)) := copy x
              | (sum.inr (sum.inr _)) := hub
              end,
  left_inv  := by { intro v, cases v; refl },
  right_inv := by { intro v, repeat { cases v, refl } } }

instance (α : Type*) [h : fintype α] : fintype (mvertex α) :=
fintype.of_equiv _ (mvertex_equiv α).symm

theorem card_mvertex (α : Type*) [fintype α] : card (mvertex α) = 2 * card α + 1 :=
(card_congr (mvertex_equiv α)).trans (by simp; ring)

def medge (G : graph) : mvertex G.vertex → mvertex G.vertex → bool
| hub      hub      := ff
| hub      (orig y) := ff
| (orig x) hub      := ff
| hub      (copy y) := tt
| (copy x) hub      := tt
| (orig x) (orig y) := G.edge x y
| (orig x) (copy y) := G.edge x y
| (copy x) (orig y) := G.edge x y
| (copy x) (copy y) := ff

def mycielskian (G : graph) : graph :=
{ vertex := mvertex G.vertex,
  edge   := medge G }

theorem edge_mycielskian (G : graph) : (mycielskian G).edge = medge G :=
rfl

instance fintype_vertex_mycielskian (G : graph) [fintype G.vertex] : 
  fintype (mycielskian G).vertex :=
by { unfold mycielskian, apply_instance }

@[instance] 
def undirected_mycielskian (G : graph) [h : undirected G] : undirected (mycielskian G) :=
begin
  constructor,
  intro x; cases x; intro y; cases y; dsimp [mycielskian, medge]; refl <|> apply graph.symm
end

theorem card_mycielskian (G : graph) [fintype G.vertex] : 
  card (mycielskian G).vertex = 2 * card G.vertex + 1 :=
card_mvertex _

theorem exists_triangle_of_exists_triangle_mycielskian {G : graph} 
    (h : ∃ x y z : (mycielskian G).vertex, is_triangle x y z) : 
  ∃ x y z : G.vertex, is_triangle x y z :=
begin
  rcases h with ⟨x | x | _, y | y | _, z | z | _, h⟩;
    simp [is_triangle, edge_mycielskian, medge] at h; try { contradiction };
    use [x, y, z]; simp [is_triangle, h]
end

private def aux {G : graph} {α : Type*} [decidable_eq α] (f : (mycielskian G).vertex → α) :
    G.vertex → α :=
λ x, if f (orig x) = f hub then f (copy x) else f (orig x)

private theorem aux' {G : graph} {α : Type*} [decidable_eq α] (c : coloring (mycielskian G) α) :
  ∀ x : G.vertex, aux c x ≠ c hub :=
begin
  intro x, by_cases h : c (orig x) = c hub; simp [aux, h],
  apply c.nonadj, refl
end

theorem coloring_of_coloring_mycielskian {G : graph} {α : Type*} [decidable_eq α] 
    (c : coloring (mycielskian G) α) :
  coloring G {a // a ≠ c hub} :=
{ func := λ a, ⟨aux c a, aux' c a⟩,
  nonadj := (λ x y h h',
    have h₁ : aux c x = aux c y, 
      from subtype.mk_eq_mk.1 h',
    begin
      by_cases h₂ : c (orig x) = c hub; by_cases h₃ : c (orig y) = c hub,
      { apply c.nonadj _ (h₂.trans h₃.symm), exact h },
      repeat { simp [aux, h₂, h₃] at h₁, apply c.nonadj _ h₁, exact h }
    end) }

theorem {u v} colorable_of_colorable_mycielskian {G : graph.{u}} {k : ℕ} : 
  colorable.{u v} (mycielskian G) (k + 1) → colorable.{u v} G k :=
begin
  rintros ⟨α, finα, deceqα, c, cardα⟩,
  haveI := finα, haveI := deceqα,
  refine ⟨{a // a ≠ c hub}, _, _, coloring_of_coloring_mycielskian c, _⟩,
  repeat { apply_instance },
  calc
    card {a // a ≠ c hub} 
          = finset.card (@finset.univ α _ \ {c hub}) :
              by { rw subtype_card, congr, ext, simp, refl }
      ... = k + 1 - 1 : 
              by { rw [finset.card_sdiff (finset.subset_univ _), finset.card_univ], 
                   congr, convert cardα }
      ... = k : rfl
end

def iterated_mycielskian (G : graph) : ℕ → graph
| 0     := G
| (n+1) := mycielskian (iterated_mycielskian n)

theorem {u v} colorable_of_colorable_iterated_mycielskian {G : graph.{u}} {k n : ℕ} : 
  colorable.{u v} (iterated_mycielskian G n) (k + n) → colorable.{u v} G k :=
by { induction n with n ih, exact id, exact ih ∘ colorable_of_colorable_mycielskian }

theorem exists_triangle_of_exists_triangle_iterated_mycielskian {G : graph} {n : ℕ} :
  (∃ x y z : (iterated_mycielskian G n).vertex, is_triangle x y z) → 
    ∃ x y z : G.vertex, is_triangle x y z :=
by { induction n with n ih, exact id, exact ih ∘ exists_triangle_of_exists_triangle_mycielskian }

instance fintype_vertex_iterated_mycielskian (G : graph) [fintype G.vertex] (n : ℕ): 
  fintype (iterated_mycielskian G n).vertex :=
by { induction n with n ih, assumption, exact @fintype_vertex_mycielskian _ ih }

theorem card_iterated_mycielskian (G : graph) [fintype G.vertex] (n : ℕ) : 
  card (iterated_mycielskian G n).vertex = 2^n * (card G.vertex + 1) - 1 :=
begin
  induction n with n ih; simp [iterated_mycielskian],
  rw [card_mycielskian, ih, nat.pow_succ, nat.left_distrib, nat.left_distrib, 
    nat.mul_sub_left_distrib], ring, 
  rw [nat.sub_add_eq_add_sub],
  { apply nat.succ_sub_succ },
  change 2 * 1 ≤ _, apply mul_le_mul; try {simp},
  change 2^0 ≤ _, apply nat.pow_le_pow_of_le_right; norm_num
end

end