-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
have have₁ have₂ :
  ∀
    (hrep :
      ConnectedComponent.Represents
        (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
        G.deleteUniversalVerts.coe.oddComponents),
    ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
have have₃ : ∀
  (hrep :
    ConnectedComponent.Represents
      (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
      G.deleteUniversalVerts.coe.oddComponents)
  (t : Set V) (ht : t ⊆ G.universalVerts) (M1 : G.Subgraph)
  (hM1 :
    M1.verts =
        Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
            Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
          t ∧
      M1.IsMatching),
  ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
Tactic: classical
  have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents
  -- First we match one node from each odd component to a universal vertex
  obtain ⟨t, ht, M1, hM1⟩ := Subgraph.IsMatching.exists_of_universalVerts
      (disjoint_image_val_universalVerts _).symm (by
        simp only [IsTutteViolator, not_lt] at h
        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq])
  -- Then we match all other nodes in components internally
  have exists_complMatch (K : G.deleteUniversalVerts.coe.ConnectedComponent) :
      ∃ M : Subgraph G, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching := by
    have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
      ((h' K).of_induce).subset Set.diff_subset
    rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]
    exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep
  choose complMatch hcomplMatch_compl hcomplMatch_match using exists_complMatch
  let M2 : Subgraph G := ⨆ K, complMatch K
  have hM2 : M2.IsMatching := by
    refine .iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)
    rw [(hcomplMatch_match i).support_eq_verts, hcomplMatch_compl i,
        (hcomplMatch_match j).support_eq_verts, hcomplMatch_compl j]
    exact Set.disjoint_of_subset Set.diff_subset Set.diff_subset <|
      Set.disjoint_image_of_injective Subtype.val_injective <|
        SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij
  have disjointM12 : Disjoint M1.support M2.support := by
    rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
      Set.disjoint_iUnion_right]
    exact fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right
  -- The only vertices left are indeed contained in universalVerts
  have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
    rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]
    intro v hv
    by_cases h : v ∈ M1.verts
    · exact M1.verts.mem_union_left _ h
    right
    simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
      hcomplMatch_compl]
    use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
    aesop
  exact ⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩