-- Module: Mathlib.Combinatorics.Hall.Basic
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
mp mp₁ mp₂ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')),
    ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
mp₃ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections),
    ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
mp₄ :
  (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')) →
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) → (hu : u ∈ (hallMatchingsFunctor t).sections) → ι → α
mp₅ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections),
    Injective.{u + 1, v + 1} (β := α) fun (i : ι) ↦
      (↑(u (Opposite.op {i})) : ↥(Opposite.unop (Opposite.op {i})) → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {i})) x) i ⋯)
mp₆ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections) (x : ι),
    Membership.mem (α := α) (t x)
      ((↑(u (Opposite.op {x})) : ↥(Opposite.unop (Opposite.op {x})) → α)
          (Subtype.mk (p := fun (x_1 : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {x})) x_1) x ⋯) :
        α)
mp₇ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections),
    Injective.{u + 1, v + 1} (β := α) fun (i : ι) ↦
      (↑(u (Opposite.op {i})) : ↥(Opposite.unop (Opposite.op {i})) → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {i})) x) i ⋯)
mp₈ mp₉ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections) (x : ι),
    Membership.mem (α := α) (t x)
      ((↑(u (Opposite.op {x})) : ↥(Opposite.unop (Opposite.op {x})) → α)
          (Subtype.mk (p := fun (x_1 : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {x})) x_1) x ⋯) :
        α)
⊢ ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
classical
      haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
        intro ι'
        rw [hallMatchingsFunctor]
        infer_instance
      -- Apply the compactness argument
      obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
      refine ⟨?_, ?_, ?_⟩
      · -- Build the matching function from the section
        exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩
      · -- Show that it is injective
        intro i i'
        have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
        have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
        rw [← Finset.le_iff_subset] at subi subi'
        simp only
        rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
        let uii' := u (Opposite.op ({i, i'} : Finset ι))
        exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
      · -- Show that it maps each index to the corresponding finite set
        intro i
        apply (u (Opposite.op ({i} : Finset ι))).property.2

Premises used: Finset.le_iff_subset