case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
constructor
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
intro h
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
  hallMatchingsOn.nonempty t h ι'.unop
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
  intro ι'
  rw [hallMatchingsFunctor]
  infer_instance
case mp.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)
case mp.intro.refine'_1
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ ι → α

case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ Function.Injective ?mp.intro.refine'_1

case mp.intro.refine'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ ∀ (x : ι), ?mp.intro.refine'_1 x ∈ t x
case mp.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
refine' ⟨_, _, _⟩
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite ((hallMatchingsFunctor t).obj ι')
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
intro ι'
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ((CategoryTheory.Functor.mk
          { obj := fun ι' => ↑(hallMatchingsOn t ι'.unop),
            map := fun {ι' ι''} g f => hallMatchingsOn.restrict t (_ : ι''.unop ≤ ι'.unop) f }).obj
      ι')
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite ((hallMatchingsFunctor t).obj ι')
rw [hallMatchingsFunctor]
no goals
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ((CategoryTheory.Functor.mk
          { obj := fun ι' => ↑(hallMatchingsOn t ι'.unop),
            map := fun {ι' ι''} g f => hallMatchingsOn.restrict t (_ : ι''.unop ≤ ι'.unop) f }).obj
      ι')
infer_instance
no goals
case mp.intro.refine'_1
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ ι → α
exact fun i =>
  (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [Opposite.unop_op, mem_singleton]⟩
no goals
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ i ∈ {i}.op.unop
simp only [Opposite.unop_op, mem_singleton]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ Function.Injective fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }
intro i i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
rw [← Finset.le_iff_subset] at subi subi'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) } = ↑(u {i'}.op) { val := i', property := (_ : i' ∈ {i'}) } → i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
simp only
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi).op (u {i, i'}.op))
        { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi').op (u {i, i'}.op))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) } = ↑(u {i'}.op) { val := i', property := (_ : i' ∈ {i'}) } → i = i'
rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
uii' : (hallMatchingsFunctor t).obj {i, i'}.op := u {i, i'}.op
⊢ ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi).op (u {i, i'}.op))
        { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi').op (u {i, i'}.op))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi).op (u {i, i'}.op))
        { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi').op (u {i, i'}.op))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
let uii' := u (Opposite.op ({i, i'} : Finset ι))
no goals
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
uii' : (hallMatchingsFunctor t).obj {i, i'}.op := u {i, i'}.op
⊢ ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi).op (u {i, i'}.op))
        { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (CategoryTheory.homOfLE subi').op (u {i, i'}.op))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
no goals
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ {i} ⊆ {i, i'}
simp
no goals
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ {i'} ⊆ {i, i'}
simp
case mp.intro.refine'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) } ∈ t i
case mp.intro.refine'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
⊢ ∀ (x : ι), ↑(u {x}.op) { val := x, property := (_ : x ∈ {x}) } ∈ t x
intro i
no goals
case mp.intro.refine'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ CategoryTheory.Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ ↑(u {i}.op) { val := i, property := (_ : i ∈ {i}) } ∈ t i
apply (u (Opposite.op ({i} : Finset ι))).property.2
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ card s ≤ card (Finset.biUnion s t)
case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
rintro ⟨f, hf₁, hf₂⟩ s
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ card (image f s) ≤ card (Finset.biUnion s t)
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ card s ≤ card (Finset.biUnion s t)
rw [← Finset.card_image_of_injective s hf₁]
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ image f s ⊆ Finset.biUnion s t
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ card (image f s) ≤ card (Finset.biUnion s t)
apply Finset.card_le_of_subset
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ a✝ ∈ image f s → a✝ ∈ Finset.biUnion s t
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ image f s ⊆ Finset.biUnion s t
intro
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ (∃ a, a ∈ s ∧ f a = a✝) → ∃ a, a ∈ s ∧ a✝ ∈ t a
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ a✝ ∈ image f s → a✝ ∈ Finset.biUnion s t
rw [Finset.mem_image, Finset.mem_biUnion]
case mpr.intro.intro.a.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a, a ∈ s ∧ f x ∈ t a
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ (∃ a, a ∈ s ∧ f a = a✝) → ∃ a, a ∈ s ∧ a✝ ∈ t a
rintro ⟨x, hx, rfl⟩
no goals
case mpr.intro.intro.a.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a, a ∈ s ∧ f x ∈ t a
exact ⟨x, hx, hf₂ x⟩