/-
This file was edited by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: 68d2a312-39a3-4cdb-b694-9410cb2ea928

The following was proved by Aristotle:

- lemma even_length_iff_even_bypass_length [DecidableEq V]
    (h_cycles : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length)
    {u v : V} (p : G.Walk u v) :
    Even p.length ↔ Even p.bypass.length
-/

import Mathlib


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

open SimpleGraph

/- Aristotle failed to load this code into its environment. Double check that the syntax is correct.

Unknown constant `SimpleGraph.Walk.isTrail_cons`-/
lemma even_cycle_length_of_path
    (h_cycles : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length)
    {u v : V} (q : G.Walk v u) (hq : q.IsPath) (ha : G.Adj u v) :
    Even (SimpleGraph.Walk.cons ha q).length := by
      by_cases hq' : q.length = 1 <;>
      simp_all +decide only [Walk.length_cons]
      have h_cycle : SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.cons ha q) := by
        simp_all only [Walk.isCycle_def, ne_eq, and_imp, Walk.isTrail_cons, reduceCtorEq,
          not_false_eq_true, Walk.support_cons, List.tail_cons, true_and]
        apply And.intro
        · sorry
        · sorry
      have := h_cycles u (SimpleGraph.Walk.cons ha q) h_cycle
      simp_all +decide [parity_simps]

noncomputable section AristotleLemmas

/-
If a path between `u` and `v` contains the edge `{u, v}`, then the path has length 1.
-/
lemma IsPath.length_eq_one_of_mem_edges {u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : s(u, v) ∈ p.edges) : p.length = 1 := by
  -- If `p` is a path from `u` to `v` and `p.edges` contains `s(u, v)`, then any cycle in `p` must include the edge `s(u, v)`. This would make `p` a non-simple cycle, contradicting `hp`.
  by_contra h_non_simple_cycle;
  -- If `p` contains an edge `s(u, v)`, then any cycle in `p` must include the edge `s(u, v)`. This would make `p` a non-simple cycle, contradicting `hp`.
  have h_cycle : ∃ q : G.Walk u u, q.IsCycle := by
    rcases p with ( _ | ⟨ _, _, p ⟩ ) <;> aesop;
    have := SimpleGraph.Walk.fst_mem_support_of_mem_edges p h_3; aesop;
  obtain ⟨ q, hq ⟩ := h_cycle;
  cases q <;> simp_all +decide [ SimpleGraph.Walk.isCycle_def ];
  cases p <;> simp_all +decide [ SimpleGraph.Walk.isTrail_def ];
  aesop;
  exact right_1 ( SimpleGraph.Walk.fst_mem_support_of_mem_edges _ h_4 )

/-
If `q` is a path from `v` to `w` containing `u`, and `ha` is an edge between `u` and `v`, then the walk formed by `ha` followed by the part of `q` up to `u` has even length.
-/
lemma even_length_cons_takeUntil_of_bypass
    {u v w : V} (q : G.Walk v w) (hq : q.IsPath) (ha : G.Adj u v) (hs : u ∈ q.support)
    (h_cycles : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length) :
    Even (SimpleGraph.Walk.cons ha (q.takeUntil u hs)).length := by
  by_cases hc : SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.cons ha (q.takeUntil u hs));
  · exact h_cycles _ _ hc;
  · -- If `c` is not a cycle, then `s(u, v) ∈ p.edges`.
    have h_edge : s(u, v) ∈ (q.takeUntil u hs).edges := by
      contrapose! hc; simp_all +decide [ SimpleGraph.Walk.cons_isCycle_iff ] ;
      exact?;
    have h_length : (q.takeUntil u hs).length = 1 := by
      apply IsPath.length_eq_one_of_mem_edges;
      · exact hq.takeUntil _;
      · rwa [ Sym2.eq_swap ];
    aesop

end AristotleLemmas

lemma even_length_iff_even_bypass_length [DecidableEq V]
    (h_cycles : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length)
    {u v : V} (p : G.Walk u v) :
    Even p.length ↔ Even p.bypass.length := by
  induction p with
  | nil =>
    simp_all only [Walk.length_nil, Even.zero, true_iff]
    exact even_iff_two_dvd.mpr ⟨0, rfl⟩
  | cons h p ih =>
    simp +decide [ SimpleGraph.Walk.bypass ];
    split_ifs <;> simp_all +decide [ parity_simps ];
    have h_even : Even (SimpleGraph.Walk.cons h (p.bypass.takeUntil _ ‹_›)).length := by
      apply even_length_cons_takeUntil_of_bypass;
      · exact?;
      · assumption;
    simp_all +decide [ SimpleGraph.Walk.length_cons, parity_simps ];
    have h_even : Even (SimpleGraph.Walk.length p.bypass) ↔ Even (SimpleGraph.Walk.length (p.bypass.takeUntil _ ‹_›) + SimpleGraph.Walk.length (p.bypass.dropUntil _ ‹_›)) := by
      rw [ ← SimpleGraph.Walk.length_append, SimpleGraph.Walk.take_spec ];
    grind