CubicPathwidth.Alg.Proofs2.X1Relabel

Source file CubicPathwidth/Alg/Proofs2/X1Relabel.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.B2OfSimpleGraph

/-!
Stage 2 task X1: `RelabelOfSimpleGraph`.

From the Stage 1 statement `ofSimpleGraphSpec`: the nodes of `ofSimpleGraph S` are
`{v | v < n}`, `toSimpleGraph n` of it is `S`, and `Graph.toSimpleGraph` is
`SimpleGraph.fromRel` of `G.Adj`. Renaming by `Fin.val` is injective, its range is the
node set, and adjacency agrees: `fromRel` gives `i ≠ j ∧ (G.Adj i j ∨ G.Adj j i)`, and
`G.Adj j i → G.Adj i j` by symmetry, `G.Adj i j → i ≠ j` by looplessness.
-/

namespace CubicPathwidth.Alg

open Graph

/-- `ofSimpleGraph S` is `S` renamed by `Fin.val`. -/
theorem relabelOfSimpleGraph : RelabelOfSimpleGraph := by
  unfold RelabelOfSimpleGraph IsRelabel
  intro n S _inst
  obtain ⟨hWF, hNodes, hTo, -⟩ := ofSimpleGraphSpec n S
  refine ⟨Fin.val_injective, ?_, ?_⟩
  · intro v
    constructor
    · intro hv
      exact ⟨⟨v, (hNodes v).1 hv⟩, rfl⟩
    · rintro ⟨i, rfl⟩
      exact (hNodes _).2 i.isLt
  · intro i j
    have hS : S.Adj i j ↔ (Graph.toSimpleGraph (Graph.ofSimpleGraph S) n).Adj i j := by
      rw [hTo]
    rw [hS, Graph.toSimpleGraph, SimpleGraph.fromRel_adj]
    constructor
    · rintro ⟨-, h | h⟩
      · exact h
      · exact hWF.symm _ _ h
    · intro h
      refine ⟨fun hij => ?_, Or.inl h⟩
      have hij' : (i : Nat) = (j : Nat) := congrArg Fin.val hij
      rw [hij'] at h
      exact hWF.loopless _ h

#print axioms CubicPathwidth.Alg.relabelOfSimpleGraph

end CubicPathwidth.Alg