-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
pos : ∀ (hvw : v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg neg₁ : ∀ (hvw : ¬v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₂ : ∀ (hvw : ¬v = w) (hpn : ¬p.Nil), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₃ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w'), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₄ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w') (hnpvw' : ¬p.toSubgraph.Adj v w'),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
pos₁ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : w = w'),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₅ neg₆ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : ¬w = w'),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₇ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : ¬w = w')
    (hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₈ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : ¬w = w')
    (hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe) (hp'p : (Walk.cons ⋯ p).IsPath),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₉ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w')
    (hw'1 : p.snd ≠ w') (hw'2 : G.Adj v w') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : ¬w = w')
    (hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe) (hp'p : (Walk.cons ⋯ p).IsPath)
    (this : (G \ p.toSubgraph.spanningCoe).Adj w' v), (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
classical
  -- Consider the case when p is nil
  by_cases hvw : v = w
  · subst hvw
    use .nil
  have hpn : ¬p.Nil := Walk.not_nil_of_ne hvw
  obtain ⟨w', ⟨hw'1, hw'2⟩, hwu⟩ := hcyc.existsUnique_ne_adj
    (p.toSubgraph_adj_snd hpn).adj_sub
  -- The edge (v, w) can't be in p, because then it would be the second node
  have hnpvw' : ¬ p.toSubgraph.Adj v w' := by
    intro h
    exact hw'1 (hp.snd_of_toSubgraph_adj h)
  -- If w = w', then the reachability can be proved with just one edge
  by_cases hww' : w = w'
  · subst hww'
    have : (G \ p.toSubgraph.spanningCoe).Adj w v := by
      simp only [sdiff_adj, Subgraph.spanningCoe_adj]
      exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩
    exact this.reachable
  -- Construct the walk needed recursively by extending p
  have hle : (G \ (p.cons hw'2.symm).toSubgraph.spanningCoe) ≤ (G \ p.toSubgraph.spanningCoe) := by
    apply sdiff_le_sdiff (by rfl) ?hcd
    simp
  have hp'p : (p.cons hw'2.symm).IsPath := by
    rw [Walk.cons_isPath_iff]
    refine ⟨hp, fun hw' ↦ ?_⟩
    exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)
  have : (G \ p.toSubgraph.spanningCoe).Adj w' v := by
    simp only [sdiff_adj, Subgraph.spanningCoe_adj]
    refine ⟨hw'2.symm, fun h ↦ ?_⟩
    exact hnpvw' h.symm
  use (((hcyc.reachable_sdiff_toSubgraph_spanningCoe_aux
    (p.cons hw'2.symm) hp'p).some).mapLe hle).append this.toWalk