-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
    ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
obtain₁ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁), ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
h :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁),
    p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯) ∧
      Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this ⋯)
h₃ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
    (hv : v ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯)),
    ∃! w : V, Subgraph.Adj (G := G) (hall_subgraph (p := p₁) f this ⋯) v w
h₄ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
    (hv : v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v),
    ∃! w : V,
      if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
      else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
h₅ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V) (h' : v ∈ p₁),
    ∃! w : V,
      if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
      else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
h₆ h₇ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v x : V) (hx₁ : x ∈ p₁)
    (hx₂ : f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) x hx₁) = v),
    ∃! w : V,
      if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
      else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching

Tactic:
classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)

Premises used: Set.mem_union, Set.mem_range, dite_else_false, Subtype.exists, forall_exists_index, reduceDIte, true_and