-- Mathlib/Combinatorics/Hall/Basic.lean
theorem Finset.all_card_le_biUnion_card_iff_exists_injective {ι : Type u} {α : Type v}
    [DecidableEq α] (t : ι → Finset α) :
    (∀ s : Finset ι, #s ≤ #(s.biUnion t)) ↔
      ∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x

Proof state:
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)

Result:
case mp.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
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

Proof state:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i : ι
⊢ i ∈ Opposite.unop (Opposite.op {i})

Tactic:
simp only [Opposite.unop_op, mem_singleton]

Result:
no goals

Proof state:
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ (∃ a ∈ s, f a = a✝) → ∃ a ∈ s, a✝ ∈ t a

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case mpr.intro.intro.a.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a ∈ s, f x ∈ t a

Proof state:
case mp.intro.refine_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i : ι
⊢ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩ ∈ t i

Tactic:
apply (u (Opposite.op ({i} : Finset ι))).property.2

Result:
no goals

Proof state:
case mp.intro.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
⊢ (fun i => ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i = (fun i => ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i' → i = i'

Tactic:
have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp

Result:
case mp.intro.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i = (fun i => ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i' → i = i'

Proof state:
case mpr.intro.intro.a.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a ∈ s, f x ∈ t a

Tactic:
exact ⟨x, hx, hf₂ x⟩

Result:
no goals

Proof state:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ({ obj := fun ι' => ↑(hallMatchingsOn t (Opposite.unop ι')),
          map := fun {x x_1} g f => hallMatchingsOn.restrict t ⋯ f, map_id := ⋯, map_comp := ⋯ }.obj
      ι')

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #(image f s) ≤ #(s.biUnion t)

Tactic:
apply Finset.card_le_card

Result:
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ image f s ⊆ s.biUnion t

Proof state:
case mp.intro.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑((hallMatchingsFunctor t).map (homOfLE subi).op (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'}))) ⟨i', ⋯⟩ →
    i = i'

Tactic:
let uii' := u (Opposite.op ({i, i'} : Finset ι))

Result:
case mp.intro.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
uii' : (hallMatchingsFunctor t).obj (Opposite.op {i, i'}) := u (Opposite.op {i, i'})
⊢ ↑((hallMatchingsFunctor t).map (homOfLE subi).op (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'}))) ⟨i', ⋯⟩ →
    i = i'

Proof state:
case mp.intro.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
uii' : (hallMatchingsFunctor t).obj (Opposite.op {i, i'}) := u (Opposite.op {i, i'})
⊢ ↑((hallMatchingsFunctor t).map (homOfLE subi).op (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'}))) ⟨i', ⋯⟩ →
    i = i'

Tactic:
exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)

Result:
no goals

Proof state:
case mp.intro.refine_1
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ ι → α

Tactic:
exact fun i =>
  (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [Opposite.unop_op, mem_singleton]⟩

Result:
no goals