-- 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 : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)), ∃ (M : G.Subgraph), M.IsPerfectMatching
h :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₃ :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V))
    (this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₄ :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V))
    (this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ),
    ∀ v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).Adj v w
h₅ :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V))
    (this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ),
    ∀ v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      ∃! w : V,
        if h : v ∈ p₁ then (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w
        else ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
h₆ :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V))
    (this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ),
    ∀ v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      ∀ (h : v ∈ p₁), ∃! w : V, (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w
h₇ h₈ :
  ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
    (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V))
    (this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ),
    ∀ v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      v ∉ p₁ → ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩

Premises used: SimpleGraph.exists_bijective_of_forall_ncard_le, dite_else_false, existsUnique_eq'