/-- **R(3, 3) ≤ 6: every red–blue colouring of the edges of K₆ has a monochromatic triangle.**
The proof of the lesson: vertex `0` has five edges, so three of them, to `x, y, z`, share a
colour `col` (`three_of_five`). If any edge among `x, y, z` also has colour `col`, it forms a
triangle with `0`; otherwise all three edges among `x, y, z` have the other colour. -/
theorem ramsey_three_three (c : Sym2 (Fin 6) → Bool) :
∃ a b d : Fin 6, a ≠ b ∧ b ≠ d ∧ a ≠ d ∧ c s(a, b) = c s(b, d) ∧ c s(b, d) = c s(a, d) := by
-- Step 1: three edges at vertex 0 with the same colour. Vertex `k.succ` is the `k`-th neighbour.
obtain ⟨col, x, y, z, hxy, hxz, hyz, hx, hy, hz⟩ := three_of_five fun k => c s(0, k.succ)
have h0x : (0 : Fin 6) ≠ x.succ := (Fin.succ_ne_zero x).symm
have h0y : (0 : Fin 6) ≠ y.succ := (Fin.succ_ne_zero y).symm
have h0z : (0 : Fin 6) ≠ z.succ := (Fin.succ_ne_zero z).symm
have hxy' : x.succ ≠ y.succ := fun h => hxy (Fin.succ_inj.1 h)
have hxz' : x.succ ≠ z.succ := fun h => hxz (Fin.succ_inj.1 h)
have hyz' : y.succ ≠ z.succ := fun h => hyz (Fin.succ_inj.1 h)
-- Step 2: an edge among `x, y, z` of colour `col` closes a triangle with `0`.
by_cases e1 : c s(x.succ, y.succ) = col
· exact ⟨0, x.succ, y.succ, h0x, hxy', h0y, hx.trans e1.symm, e1.trans hy.symm⟩
by_cases e2 : c s(x.succ, z.succ) = col
· exact ⟨0, x.succ, z.succ, h0x, hxz', h0z, hx.trans e2.symm, e2.trans hz.symm⟩
by_cases e3 : c s(y.succ, z.succ) = col
· exact ⟨0, y.succ, z.succ, h0y, hyz', h0z, hy.trans e3.symm, e3.trans hz.symm⟩
-- Step 3: otherwise `x, y, z` form a triangle of the other colour.
exact ⟨x.succ, y.succ, z.succ, hxy', hyz', hxz', bool_eq_of_ne_of_ne e1 e3,
bool_eq_of_ne_of_ne e3 e2⟩