[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
⊢ ↑(hallMatchingsOn t ι')
[PROOFSTEP]
refine' ⟨fun i => f.val ⟨i, h i.property⟩, _⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
⊢ (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) ∈ hallMatchingsOn t ι'
[PROOFSTEP]
cases' f.property with hinj hc
[GOAL]
case intro
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Function.Injective ↑f
hc : ∀ (x : { x // x ∈ ι'' }), ↑f x ∈ t ↑x
⊢ (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) ∈ hallMatchingsOn t ι'
[PROOFSTEP]
refine' ⟨_, fun i => hc ⟨i, h i.property⟩⟩
[GOAL]
case intro
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Function.Injective ↑f
hc : ∀ (x : { x // x ∈ ι'' }), ↑f x ∈ t ↑x
⊢ Function.Injective fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }
[PROOFSTEP]
rintro ⟨i, hi⟩ ⟨j, hj⟩ hh
[GOAL]
case intro.mk.mk
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Function.Injective ↑f
hc : ∀ (x : { x // x ∈ ι'' }), ↑f x ∈ t ↑x
i : ι
hi : i ∈ ι'
j : ι
hj : j ∈ ι'
hh :
  (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) { val := i, property := hi } =
    (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
[PROOFSTEP]
simpa only [Subtype.mk_eq_mk] using hinj hh
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ Nonempty ↑(hallMatchingsOn t ι')
[PROOFSTEP]
classical
refine' ⟨Classical.indefiniteDescription _ _⟩
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
intro s'
convert h (s'.image (↑)) using 1
simp only [card_image_of_injective s' Subtype.coe_injective]
rw [image_biUnion]
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ Nonempty ↑(hallMatchingsOn t ι')
[PROOFSTEP]
refine' ⟨Classical.indefiniteDescription _ _⟩
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ ∃ x, x ∈ hallMatchingsOn t ι'
[PROOFSTEP]
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ ∀ (s : Finset { x // x ∈ ι' }), card s ≤ card (Finset.biUnion s fun i => t ↑i)
[PROOFSTEP]
intro s'
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card s' ≤ card (Finset.biUnion s' fun i => t ↑i)
[PROOFSTEP]
convert h (s'.image (↑)) using 1
[GOAL]
case h.e'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card s' = card (image Subtype.val s')
case h.e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card (Finset.biUnion s' fun i => t ↑i) = card (Finset.biUnion (image Subtype.val s') t)
[PROOFSTEP]
simp only [card_image_of_injective s' Subtype.coe_injective]
[GOAL]
case h.e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card (Finset.biUnion s' fun i => t ↑i) = card (Finset.biUnion (image Subtype.val s') t)
[PROOFSTEP]
rw [image_biUnion]
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')
[PROOFSTEP]
classical
rw [hallMatchingsOn]
let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
  rintro f i
  refine' ⟨f.val i, _⟩
  rw [mem_biUnion]
  exact ⟨i, i.property, f.property.2 i⟩
apply Finite.of_injective g
intro f f' h
ext a
rw [Function.funext_iff] at h 
simpa using h a
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')
[PROOFSTEP]
rw [hallMatchingsOn]
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑{f | Function.Injective f ∧ ∀ (x : { x // x ∈ ι' }), f x ∈ t ↑x}
[PROOFSTEP]
let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
  rintro f i
  refine' ⟨f.val i, _⟩
  rw [mem_biUnion]
  exact ⟨i, i.property, f.property.2 i⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t }
[PROOFSTEP]
rintro f i
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : { x // x ∈ ι' }
⊢ { x // x ∈ Finset.biUnion ι' t }
[PROOFSTEP]
refine' ⟨f.val i, _⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : { x // x ∈ ι' }
⊢ ↑f i ∈ Finset.biUnion ι' t
[PROOFSTEP]
rw [mem_biUnion]
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : { x // x ∈ ι' }
⊢ ∃ a, a ∈ ι' ∧ ↑f i ∈ t a
[PROOFSTEP]
exact ⟨i, i.property, f.property.2 i⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
⊢ Finite ↑{f | Function.Injective f ∧ ∀ (x : { x // x ∈ ι' }), f x ∈ t ↑x}
[PROOFSTEP]
apply Finite.of_injective g
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
⊢ Function.Injective g
[PROOFSTEP]
intro f f' h
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
⊢ f = f'
[PROOFSTEP]
ext a
[GOAL]
case a.h
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
a : { x // x ∈ ι' }
⊢ ↑f a = ↑f' a
[PROOFSTEP]
rw [Function.funext_iff] at h 
[GOAL]
case a.h
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
f f' : ↑(hallMatchingsOn t ι')
h : ∀ (a : { x // x ∈ ι' }), g f a = g f' a
a : { x // x ∈ ι' }
⊢ ↑f a = ↑f' a
[PROOFSTEP]
simpa using h a
[GOAL]
ι : 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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro h
[GOAL]
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
[PROOFSTEP]
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
  hallMatchingsOn.nonempty t h ι'.unop
[GOAL]
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
[PROOFSTEP]
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 sectionexact fun i =>
    (u (Opposite.op ({ i } : Finset ι))).val ⟨i, by simp only [Opposite.unop_op, 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
[GOAL]
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
[PROOFSTEP]
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') :=
  by
  intro ι'
  rw [hallMatchingsFunctor]
  infer_instance
    -- Apply the compactness argument
[GOAL]
ι : 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 ι')
[PROOFSTEP]
intro ι'
[GOAL]
ι : 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 ι')
[PROOFSTEP]
rw [hallMatchingsFunctor]
[GOAL]
ι : 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
      ι')
[PROOFSTEP]
infer_instance
  -- Apply the compactness argument
[GOAL]
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
[PROOFSTEP]
obtain ⟨u, hu⟩ :=
  nonempty_sections_of_finite_inverse_system
    (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
⊢ ι → α
[PROOFSTEP]
exact fun i => (u (Opposite.op ({ i } : Finset ι))).val ⟨i, by simp only [Opposite.unop_op, mem_singleton]⟩
[GOAL]
ι : 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 ∈ Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ i ∈ (Opposite.op {i}).unop
[PROOFSTEP]
simp only [Opposite.unop_op, mem_singleton]
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
⊢ Function.Injective fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }
[PROOFSTEP]
intro i i'
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
have subi : ({ i } : Finset ι) ⊆ { i, i' } := by simp
[GOAL]
ι : 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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ {i} ⊆ {i, i'}
[PROOFSTEP]
simp
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
have subi' : ({ i' } : Finset ι) ⊆ { i, i' } := by simp
[GOAL]
ι : 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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ {i'} ⊆ {i, i'}
[PROOFSTEP]
simp
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
rw [← Finset.le_iff_subset] at subi subi' 
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
simp only
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) } =
      ↑(u (Opposite.op {i'})) { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
[PROOFSTEP]
rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑((hallMatchingsFunctor t).map (homOfLE subi).op (u (Opposite.op {i, i'}))) { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'})))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
[PROOFSTEP]
let uii' := u (Opposite.op ({ i, i' } : Finset ι))
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
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'}))) { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'})))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
[PROOFSTEP]
exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
⊢ ∀ (x : ι), ↑(u (Opposite.op {x})) { val := x, property := (_ : x ∈ {x}) } ∈ t x
[PROOFSTEP]
intro i
[GOAL]
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 ∈ Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) } ∈ t i
[PROOFSTEP]
apply (u (Opposite.op ({ i } : Finset ι))).property.2
[GOAL]
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)
[PROOFSTEP]
rintro ⟨f, hf₁, hf₂⟩ s
[GOAL]
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)
[PROOFSTEP]
rw [← Finset.card_image_of_injective s hf₁]
[GOAL]
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)
[PROOFSTEP]
apply Finset.card_le_of_subset
[GOAL]
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
[PROOFSTEP]
intro
[GOAL]
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
[PROOFSTEP]
rw [Finset.mem_image, Finset.mem_biUnion]
[GOAL]
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
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨x, hx, hf₂ x⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
⊢ Fintype ↑(Rel.image r ↑A)
[PROOFSTEP]
have h : Rel.image r A = (A.biUnion fun a => (Rel.image r { a }).toFinset : Set β) :=
  by
  ext
    -- Porting note: added `Set.mem_toFinset`
  simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
⊢ Rel.image r ↑A = ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
[PROOFSTEP]
ext
  -- Porting note: added `Set.mem_toFinset`
[GOAL]
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
x✝ : β
⊢ x✝ ∈ Rel.image r ↑A ↔ x✝ ∈ ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
[PROOFSTEP]
simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
h : Rel.image r ↑A = ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
⊢ Fintype ↑(Rel.image r ↑A)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
h : Rel.image r ↑A = ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
⊢ Fintype ↑↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
[PROOFSTEP]
apply FinsetCoe.fintype
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
let r' a := (Rel.image r { a }).toFinset
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h : ∀ A : Finset α, Fintype.card (Rel.image r A) = (A.biUnion r').card :=
  by
  intro A
  rw [← Set.toFinset_card]
  apply congr_arg
  ext b
  simp [Rel.image, (Set.mem_toFinset)]
    -- Porting note: added `Set.mem_toFinset`
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
⊢ ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
[PROOFSTEP]
intro A
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
⊢ card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
[PROOFSTEP]
rw [← Set.toFinset_card]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
⊢ Finset.card (Set.toFinset (Rel.image r ↑A)) = Finset.card (Finset.biUnion A r')
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
⊢ Set.toFinset (Rel.image r ↑A) = Finset.biUnion A r'
[PROOFSTEP]
ext b
[GOAL]
case h.a
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
b : β
⊢ b ∈ Set.toFinset (Rel.image r ↑A) ↔ b ∈ Finset.biUnion A r'
[PROOFSTEP]
simp [Rel.image, (Set.mem_toFinset)]
  -- Porting note: added `Set.mem_toFinset`
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
[PROOFSTEP]
simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
simp only [h, h']
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ Set.toFinset (Rel.image r {x})
[PROOFSTEP]
apply Finset.all_card_le_biUnion_card_iff_exists_injective
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
haveI := Classical.decEq β
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
let r' a := univ.filter fun b => r a b
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h : ∀ A : Finset α, (univ.filter fun b : β => ∃ a ∈ A, r a b) = A.biUnion r' :=
  by
  intro A
  ext b
  simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
[PROOFSTEP]
intro A
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
⊢ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
[PROOFSTEP]
ext b
[GOAL]
case a
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
b : β
⊢ b ∈ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ ↔ b ∈ Finset.biUnion A r'
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
simp_rw [h, h']
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (Finset.biUnion A fun a => filter (fun b => r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ filter (fun b => r x b) univ
[PROOFSTEP]
apply Finset.all_card_le_biUnion_card_iff_exists_injective
