Formalizing Graph Theory - The Odd Cycle Theorem in Lean

Stream: mathlib4

[Nick Adfor]

The following is trying to prove a TODO in
https://github.com/leanprover-community/mathlib4/blob/v4.26.0/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean from @Mitchell Horner with one sorry left in Theorem "No Odd Cycles Implies Bipartite". I'm trying to fill the sorry (just try because I cannot ensure that the mathematical proof is suitable. It has not been checked mathematically)

1. Establish Component-Wise Structure

   The proof proceeds by analyzing each connected component of the graph independently. Since a graph is bipartite if and only if every connected component is bipartite, it suffices to prove the theorem for connected graphs. For disconnected graphs, we apply the same reasoning to each component separately and then combine the resulting colorings. This reduction allows us to assume, without loss of generality, that the graph G is connected for the remainder of the argument.

2. Define a Candidate Coloring Based on Distance Parity

   Select an arbitrary vertex r in V as a root. For any vertex v ∈ V, define a coloring function color(v) as the parity (modulo 2) of the graph distance dist_G(r, v). Specifically, color(v) = 0 if the distance is even and color(v) = 1 if the distance is odd. This definition is intuitive: vertices at even distances from the root are assigned one color, and vertices at odd distances are assigned the other.

3. Verify the Coloring is Well-Defined

   A potential issue arises: the distance dist_G(r, v) is defined as the length of a shortest path, but there might be multiple shortest paths. We must show that all shortest paths from r to any vertex v have the same parity. Suppose, for contradiction, that there exist two paths p₁ and p₂ from r to v such that length(p₁) is even and length(p₂) is odd. The concatenation of p₁ with the reverse of p₂ forms a closed walk from r to r. While this closed walk might not be a simple cycle, it contains a cycle (by standard graph theory lemmas about walks). The total length of this closed walk is length(p₁) + length(p₂), which is odd. Since an odd closed walk must contain an odd cycle, this contradicts the hypothesis that all cycles in G have even length. Therefore, the parity of the distance is uniquely determined.

4. Prove Adjacent Vertices Receive Different Colors

   Consider an edge (u, v) ∈ G.edgeSet. We aim to show color(u) ≠ color(v). Assume, for contradiction, that color(u) = color(v), meaning dist_G(r, u) and dist_G(r, v) have the same parity. Let p be a shortest path from r to u. Consider the walk formed by concatenating p, the single edge (u, v), and then a shortest path from v back to r. The length of this closed walk is dist_G(r, u) + 1 + dist_G(r, v). Since the two distances have the same parity, their sum is even, and adding 1 makes the total length odd. This closed walk, being of odd length, must contain an odd cycle (again, by the property that any odd closed walk contains an odd cycle). This contradicts the assumption that all cycles are even. Hence, adjacent vertices must have different colors.

5. Construct the Bipartite Structure

   The function color : V → Fin 2 defined above satisfies the condition of a proper 2-coloring: for every edge (u, v), we have color(u) ≠ color(v). This is precisely the definition of a SimpleGraph.Coloring (Fin 2). Therefore, we can construct a coloring object and conclude that G is bipartite, as G.IsBipartite is defined by the existence of such a coloring.

6. Address the Empty Graph and Corner Cases

   If the vertex set V is empty, the statement holds vacuously. If the graph has no edges, any coloring is valid, so the graph is trivially bipartite. The proof outlined above covers the non-trivial case where G has at least one edge and is connected. The formalization in Lean would need to handle these degenerate cases explicitly, though they are straightforward.

import Mathlib


variable {V : Type*} [DecidableEq V] (G : SimpleGraph V)

set_option linter.unusedSectionVars false

lemma even_length_iff_same_color
    {c : G.Coloring (Fin 2)}
    {u v : V} (p : G.Walk u v) :
    Even p.length ↔ c u = c v := by
  induction p with
  | nil =>
    -- Base case: length 0 is even, c u = c u is true
    simp
  | cons h_adj p_tail ih =>
    -- Inductive step
    -- Goal: Even (cons ...).length ↔ c u = c w
    have h_first_step_diff := c.valid h_adj
    rw [SimpleGraph.Walk.length_cons]
    rw [Nat.even_add_one] -- 1 + x is even <-> x is odd

    -- Using induction hypothesis ih: Even p_tail.length ↔ c v = c w
    rw [ih]

    -- Now the goal becomes: ¬(c v = c w) ↔ c u = c w
    constructor
    · -- Direction 1: (c next ≠ c end) -> (c start = c end)
      intro h_next_ne_end

      have h_cases : c u = 0 ∨ c u = 1 := by
        match c u with
        | 0 => left; rfl
        | 1 => right; rfl

      cases h_cases
      · -- Case 1: c u = 0
        simp_all
        omega
      · -- Case 2: c u = 1
        simp_all
        omega
    · -- Direction 2: (c start = c end) -> (c next ≠ c end)
      intro h_start_eq_end
      -- Given: start ≠ next
      -- Replacing start with end, we get end ≠ next
      rw [h_start_eq_end] at h_first_step_diff
      exact h_first_step_diff.symm

/-- Our target theorem: G is bipartite ↔ All cycles in G have even length -/
-- Proof of necessity
theorem bipartite_implies_even_cycles (h : G.IsBipartite) :
    ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length := by
  -- 1. Since it's a bipartite graph, there exists a 2-coloring scheme (color : V -> Bool)
  rcases h with ⟨color⟩
  -- 2. Analyze any cycle c
  intro v c hc

  -- 3. Use Walk property: In a bipartite graph, if a path has same start and end color,
  --    then the path length must be even.
  --    A cycle starts and ends at the same point v, so colors are obviously the same.
  have h_color_eq : color v = color v := rfl

  -- 4. Call the lemma about bipartite path parity in Mathlib
  -- (SimpleGraph.Coloring.valid_walk_length_even_iff)
  rw [even_length_iff_same_color]
  exact color

namespace SimpleGraph.Walk

-- Helper lemma 1: The prefix of a shortest path is also a shortest path
lemma dist_eq_length_takeUntil {u v x : V} (p : G.Walk u v) (hp : p.IsPath)
    (hp_len : p.length = G.dist u v) (hx : x ∈ p.support) :
    (p.takeUntil x hx).length = G.dist u x := by
  -- Strategy: Prove takeUntil yields a path, and length ≤ dist
  -- Since dist ≤ length of any walk, they are equal
  let p_to_x := p.takeUntil x hx

  -- p_to_x is a path
  have hp_to_x : p_to_x.IsPath := by
    have : (p.takeUntil x hx).append (p.dropUntil x hx) = p := p.take_spec hx
    exact hp.takeUntil _
  -- p_to_x.length ≤ p.length
  have h_le : p_to_x.length ≤ p.length := SimpleGraph.Walk.length_takeUntil_le p hx
  have h_triangle : G.dist u v ≤ G.dist u x + G.dist x v := by
    by_cases h : G.Reachable u x ∧ G.Reachable x v;
    · obtain ⟨q, hq⟩ : ∃ q : G.Walk u x, q.length = G.dist u x := by
        have := h.1;
        exact Reachable.exists_walk_length_eq_dist this
      obtain ⟨r, hr⟩ : ∃ r : G.Walk x v, r.length = G.dist x v := by
        obtain ⟨r, hr⟩ : ∃ r : G.Walk x v, r.length = G.dist x v := by
          have h_reachable : G.Reachable x v := h.right
          exact Reachable.exists_walk_length_eq_dist h_reachable
        use r;
      exact SimpleGraph.dist_le ( q.append r ) |> le_trans <| by simp +decide [ hq, hr ] ;
    · cases hp_to_x ; simp_all +decide [ SimpleGraph.Reachable ];
      contrapose! h;
      exact ⟨ p_to_x, ⟨ p.dropUntil x hx ⟩ ⟩
  have h_dist_xv_le : G.dist x v ≤ (p.dropUntil x hx).length := SimpleGraph.dist_le (p.dropUntil x hx)

  have h_eq_parts : p.length = p_to_x.length + (p.dropUntil x hx).length := by
    have := congr_arg Walk.length (p.take_spec hx)
    -- The length of the appended walk is the sum of the lengths of the two parts.
    rw [← this];
    -- The length of the appended walk is the sum of the lengths of the two parts by definition.
    apply SimpleGraph.Walk.length_append
  have h_upper : p_to_x.length ≤ G.dist u x := by
    rw [hp_len] at h_eq_parts
    have := calc G.dist u v
      _ ≤ G.dist u x + G.dist x v := h_triangle
      _ ≤ G.dist u x + (p.dropUntil x hx).length := Nat.add_le_add_left h_dist_xv_le _
    omega
  refine' le_antisymm h_upper _;
  exact dist_le (p.takeUntil x hx)

-- Helper lemma 2: Length of the suffix of a shortest path
lemma length_dropUntil_eq_dist_sub {u v x : V} (p : G.Walk u v) (hp : p.IsPath)
    (hp_len : p.length = G.dist u v) (hx : x ∈ p.support) :
    (p.dropUntil x hx).length = G.dist u v - G.dist u x := by
  have h1 := congr_arg Walk.length (p.take_spec hx)
  have h4 : (p.takeUntil x hx).length = G.dist u x := by
    rw [ SimpleGraph.Walk.dist_eq_length_takeUntil ];
    · assumption;
    · exact hp_len;
  rw [ ← h4, ← hp_len, ← h1, SimpleGraph.Walk.length_append ] ; aesop

-- Proof of sufficiency: If all cycles have even length, then the graph is bipartite
theorem no_odd_cycles_implies_bipartite (h : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length) :
    G.IsBipartite := by sorry

theorem bipartite_iff_all_cycles_even :
  G.IsBipartite ↔ ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length := by
  constructor
  · -- Forward direction: G is bipartite → all cycles have even length
    intro h_bip
    exact bipartite_implies_even_cycles G h_bip
  · -- Reverse direction: all cycles have even length → G is bipartite
    intro h_even
    exact no_odd_cycles_implies_bipartite G h_even

[Snir Broshi]

#Is there code for X? > bipartite iff does not contain an odd cycle

[Snir Broshi]

Can I ask that if you used AI to write the big message/code that you please disclose it? If not, ignore this

[Yaël Dillies]

(Nick uses LLMs to translate from Chinese)

[Jakub Nowak]

We already have bipartite_implies_even_cycles (without IsCycle assumption, which is not needed, and you also doesn't use it in your proof). SimpleGraph.two_colorable_iff_forall_loop_even

I know of two ways to prove bipartite_iff_all_cycles_even. One, that you write about, requires lemma that odd closed walk contains odd cycle. I have a proof of this here #Is there code for X? > bipartite iff does not contain an odd cycle @ 💬, it's not in mathlib yet though. That lemma and SimpleGraph.two_colorable_iff_forall_loop_even is all you need to prove bipartite_iff_all_cycles_even, this is because SimpleGraph.two_colorable_iff_forall_loop_even already proves all the other details of your proof, like "graph is bipartite if and only if every connected component is bipartite" and constructing the coloring.

That two helper lemmas you have might be useful for a different proof I have in mind. That is, constructing the odd cycle directly, without going through odd closed walk. The idea of that proof, is that you start with an arbitrary BFS tree rooted in r. Then, in the part of the proof were you take (u, v) ∈ G.edgeSet and assume dist_G(r, u) and dist_G(r, v) have the same parity. You take a vertex z that is the lowest common ancestor of u and v in the tree. You have to disprove the cases z = u and z = v using parity assumption. If z ≠ u and z ≠ v then concatenating the path from z to u, edge u v, and the path from v to z, yields a cycle (and not just a closed walk). And it is an odd cycle because of the parity assumption.

A proof that uses arbitrary shortest paths, instead of starting with BFS tree might also be possible, but I haven't given it much thought. You would have to deal with a few more cases. One being, that the lowest point where the path r->u meets with the path r->v, and the lowest point where that path r->v meets with the path r->u could be different (I think that's impossible possible from the assumption that these paths are the shortest paths?)

[Jakub Nowak]

(deleted)

[Jakub Nowak]

The "graph is bipartite if and only if every connected component is bipartite" part was actually very nontrivial and we have to thank @John Talbot for his work on it. :)

[Nick Adfor]

Snir Broshi said:

Can I ask that if you used AI to write the big message/code that you please disclose it? If not, ignore this

The origin code comments are Chinese :( maybe I should write another pure English version.

As for the "long math proof" about Theorem "No Odd Cycles Implies Bipartite", I should say that I do not understand it very well. The more precise proof is in the textbook (I can provide a picture)

[Nick Adfor]

precise and concise proof.jpg

[Jakub Nowak]

I think that "Since the first vertex of each of these walks is x there is a vertex z that is the last common vertex of these two walks" is not true.
This is because you can take the last vertex on the walk x⋯a that is common with the walk x⋯b, and you can take the last vertex on the walk x⋯b that is common with the walk x⋯a. And these two are not necessarily equal.

[Nick Adfor]

Jakub Nowak said:

A proof that uses arbitrary shortest paths, instead of starting with BFS tree might also be possible, but I haven't given it much thought. You would have to deal with a few more cases. One being, that the lowest point where the path r->u meets with the path r->v, and the lowest point where that path r->v meets with the path r->u could be different (I think that's impossible from the assumption that these paths are the shortest paths?)

Since you refered to "that's impossible", I would consider give up that :(

[Jakub Nowak]

Oh no, sorry, that was a typo, I meant possible, not impossible.

[Jakub Nowak]

I meant that the last vertex on the path x⋯a that is common with the path x⋯b, and the last vertex on the path x⋯b that is common with the path x⋯a are not necessarily equal for arbitrary paths. For example, they aren't equal for paths x u v a and x v u b. However, I suspect that they must be equal if you also take into consideration that these paths are the shortest paths. And your dist_eq_length_takeUntil lemma is I think useful in a proof of that equality.

[Nick Adfor]

Jakub Nowak said:

I meant that the last vertex on the path x⋯a that is common with the path x⋯b, and the last vertex on the path x⋯b that is common with the path x⋯a are not necessarily equal for arbitrary paths. For example, they aren't equal for paths x u v a and x v u b. However, I suspect that they must be equal if you also take into consideration that these paths are the shortest paths. And your dist_eq_length_takeUntil lemma is I think useful in a proof of that equality.

Is there difference between the proof 11.4.1 in my posted picture and the code already posted in #Is there code for X? > bipartite iff does not contain an odd cycle

[Jakub Nowak]

Nick_adfor said:

Is there difference between the proof 11.4.1 in my posted picture and the code already posted in #Is there code for X? > bipartite iff does not contain an odd cycle

You mean the proof that defines odd_cycle_of_odd_walk? I think, these two are very different. The proof via odd_cycle_of_odd_walk is pretty much the same proof you described in your first post in this topic #mathlib4 > Formalizing Graph Theory - The Odd Cycle Theorem in Lean @ 💬.

The proof of 11.4.1 and your have common parts, but they diverge in how the odd cycle is constructed. Your proof constructs an odd closed walk, and then invokes on the lemma that you can extract odd cycle from odd closed walk. The proof of 11.4.1 tries to construct odd cycle directly, without going through odd closed walk.

[Nick Adfor]

Jakub Nowak said:

I think that "Since the first vertex of each of these walks is x there is a vertex z that is the last common vertex of these two walks" is not true.
This is because you can take the last vertex on the walk x⋯a that is common with the walk x⋯b, and you can take the last vertex on the walk x⋯b that is common with the walk x⋯a. And these two are not necessarily equal.

Yes, and till now I've not introduced any definition. I may think that I need a new def on "the last common vertex". The "… is not true" might be because it is not-well-defined

[Nick Adfor]

Finish bipartite_iff_all_cycles_even.lean

[Nick Adfor]

This is generated by Aristotle. It focus on a definition in Mathlib "bypass". What is "bypass"?...... It's not in the textbook, just in Mathlib. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Paths.html

[Nick Adfor]

I try to explain what happened to the proof. First this theorem no_odd_cycles_implies_bipartite (also in the textbook, see the picture) relies on the well-definition about the last common vertex, but now we don't have a well-definition (see what Jakub Nowak has said before). So anything connected with that should be deleted. That is to delete the second part of the constructor.

/- Aristotle failed to find a proof. -/
theorem no_odd_cycles_implies_bipartite (h : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length) :
    G.IsBipartite := by sorry

theorem bipartite_iff_all_cycles_even :
  G.IsBipartite ↔ ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length := by
  constructor
  · intro h_bip
    exact bipartite_implies_even_cycles G h_bip
  · intro h_even
    exact no_odd_cycles_implies_bipartite G h_even -- replace this line with `sorry`

And in this way, Aristotle was able to rely on another well-definition already in Mathlib, that is "bypass".

[Nick Adfor]

Very thanks for @Kyle Miller's work to introduce definition about "bypass", which solves this problem on The Odd Cycle Theorem, (though I'm not so familiar with the definition and unable to find some references)

[Snir Broshi]

So did you prove it? Is there a PR?

[Nick Adfor]

Snir Broshi said:

So did you prove it? Is there a PR?

There's a file but not a PR yet

[Nick Adfor]

Nick_adfor said:

Finish bipartite_iff_all_cycles_even.lean

Here

[Jakub Nowak]

I though that docs#Walk.bypass couldn't be useful for this theorem, but going away from closed walks to prove Even p.length ↔ Even p.bypass.length by induction was pretty clever. The proof made by AI is much more complicated than it could be, I think for mathlib PR a human would have to redo the proofs. I did rewrite part of the proof and I think that it could end up being a very nice proof, probably shorter and simpler than mine.

[Mitchell Horner]

When I wrote that todo I imagined a proof in terms of containment.

theorem SimpleGraph.Walk.IsCycle.adj_getVert_of_cycleGraph_adj
    {v} {p : G.Walk v v} (h : p.IsCycle)
    {i j : Fin (p.length)} (hadj : (cycleGraph p.length).Adj i j) :
    G.Adj (p.getVert i) (p.getVert j) := by
  rcases eq_zero_or_neZero p.length with heq | _
  · rw [heq] at i
    exact i.elim0
  · wlog hlt : i < j generalizing i j
    · rw [G.adj_comm]
      apply this hadj.symm
      exact lt_of_le_of_ne (le_of_not_gt hlt) hadj.symm.ne
    · by_cases hi : i = 0
      · simp_rw [hi, cycleGraph_adj', zero_sub, sub_zero, Fin.neg_def,
          Nat.mod_eq_of_lt (by omega : p.length - j < p.length), Nat.sub_eq_iff_eq_add j.is_lt.le,
          ← Nat.sub_eq_iff_eq_add' (by omega : 1 ≤ p.length), eq_comm] at hadj
        rcases hadj with hsnd | hpen
        · simp_rw [hi, Fin.val_zero, hsnd, Walk.getVert_zero]
          exact (p.adj_penultimate h.not_nil).symm
        · simp_rw [hi, Fin.val_zero, hpen]
          exact p.adj_getVert_succ (by omega : 0 < p.length)
      · have hsub : j - i < p.length - 1 := (Nat.le_pred_of_lt j.is_lt).trans' <|
            Nat.sub_lt_self (Nat.pos_of_ne_zero <| Fin.val_eq_zero_iff.ne.mpr hi) hlt.le
        simp_rw [cycleGraph_adj', Fin.coe_sub_iff_lt.mpr hlt,
          ← tsub_tsub_eq_add_tsub_of_le (Fin.val_fin_le.mpr hlt.le),
          Nat.sub_eq_iff_eq_add (by omega : j - i ≤ p.length),
          ← Nat.sub_eq_iff_eq_add' (Nat.pos_of_neZero p.length), hsub.ne', false_or,
          Fin.sub_val_of_le hlt.le, Nat.sub_eq_iff_eq_add' hlt.le] at hadj
        rw [hadj]
        exact p.adj_getVert_succ i.is_lt

def SimpleGraph.Walk.IsCycle.toCopy {v} {p : G.Walk v v} (h : p.IsCycle) : Copy (cycleGraph p.length) G where
  toHom := ⟨(p.getVert ·), h.adj_getVert_of_cycleGraph_adj⟩
  injective' i j heq :=
    Fin.ext <| h.getVert_injOn' (Nat.le_pred_of_lt i.is_lt) (Nat.le_pred_of_lt j.is_lt) heq

def SimpleGraph.ConnectedComponent.toCopy {c : G.ConnectedComponent} : Copy c.toSimpleGraph G where
  toHom := c.toSimpleGraph_hom
  injective' _ _ := by simp [toSimpleGraph_hom]

example [DecidableEq V] : G.IsBipartite ↔ ∀ n ≥ 2, Odd n → (cycleGraph n).Free G := by
  constructor
  · contrapose!
    rintro ⟨n, hn, h_odd, h_cycle⟩
    contrapose h_cycle with hc
    refine free_of_colorable ?_ hc
    have hχ := chromaticNumber_cycleGraph_of_odd n hn h_odd
    rw [show (3 : ℕ∞) = (2 : ℕ) + 1 by norm_cast,
      chromaticNumber_eq_iff_colorable_not_colorable] at hχ
    exact hχ.2
  · refine fun h ↦ colorable_iff_forall_connectedComponents.2 fun c ↦ ?_
    refine IsBipartite.of_eachCycleEven ?_ c.connected_toSimpleGraph
    contrapose! h
    obtain ⟨v, W, hW_cycle, hW_len⟩ := h
    refine ⟨W.length, ?_, ?_, ?_⟩
    · exact hW_cycle.three_le_length.trans' (by omega)
    · simp [Nat.odd_iff, Nat.mod_two_of_bodd, hW_len]
    · exact ⟨c.toCopy.comp hW_cycle.toCopy⟩

I just threw this together on top of @Jakub Nowak's proof of SimpleGraph.IsBipartite.of_eachCycleEven (live.lean-lang.org).

[Nick Adfor]

Jakub Nowak said:

I though that docs#Walk.bypass couldn't be useful for this theorem.

But in my file bypass finished some kind of proof:fear:

[Jakub Nowak]

My intention in the second part of the sentence you cited was to say, that I was wrong in thinking that. I've tried to use docs#Walk.bypass before, and I failed. But formulation of the lemma Even p.length ↔ Even p.bypass.length is I think quite clever use of it.

[Nick Adfor]

My version about the theorem eachCycleEven bipartite_iff_all_cycles_even. In this way, we have two different version now.

[Nick Adfor]

Ref #Is there code for X? > bipartite iff does not contain an odd cycle:
Jakub Nowak said:

Snir Broshi I will answer your question here.

Snir Broshi said:

I'm interested to learn how you managed to get an odd cycle from an odd walk, can you share the body of that function? This might enhance #31217

Here's the implementation: live.lean-lang.org
It's implemented by following the walk, until first repetition of a vertex. This gives either a cycle, or a A -> B -> A walk. If it's an odd cycle, then we get an odd cycle, otherwise it has even length, we can recurse on the walk with the repetition bypassed, and the length of the whole walk is still kept odd. At some point we must end up with odd length cycle, because .nil has even length.

If you try to apply similar algorithm to any closed walk, to get any cycle, the problem that arises is that we could always end up with A -> B -> A case. I think that the exact condition for when it is possible to extract cycle from closed walk isn't easy to formulate. E.g., you can't extract a cycle from such a walk: A -> B -> C -> B -> C -> D -> C -> E -> F -> E -> C -> B -> A. I think IsTrail is a good, simple condition. Odd length is another. Maybe another simple condition, weaker then IsTrail, is to require that the walk does not contain a back-and-forth A -> B -> A subwalk (this would require implementing similar recursive algorithm, the implementation from #31217 won't work).

[Nick Adfor]

Snir Broshi said:

So did you prove it? Is there a PR?

NowI have a PR. For more problem in PR, there's another post.
(5126) #PR reviews > #33257 Odd Cycle Theorem - Lean - Zulip

[Nick Adfor]

Mitchell Horner said:

When I wrote that todo I imagined a proof in terms of containment.

theorem SimpleGraph.Walk.IsCycle.adj_getVert_of_cycleGraph_adj
    {v} {p : G.Walk v v} (h : p.IsCycle)
    {i j : Fin (p.length)} (hadj : (cycleGraph p.length).Adj i j) :
    G.Adj (p.getVert i) (p.getVert j) := by
  rcases eq_zero_or_neZero p.length with heq | _
  · rw [heq] at i
    exact i.elim0
  · wlog hlt : i < j generalizing i j
    · rw [G.adj_comm]
      apply this hadj.symm
      exact lt_of_le_of_ne (le_of_not_gt hlt) hadj.symm.ne
    · by_cases hi : i = 0
      · simp_rw [hi, cycleGraph_adj', zero_sub, sub_zero, Fin.neg_def,
          Nat.mod_eq_of_lt (by omega : p.length - j < p.length), Nat.sub_eq_iff_eq_add j.is_lt.le,
          ← Nat.sub_eq_iff_eq_add' (by omega : 1 ≤ p.length), eq_comm] at hadj
        rcases hadj with hsnd | hpen
        · simp_rw [hi, Fin.val_zero, hsnd, Walk.getVert_zero]
          exact (p.adj_penultimate h.not_nil).symm
        · simp_rw [hi, Fin.val_zero, hpen]
          exact p.adj_getVert_succ (by omega : 0 < p.length)
      · have hsub : j - i < p.length - 1 := (Nat.le_pred_of_lt j.is_lt).trans' <|
            Nat.sub_lt_self (Nat.pos_of_ne_zero <| Fin.val_eq_zero_iff.ne.mpr hi) hlt.le
        simp_rw [cycleGraph_adj', Fin.coe_sub_iff_lt.mpr hlt,
          ← tsub_tsub_eq_add_tsub_of_le (Fin.val_fin_le.mpr hlt.le),
          Nat.sub_eq_iff_eq_add (by omega : j - i ≤ p.length),
          ← Nat.sub_eq_iff_eq_add' (Nat.pos_of_neZero p.length), hsub.ne', false_or,
          Fin.sub_val_of_le hlt.le, Nat.sub_eq_iff_eq_add' hlt.le] at hadj
        rw [hadj]
        exact p.adj_getVert_succ i.is_lt

def SimpleGraph.Walk.IsCycle.toCopy {v} {p : G.Walk v v} (h : p.IsCycle) : Copy (cycleGraph p.length) G where
  toHom := ⟨(p.getVert ·), h.adj_getVert_of_cycleGraph_adj⟩
  injective' i j heq :=
    Fin.ext <| h.getVert_injOn' (Nat.le_pred_of_lt i.is_lt) (Nat.le_pred_of_lt j.is_lt) heq

def SimpleGraph.ConnectedComponent.toCopy {c : G.ConnectedComponent} : Copy c.toSimpleGraph G where
  toHom := c.toSimpleGraph_hom
  injective' _ _ := by simp [toSimpleGraph_hom]

example [DecidableEq V] : G.IsBipartite ↔ ∀ n ≥ 2, Odd n → (cycleGraph n).Free G := by
  constructor
  · contrapose!
    rintro ⟨n, hn, h_odd, h_cycle⟩
    contrapose h_cycle with hc
    refine free_of_colorable ?_ hc
    have hχ := chromaticNumber_cycleGraph_of_odd n hn h_odd
    rw [show (3 : ℕ∞) = (2 : ℕ) + 1 by norm_cast,
      chromaticNumber_eq_iff_colorable_not_colorable] at hχ
    exact hχ.2
  · refine fun h ↦ colorable_iff_forall_connectedComponents.2 fun c ↦ ?_
    refine IsBipartite.of_eachCycleEven ?_ c.connected_toSimpleGraph
    contrapose! h
    obtain ⟨v, W, hW_cycle, hW_len⟩ := h
    refine ⟨W.length, ?_, ?_, ?_⟩
    · exact hW_cycle.three_le_length.trans' (by omega)
    · simp [Nat.odd_iff, Nat.mod_two_of_bodd, hW_len]
    · exact ⟨c.toCopy.comp hW_cycle.toCopy⟩

I just threw this together on top of Jakub Nowak's proof of SimpleGraph.IsBipartite.of_eachCycleEven (live.lean-lang.org).

Mitchell, I've used my origin way to prove your TODO in my #33257 (means that the theorem statement is yours but the proof is mine). I'm wondering if your proof here will be next branch of my PR or if I should add it in my PR (even repeatedly prove the same theorem statement).

[Jakub Nowak]

Mitchell Horner said:

When I wrote that todo I imagined a proof in terms of containment.

Why do you need the theorem in term of containments? One possible direction where someone could try to go further, would be to prove some things about matchings in bipartite graphs. It's hard to guess what form of this theorem would be easier to use, but the one in terms .IsCycle seems to me much more usable than the one in terms of containments.

[Mitchell Horner]

Jakub Nowak said:

Why do you need the theorem in term of containments?

For excluding cycles in forbidden subgraph problems.

Jakub Nowak said:

It's hard to guess what form of this theorem would be easier to use

Ah. Sorry. I don't want the theorem in terms of containment because I think it is a better representation. :sweat_smile: On the contrary. The forbidden subgraph problems are written in terms of containment and I'd like to iff a containment statement to its corresponding statement in terms of .IsCycle - I agree with you that they are much more usable.

Ideally, you have everything in terms of .IsCycle and then a handful of small lemmas/defs linking .IsCycle to cycleGraph and one small iff to convert the statement in discussion simply for convenience. (See this comment on a PR implementing some of these for pathGraph.)