Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
⊢ ∃ M, M.IsPerfectMatching

Tactic:
classical
  -- If either matching does not contain their extra edge, we just use it as a perfect matching
  by_cases hM1xb : ¬M1.Adj x b
  · use G.toSubgraph M1.spanningCoe (M1.spanningCoe_sup_edge_le _ hM1xb)
    exact (Subgraph.IsPerfectMatching.toSubgraph_iff (M1.spanningCoe_sup_edge_le _ hM1xb)).mpr hM1
  by_cases hM2ac : ¬M2.Adj a c
  · use G.toSubgraph M2.spanningCoe (M2.spanningCoe_sup_edge_le _ hM2ac)
    exact (Subgraph.IsPerfectMatching.toSubgraph_iff (M2.spanningCoe_sup_edge_le _ hM2ac)).mpr hM2
  simp only [not_not] at hM1xb hM2ac
  -- Neither matching contains the edge that would make the other matching of G perfect
  have hM1nac : ¬M1.Adj a c := fun h ↦ by simpa [hnGac, edge_adj, hnac, hxa.ne, hnbc.symm, hab.ne]
    using h.adj_sub
  have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = (G ⊔ edge a c) ⊔ edge x b := by grind
  -- We state conditions for our cycle that hold in all cases and show that this suffices
  suffices ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧
      G'.Adj a c ∧ G' ≤ G ⊔ edge a c by
    obtain ⟨G', hG', hG'cyc, hG'xb, hnG'ac, hle⟩ := this
    have : M2.spanningCoe ∆ G' ≤ G := by
      apply Disjoint.left_le_of_le_sup_right (symmDiff_le (le_sup_of_le_right M2.spanningCoe_le)
        (le_sup_of_le_right hle))
      simp [disjoint_edge, symmDiff_def, hM2ac, hnG'ac]
    use (G.toSubgraph (symmDiff M2.spanningCoe G') this)
    apply hM2.symmDiff_of_isAlternating hG' hG'cyc
  -- We consider the symmetric difference of the two matchings
  let cycles := M1.spanningCoe ∆ M2.spanningCoe
  have hcalt : cycles.IsAlternating M2.spanningCoe := hM1.isAlternating_symmDiff_right hM2
  have hcycles := Subgraph.IsPerfectMatching.symmDiff_isCycles hM1 hM2
  have hcac : cycles.Adj a c := by simp [cycles, symmDiff_def, hM2ac, hM1nac]
  have hM1sub := Subgraph.spanningCoe_le M1
  have hM2sub := Subgraph.spanningCoe_le M2
  -- We consider the cycle that contains the vertex `c`
  have induce_le : ((cycles.connectedComponentMk c).toSimpleGraph).spanningCoe ≤
      (G ⊔ edge a c) ⊔ edge x b := by
    refine le_trans (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp) ?_
    simp only [← hsupG, cycles]
    exact le_trans (by apply symmDiff_le_sup) (sup_le_sup hM1sub hM2sub)
  -- If that cycle does not contain the vertex `x`, we use it as an alternating cycle
  by_cases! hxc : x ∉ (cycles.connectedComponentMk c).supp
  · use (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe
    refine ⟨hcalt.mono (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp), ?_⟩
    simp only [ConnectedComponent.adj_spanningCoe_toSimpleGraph, hxc, hcac, false_and,
      not_false_eq_true, ConnectedComponent.mem_supp_iff, ConnectedComponent.eq, and_true,
      true_and, hcac.reachable]
    refine ⟨hcycles.toSimpleGraph (cycles.connectedComponentMk c),
      Disjoint.left_le_of_le_sup_right induce_le ?_⟩
    rw [disjoint_edge]
    rw [ConnectedComponent.adj_spanningCoe_toSimpleGraph]
    simp_all
  have hacc := ((cycles.connectedComponentMk c).mem_supp_congr_adj hcac.symm).mp rfl
  have (G : SimpleGraph V) : LocallyFinite G := fun _ ↦ Fintype.ofFinite _
  have hnM2 (x' : V) (h : x' ≠ c) : ¬ M2.Adj x' a := by
    rw [M2.adj_comm]
    exact hM2.1.not_adj_left_of_ne h.symm hM2ac
  -- Else we construct a path that contain the edge `a c`, but not the edge `x b`
  obtain ⟨x', hx', p, hp, hpac, hnpxb⟩ :
      ∃ x' ∈ ({x, b} : Finset V), ∃ (p : cycles.Walk a x'), p.IsPath ∧
        p.toSubgraph.Adj a c ∧ ¬p.toSubgraph.Adj x b := by
    obtain ⟨p, hp⟩ := hcycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp hacc
      ⟨_, hcac⟩
    obtain ⟨p', hp'⟩ := hp.1.exists_isCycle_snd_verts_eq (by
      rwa [hp.1.adj_toSubgraph_iff_of_isCycles hcycles (hp.2 ▸ hacc)])
    obtain ⟨x', hx', hx'p, htw⟩ := Walk.exists_mem_support_forall_mem_support_imp_eq {x, b} <| by
      use x
      simp only [Finset.mem_filter, Finset.mem_insert, Finset.mem_singleton, true_or, true_and]
      rwa [← @Walk.mem_verts_toSubgraph, hp'.2.2, hp.2]
    refine ⟨x', hx', p'.takeUntil x' hx'p, hp'.1.isPath_takeUntil hx'p, ?_, fun h ↦ ?_⟩; swap
    · simp [htw _ (by simp) (Walk.mem_support_of_adj_toSubgraph h.symm),
        htw _ (by simp) (Walk.mem_support_of_adj_toSubgraph h)] at hnxb
    have : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd := by
      apply Walk.toSubgraph_adj_snd
      rw [Walk.nil_takeUntil]
      grind
    rwa [Walk.snd_takeUntil, hp'.2.1] at this
    simp only [Finset.mem_insert, Finset.mem_singleton] at hx'
    obtain rfl | rfl := hx'
    exacts [hxa.ne, hab.ne.symm]
  -- We show this path satisfies all requirements
  have hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c := by
    rw [← sdiff_edge _ (by simpa : ¬p.toSubgraph.spanningCoe.Adj x b), sdiff_le_iff']
    intro v w hvw
    apply hsupG ▸ sup_le_sup hM1sub hM2sub
    have := p.toSubgraph.spanningCoe_le hvw
    simp only [cycles, symmDiff_def] at this
    aesop
  -- Helper condition to show that `p` ends with an edge in `M2`
  have aux {x' : V} (hx' : x' ∈ ({x, b} : Set V)) (c' : V) (hc : c' ≠ a)
      (hadj : p.toSubgraph.Adj c' x') : M2.Adj c' x' := by
    refine (hadj.adj_sub.resolve_left fun hl ↦ hnpxb ?_).1
    obtain ⟨w, -, hw⟩ := hM1.1 (hM1.2 x')
    obtain rfl | rfl := hx'
    · rw [hw _ hM1xb, ← hw _ hl.1.symm]
      exact hadj.symm
    · rw [hw _ hM1xb.symm, ← hw _ hl.1.symm]
      exact hadj
  simp only [Finset.mem_insert, Finset.mem_singleton] at hx'
  obtain rfl | rfl := hx'
  · exact tutte_exists_isAlternating_isCycles p hp hcalt (hnM2 x' hnxc) hpac hnpxb hM2ac
      hxa hnxc hab.ne hle (aux (by simp))
  · conv =>
      enter [1, G', 2, 2, 1, 1]
      rw [adj_comm]
    rw [Subgraph.adj_comm] at hnpxb
    exact tutte_exists_isAlternating_isCycles p hp hcalt (hnM2 _ hnbc) hpac hnpxb hM2ac
      hab.symm hnbc hxa.ne.symm hle (aux (by simp))

Goal state after: