-- 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 :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x),
    ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
obtain₁ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁),
    ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
obtain₂ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂),
    ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
obtain₃ obtain₄ obtain₅ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
refine_1 :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    Injective f'
refine_2 :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    let g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) := fun (x : (↑p₂ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯;
    Injective g'
refine_3 :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    ∀ (a : (↑p₁ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) a (f' a)
refine_4 :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    let g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) := fun (x : (↑p₂ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯;
    ∀ (b : (↑p₂ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) (g' b) b
refine_2₁ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    let g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) := fun (x : (↑p₂ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯;
    Injective g'
refine_3₁ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    ∀ (a : (↑p₁ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) a (f' a)
refine_4₁ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    let g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) := fun (x : (↑p₂ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯;
    ∀ (b : (↑p₂ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) (g' b) b
refine_3₂ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    ∀ (a : (↑p₁ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) a (f' a)
refine_4₂ refine_4₃ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
    let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯;
    let g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) := fun (x : (↑p₂ : Type u_1)) ↦
      Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯;
    ∀ (b : (↑p₂ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) (g' b) b
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)

Tactic:
classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : V) (h : x ∈ p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) (h : x ∈ p₂) : f x ∉ p₂ := h₁.disjoint |>.notMem_of_mem_left <|
    isBipartiteWith_neighborSet_subset h₁.symm h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm

Premises used: Function.Injective.of_comp