[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
α : Type u
inst✝ : SemilatticeSup α
X Y : α
f g : X ⟶ Y
⊢ f ≫ 𝟙 Y = g ≫ 𝟙 Y
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
α : Type u
inst✝ : SemilatticeSup α
X Y : α
f g : X ⟶ Y
⊢ (f ≫ 𝟙 Y).down = (g ≫ 𝟙 Y).down
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x x_1 => x ≤ x_1
X Y : α
f g : X ⟶ Y
⊢ f ≫ 𝟙 Y = g ≫ 𝟙 Y
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x x_1 => x ≤ x_1
X Y : α
f g : X ⟶ Y
⊢ (f ≫ 𝟙 Y).down = (g ≫ 𝟙 Y).down
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ IsFiltered α
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
⊢ IsFiltered α
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
⊢ X.as = { as := PUnit.unit }.as
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
f g : X ⟶ Y
⊢ Y.as = { as := PUnit.unit }.as
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
f g : X ⟶ Y
⊢ f ≫ { down := { down := (_ : Y.as = Y.as) } } = g ≫ { down := { down := (_ : Y.as = Y.as) } }
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
f g : X ⟶ Y
⊢ (f ≫ { down := { down := (_ : Y.as = Y.as) } }).down = (g ≫ { down := { down := (_ : Y.as = Y.as) } }).down
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ f ≫
      ↑(Adjunction.homEquiv h Y (coeq (?m.10843 h X Y f g) (?m.10844 h X Y f g)))
        (coeqHom (?m.10843 h X Y f g) (?m.10844 h X Y f g)) =
    g ≫
      ↑(Adjunction.homEquiv h Y (coeq (?m.10843 h X Y f g) (?m.10844 h X Y f g)))
        (coeqHom (?m.10843 h X Y f g) (?m.10844 h X Y f g))
[PROOFSTEP]
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → _root_.Nonempty (X ⟶ S)
[PROOFSTEP]
classical
induction' O using Finset.induction with X O' nm h
· exact ⟨Classical.choice IsFiltered.Nonempty, by intro; simp⟩
· obtain ⟨S', w'⟩ := h
  use max X S'
  rintro Y mY
  obtain rfl | h := eq_or_ne Y X
  · exact ⟨leftToMax _ _⟩
  · exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → _root_.Nonempty (X ⟶ S)
[PROOFSTEP]
induction' O using Finset.induction with X O' nm h
[GOAL]
case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (X ⟶ S)
[PROOFSTEP]
exact ⟨Classical.choice IsFiltered.Nonempty, by intro; simp⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
⊢ ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (X ⟶ Classical.choice (_ : _root_.Nonempty C))
[PROOFSTEP]
intro
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X✝ : C
⊢ X✝ ∈ ∅ → _root_.Nonempty (X✝ ⟶ Classical.choice (_ : _root_.Nonempty C))
[PROOFSTEP]
simp
[GOAL]
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → _root_.Nonempty (X ⟶ S)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (X_1 ⟶ S)
[PROOFSTEP]
obtain ⟨S', w'⟩ := h
[GOAL]
case insert.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (X ⟶ S')
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (X_1 ⟶ S)
[PROOFSTEP]
use max X S'
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (X ⟶ S')
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (X_1 ⟶ max X S')
[PROOFSTEP]
rintro Y mY
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (X ⟶ S')
Y : C
mY : Y ∈ insert X O'
⊢ _root_.Nonempty (Y ⟶ max X S')
[PROOFSTEP]
obtain rfl | h := eq_or_ne Y X
[GOAL]
case h.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (X ⟶ S')
Y : C
nm : ¬Y ∈ O'
mY : Y ∈ insert Y O'
⊢ _root_.Nonempty (Y ⟶ max Y S')
[PROOFSTEP]
exact ⟨leftToMax _ _⟩
[GOAL]
case h.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (X ⟶ S')
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ _root_.Nonempty (Y ⟶ max X S')
[PROOFSTEP]
exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H → f ≫ T mY = T mX
[PROOFSTEP]
classical
induction' H using Finset.induction with h' H' nmf h''
· obtain ⟨S, f⟩ := sup_objs_exists O
  refine' ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
· obtain ⟨X, Y, mX, mY, f⟩ := h'
  obtain ⟨S', T', w'⟩ := h''
  refine' ⟨coeq (f ≫ T' mY) (T' mX), fun mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX), _⟩
  intro X' Y' mX' mY' f' mf'
  rw [← Category.assoc]
  by_cases h : X = X' ∧ Y = Y'
  · rcases h with ⟨rfl, rfl⟩
    by_cases hf : f = f'
    · subst hf
      apply coeq_condition
    · rw [@w' _ _ mX mY f']
      simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'
      rcases mf' with mf' | mf'
      · exfalso
        exact hf mf'.symm
      · exact mf'
  · rw [@w' _ _ mX' mY' f' _]
    apply Finset.mem_of_mem_insert_of_ne mf'
    contrapose! h
    obtain ⟨rfl, h⟩ := h
    trivial
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H → f ≫ T mY = T mX
[PROOFSTEP]
induction' H using Finset.induction with h' H' nmf h''
[GOAL]
case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ ∅ → f ≫ T mY = T mX
[PROOFSTEP]
obtain ⟨S, f⟩ := sup_objs_exists O
[GOAL]
case empty.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → _root_.Nonempty (X ⟶ S)
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ ∅ → f ≫ T mY = T mX
[PROOFSTEP]
refine' ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → _root_.Nonempty (X ⟶ S)
⊢ ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ ∅ →
      f_1 ≫ (fun {X} mX => Nonempty.some (_ : _root_.Nonempty (X ⟶ S))) mY =
        (fun {X} mX => Nonempty.some (_ : _root_.Nonempty (X ⟶ S))) mX
[PROOFSTEP]
rintro - - - - - ⟨⟩
[GOAL]
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : ¬h' ∈ H'
h'' :
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T mY = T mX
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ insert h' H' →
        f ≫ T mY = T mX
[PROOFSTEP]
obtain ⟨X, Y, mX, mY, f⟩ := h'
[GOAL]
case insert.mk.mk.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h'' :
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T mY = T mX
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      { fst := X_1, snd := { fst := Y_1, snd := { fst := mX_1, snd := { fst := mY_1, snd := f_1 } } } } ∈
          insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H' →
        f_1 ≫ T mY_1 = T mX_1
[PROOFSTEP]
obtain ⟨S', T', w'⟩ := h''
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      { fst := X_1, snd := { fst := Y_1, snd := { fst := mX_1, snd := { fst := mY_1, snd := f_1 } } } } ∈
          insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H' →
        f_1 ≫ T mY_1 = T mX_1
[PROOFSTEP]
refine' ⟨coeq (f ≫ T' mY) (T' mX), fun mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX), _⟩
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
⊢ ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
    { fst := X_1, snd := { fst := Y_1, snd := { fst := mX_1, snd := { fst := mY_1, snd := f_1 } } } } ∈
        insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H' →
      f_1 ≫ (fun {X_2} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY_1 =
        (fun {X_2} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX_1
[PROOFSTEP]
intro X' Y' mX' mY' f' mf'
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ f' ≫ (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY' =
    (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
by_cases h : X = X' ∧ Y = Y'
[GOAL]
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : X = X' ∧ Y = Y'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
rcases h with ⟨rfl, rfl⟩
[GOAL]
case pos.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
by_cases hf : f = f'
[GOAL]
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
hf : f = f'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
subst hf
[GOAL]
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ (f ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
apply coeq_condition
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
hf : ¬f = f'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
rw [@w' _ _ mX mY f']
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
hf : ¬f = f'
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : f' = f ∨ { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈ H'
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
rcases mf' with mf' | mf'
[GOAL]
case neg.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : f' = f
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
exfalso
[GOAL]
case neg.inl.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : f' = f
⊢ False
[PROOFSTEP]
exact hf mf'.symm
[GOAL]
case neg.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈ H'
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
exact mf'
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : ¬(X = X' ∧ Y = Y')
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
[PROOFSTEP]
rw [@w' _ _ mX' mY' f' _]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : ¬(X = X' ∧ Y = Y')
⊢ { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈ H'
[PROOFSTEP]
apply Finset.mem_of_mem_insert_of_ne mf'
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : ¬(X = X' ∧ Y = Y')
⊢ { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ≠
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } }
[PROOFSTEP]
contrapose! h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } =
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } }
⊢ X = X' ∧ Y = Y'
[PROOFSTEP]
obtain ⟨rfl, h⟩ := h
[GOAL]
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → f ≫ T' mY = T' mX
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ X = X ∧ Y = Y
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ _root_.Nonempty (Cocone F)
[PROOFSTEP]
classical
let O := Finset.univ.image F.obj
let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
  Finset.univ.biUnion fun X : J =>
    Finset.univ.biUnion fun Y : J => Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp, by simp, F.map f⟩
obtain ⟨Z, f, w⟩ := sup_exists O H
refine' ⟨⟨Z, ⟨fun X => f (by simp), _⟩⟩⟩
intro j j' g
dsimp
simp only [Category.comp_id]
apply w
simp only [Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq, true_and, exists_and_left]
exact ⟨j, rfl, j', g, by simp⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ _root_.Nonempty (Cocone F)
[PROOFSTEP]
let O := Finset.univ.image F.obj
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
⊢ _root_.Nonempty (Cocone F)
[PROOFSTEP]
let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
  Finset.univ.biUnion fun X : J =>
    Finset.univ.biUnion fun Y : J => Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp, by simp, F.map f⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
X Y : J
f : X ⟶ Y
⊢ F.obj X ∈ O
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
X Y : J
f : X ⟶ Y
⊢ F.obj Y ∈ O
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
⊢ _root_.Nonempty (Cocone F)
[PROOFSTEP]
obtain ⟨Z, f, w⟩ := sup_exists O H
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
⊢ _root_.Nonempty (Cocone F)
[PROOFSTEP]
refine' ⟨⟨Z, ⟨fun X => f (by simp), _⟩⟩⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
X : J
⊢ F.obj X ∈ O
[PROOFSTEP]
simp
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y),
    F.map f_1 ≫ (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) Y =
      (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) X ≫ ((Functor.const J).obj Z).map f_1
[PROOFSTEP]
intro j j' g
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) j' =
    (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) j ≫ ((Functor.const J).obj Z).map g
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) = f (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ≫ 𝟙 Z
[PROOFSTEP]
simp only [Category.comp_id]
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) = f (_ : F.obj j ∈ Finset.image F.obj Finset.univ)
[PROOFSTEP]
apply w
[GOAL]
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ { fst := F.obj j,
      snd :=
        { fst := F.obj j',
          snd :=
            { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
              snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } } } ∈
    H
[PROOFSTEP]
simp only [Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq, true_and, exists_and_left]
[GOAL]
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ ∃ a,
    F.obj a = F.obj j ∧
      ∃ x x_1,
        HEq
          { fst := F.obj x,
            snd :=
              { fst := (_ : F.obj a ∈ Finset.image F.obj Finset.univ),
                snd := { fst := (_ : F.obj x ∈ Finset.image F.obj Finset.univ), snd := F.map x_1 } } }
          { fst := F.obj j',
            snd :=
              { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
                snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } }
[PROOFSTEP]
exact ⟨j, rfl, j', g, by simp⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type v
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ HEq
    { fst := F.obj j',
      snd :=
        { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
          snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } }
    { fst := F.obj j',
      snd :=
        { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
          snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ f ≫ coeq₃Hom f g h = g ≫ coeq₃Hom f g h
[PROOFSTEP]
simp only [coeq₃Hom, ← Category.assoc, coeq_condition f g]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ g ≫ coeq₃Hom f g h = h ≫ coeq₃Hom f g h
[PROOFSTEP]
dsimp [coeq₃Hom]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ g ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
slice_lhs 2 4 => rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
case a C : Type u inst✝¹ : Category.{v, u} C inst✝ : IsFilteredOrEmpty C j₁ j₂ : C f g h : j₁ ⟶ j₂ | g
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
case a C : Type u inst✝¹ : Category.{v, u} C inst✝ : IsFilteredOrEmpty C j₁ j₂ : C f g h : j₁ ⟶ j₂ | g
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
case a C : Type u inst✝¹ : Category.{v, u} C inst✝ : IsFilteredOrEmpty C j₁ j₂ : C f g h : j₁ ⟶ j₂ | g
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
slice_rhs 2 4 => rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
case a C : Type u inst✝¹ : Category.{v, u} C inst✝ : IsFilteredOrEmpty C j₁ j₂ : C f g h : j₁ ⟶ j₂ | h
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
case a C : Type u inst✝¹ : Category.{v, u} C inst✝ : IsFilteredOrEmpty C j₁ j₂ : C f g h : j₁ ⟶ j₂ | h
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
case a C : Type u inst✝¹ : Category.{v, u} C inst✝ : IsFilteredOrEmpty C j₁ j₂ : C f g h : j₁ ⟶ j₂ | h
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
slice_lhs 1 3 => rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| g ≫ coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| g ≫ coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| g ≫ coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
rw [← Category.assoc, coeq_condition _ _]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ ((h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
i j j' : C
f : i ⟶ j
f' : i ⟶ j'
K : C
G : j ⟶ K
G' : j' ⟶ K
h✝ : True
k : C
e : K ⟶ k
he : (f ≫ G) ≫ e = (f' ≫ G') ≫ e
⊢ f ≫ G ≫ e = f' ≫ G' ≫ e
[PROOFSTEP]
simpa only [← Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
[PROOFSTEP]
obtain ⟨t, k₁t, k₂t, ht⟩ := span f₁ g₁
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
[PROOFSTEP]
obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
[PROOFSTEP]
simp_rw [Category.assoc] at hs
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
[PROOFSTEP]
exact ⟨s, k₁t ≫ ts, k₂t ≫ ts, by simp only [← Category.assoc, ht], hs⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ f₁ ≫ k₁t ≫ ts = g₁ ≫ k₂t ≫ ts
[PROOFSTEP]
simp only [← Category.assoc, ht]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
[PROOFSTEP]
obtain ⟨l', k₁l, k₂l, hl⟩ := span f₂ f₃
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
[PROOFSTEP]
obtain ⟨s, ls, l's, hs₁, hs₂⟩ := bowtie g₁ (f₁ ≫ k₁l) g₂ (f₄ ≫ k₂l)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
[PROOFSTEP]
refine' ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, _, by simp only [← Category.assoc, hl], _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₂ ≫ k₁l ≫ l's = f₃ ≫ k₂l ≫ l's
[PROOFSTEP]
simp only [← Category.assoc, hl]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₁ ≫ k₁l ≫ l's = g₁ ≫ ls
[PROOFSTEP]
simp only [hs₁, hs₂, Category.assoc]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₄ ≫ k₂l ≫ l's = g₂ ≫ ls
[PROOFSTEP]
simp only [hs₁, hs₂, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
α : Type u
inst✝ : SemilatticeInf α
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
α : Type u
inst✝ : SemilatticeInf α
X Y : α
f g : X ⟶ Y
⊢ (𝟙 X ≫ f).down = (𝟙 X ≫ g).down
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x x_1 => x ≥ x_1
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x x_1 => x ≥ x_1
X Y : α
f g : X ⟶ Y
⊢ (𝟙 X ≫ f).down = (𝟙 X ≫ g).down
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
⊢ IsCofiltered α
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ IsCofiltered α
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
⊢ { as := PUnit.unit }.as = X.as
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
f g : X ⟶ Y
⊢ { as := PUnit.unit }.as = X.as
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
f g : X ⟶ Y
⊢ { down := { down := (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as) } } ≫ f =
    { down := { down := (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as) } } ≫ g
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit
f g : X ⟶ Y
⊢ ({ down := { down := (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as) } } ≫ f).down =
    ({ down := { down := (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as) } } ≫ g).down
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
i j j' : C
f : j ⟶ i
f' : j' ⟶ i
K : C
G : K ⟶ j
G' : K ⟶ j'
h✝ : True
k : C
e : k ⟶ K
he : e ≫ G ≫ f = e ≫ G' ≫ f'
⊢ (e ≫ G) ≫ f = (e ≫ G') ≫ f'
[PROOFSTEP]
simpa only [Category.assoc] using he
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) { fst := i, snd := ij })
        ((fun f => Set.range (F.map f.snd)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) { fst := k, snd := kj })
        ((fun f => Set.range (F.map f.snd)) z)
[PROOFSTEP]
let ⟨l, li, lk, e⟩ := cospan ij kj
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) { fst := i, snd := ij })
        ((fun f => Set.range (F.map f.snd)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) { fst := k, snd := kj })
        ((fun f => Set.range (F.map f.snd)) z)
[PROOFSTEP]
refine' ⟨⟨l, lk ≫ kj⟩, e ▸ _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) { fst := i, snd := ij })
    ((fun f => Set.range (F.map f.snd)) { fst := l, snd := li ≫ ij })
[PROOFSTEP]
simp_rw [F.map_comp]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) { fst := k, snd := kj })
    ((fun f => Set.range (F.map f.snd)) { fst := l, snd := lk ≫ kj })
[PROOFSTEP]
simp_rw [F.map_comp]
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range (F.map ij) ⊇ Set.range (F.map li ≫ F.map ij)
[PROOFSTEP]
apply Set.range_comp_subset_range
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range (F.map kj) ⊇ Set.range (F.map lk ≫ F.map kj)
[PROOFSTEP]
apply Set.range_comp_subset_range
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ ↑(Adjunction.homEquiv h (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ f =
    ↑(Adjunction.homEquiv h (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ g
[PROOFSTEP]
rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → _root_.Nonempty (S ⟶ X)
[PROOFSTEP]
classical
induction' O using Finset.induction with X O' nm h
· exact ⟨Classical.choice IsCofiltered.Nonempty, by intro; simp⟩
· obtain ⟨S', w'⟩ := h
  use min X S'
  rintro Y mY
  obtain rfl | h := eq_or_ne Y X
  · exact ⟨minToLeft _ _⟩
  · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → _root_.Nonempty (S ⟶ X)
[PROOFSTEP]
induction' O using Finset.induction with X O' nm h
[GOAL]
case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (S ⟶ X)
[PROOFSTEP]
exact ⟨Classical.choice IsCofiltered.Nonempty, by intro; simp⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
⊢ ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (Classical.choice (_ : _root_.Nonempty C) ⟶ X)
[PROOFSTEP]
intro
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X✝ : C
⊢ X✝ ∈ ∅ → _root_.Nonempty (Classical.choice (_ : _root_.Nonempty C) ⟶ X✝)
[PROOFSTEP]
simp
[GOAL]
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → _root_.Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
[PROOFSTEP]
obtain ⟨S', w'⟩ := h
[GOAL]
case insert.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
[PROOFSTEP]
use min X S'
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (min X S' ⟶ X_1)
[PROOFSTEP]
rintro Y mY
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
⊢ _root_.Nonempty (min X S' ⟶ Y)
[PROOFSTEP]
obtain rfl | h := eq_or_ne Y X
[GOAL]
case h.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
nm : ¬Y ∈ O'
mY : Y ∈ insert Y O'
⊢ _root_.Nonempty (min Y S' ⟶ Y)
[PROOFSTEP]
exact ⟨minToLeft _ _⟩
[GOAL]
case h.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ _root_.Nonempty (min X S' ⟶ Y)
[PROOFSTEP]
exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H → T mX ≫ f = T mY
[PROOFSTEP]
classical
induction' H using Finset.induction with h' H' nmf h''
· obtain ⟨S, f⟩ := inf_objs_exists O
  refine' ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
· obtain ⟨X, Y, mX, mY, f⟩ := h'
  obtain ⟨S', T', w'⟩ := h''
  refine' ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, _⟩
  intro X' Y' mX' mY' f' mf'
  rw [Category.assoc]
  by_cases h : X = X' ∧ Y = Y'
  · rcases h with ⟨rfl, rfl⟩
    by_cases hf : f = f'
    · subst hf
      apply eq_condition
    · rw [@w' _ _ mX mY f']
      simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'
      rcases mf' with mf' | mf'
      · exfalso
        exact hf mf'.symm
      · exact mf'
  · rw [@w' _ _ mX' mY' f' _]
    apply Finset.mem_of_mem_insert_of_ne mf'
    contrapose! h
    obtain ⟨rfl, h⟩ := h
    trivial
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H → T mX ≫ f = T mY
[PROOFSTEP]
induction' H using Finset.induction with h' H' nmf h''
[GOAL]
case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ ∅ → T mX ≫ f = T mY
[PROOFSTEP]
obtain ⟨S, f⟩ := inf_objs_exists O
[GOAL]
case empty.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → _root_.Nonempty (S ⟶ X)
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ ∅ → T mX ≫ f = T mY
[PROOFSTEP]
refine' ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → _root_.Nonempty (S ⟶ X)
⊢ ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ ∅ →
      (fun {X} mX => Nonempty.some (_ : _root_.Nonempty (S ⟶ X))) mX ≫ f_1 =
        (fun {X} mX => Nonempty.some (_ : _root_.Nonempty (S ⟶ X))) mY
[PROOFSTEP]
rintro - - - - - ⟨⟩
[GOAL]
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : ¬h' ∈ H'
h'' :
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T mX ≫ f = T mY
⊢ ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ insert h' H' →
        T mX ≫ f = T mY
[PROOFSTEP]
obtain ⟨X, Y, mX, mY, f⟩ := h'
[GOAL]
case insert.mk.mk.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h'' :
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T mX ≫ f = T mY
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      { fst := X_1, snd := { fst := Y_1, snd := { fst := mX_1, snd := { fst := mY_1, snd := f_1 } } } } ∈
          insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H' →
        T mX_1 ≫ f_1 = T mY_1
[PROOFSTEP]
obtain ⟨S', T', w'⟩ := h''
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      { fst := X_1, snd := { fst := Y_1, snd := { fst := mX_1, snd := { fst := mY_1, snd := f_1 } } } } ∈
          insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H' →
        T mX_1 ≫ f_1 = T mY_1
[PROOFSTEP]
refine' ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, _⟩
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
⊢ ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
    { fst := X_1, snd := { fst := Y_1, snd := { fst := mX_1, snd := { fst := mY_1, snd := f_1 } } } } ∈
        insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H' →
      (fun {X_2} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX_1 ≫ f_1 =
        (fun {X_2} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY_1
[PROOFSTEP]
intro X' Y' mX' mY' f' mf'
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
case insert.mk.mk.mk.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
by_cases h : X = X' ∧ Y = Y'
[GOAL]
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : X = X' ∧ Y = Y'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
rcases h with ⟨rfl, rfl⟩
[GOAL]
case pos.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
by_cases hf : f = f'
[GOAL]
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
hf : f = f'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
subst hf
[GOAL]
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
apply eq_condition
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
hf : ¬f = f'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
rw [@w' _ _ mX mY f']
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
hf : ¬f = f'
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : f' = f ∨ { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈ H'
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
rcases mf' with mf' | mf'
[GOAL]
case neg.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : f' = f
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
exfalso
[GOAL]
case neg.inl.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : f' = f
⊢ False
[PROOFSTEP]
exact hf mf'.symm
[GOAL]
case neg.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
hf : ¬f = f'
mf' : { fst := X, snd := { fst := Y, snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈ H'
⊢ { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f' } } } } ∈ H'
[PROOFSTEP]
exact mf'
[GOAL]
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : ¬(X = X' ∧ Y = Y')
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
[PROOFSTEP]
rw [@w' _ _ mX' mY' f' _]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : ¬(X = X' ∧ Y = Y')
⊢ { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈ H'
[PROOFSTEP]
apply Finset.mem_of_mem_insert_of_ne mf'
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h : ¬(X = X' ∧ Y = Y')
⊢ { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ≠
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } }
[PROOFSTEP]
contrapose! h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
h :
  { fst := X', snd := { fst := Y', snd := { fst := mX', snd := { fst := mY', snd := f' } } } } =
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } }
⊢ X = X' ∧ Y = Y'
[PROOFSTEP]
obtain ⟨rfl, h⟩ := h
[GOAL]
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ¬{ fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈ H' → T' mX ≫ f = T' mY
mf' :
  { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } ∈
    insert { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H'
⊢ X = X ∧ Y = Y
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ _root_.Nonempty (Cone F)
[PROOFSTEP]
classical
let O := Finset.univ.image F.obj
let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
  Finset.univ.biUnion fun X : J =>
    Finset.univ.biUnion fun Y : J => Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp, by simp, F.map f⟩
obtain ⟨Z, f, w⟩ := inf_exists O H
refine' ⟨⟨Z, ⟨fun X => f (by simp), _⟩⟩⟩
intro j j' g
dsimp
simp only [Category.id_comp]
symm
apply w
simp only [Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq, true_and, exists_and_left]
exact ⟨j, rfl, j', g, by simp⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ _root_.Nonempty (Cone F)
[PROOFSTEP]
let O := Finset.univ.image F.obj
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
⊢ _root_.Nonempty (Cone F)
[PROOFSTEP]
let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
  Finset.univ.biUnion fun X : J =>
    Finset.univ.biUnion fun Y : J => Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp, by simp, F.map f⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
X Y : J
f : X ⟶ Y
⊢ F.obj X ∈ O
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
X Y : J
f : X ⟶ Y
⊢ F.obj Y ∈ O
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
⊢ _root_.Nonempty (Cone F)
[PROOFSTEP]
obtain ⟨Z, f, w⟩ := inf_exists O H
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
⊢ _root_.Nonempty (Cone F)
[PROOFSTEP]
refine' ⟨⟨Z, ⟨fun X => f (by simp), _⟩⟩⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
X : J
⊢ F.obj X ∈ O
[PROOFSTEP]
simp
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y),
    ((Functor.const J).obj Z).map f_1 ≫ (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) Y =
      (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) X ≫ F.map f_1
[PROOFSTEP]
intro j j' g
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ((Functor.const J).obj Z).map g ≫ (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) j' =
    (fun X => f (_ : F.obj X ∈ Finset.image F.obj Finset.univ)) j ≫ F.map g
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ 𝟙 Z ≫ f (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) = f (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ≫ F.map g
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ f (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) = f (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ≫ F.map g
[PROOFSTEP]
symm
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ f (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ≫ F.map g = f (_ : F.obj j' ∈ Finset.image F.obj Finset.univ)
[PROOFSTEP]
apply w
[GOAL]
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ { fst := F.obj j,
      snd :=
        { fst := F.obj j',
          snd :=
            { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
              snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } } } ∈
    H
[PROOFSTEP]
simp only [Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq, true_and, exists_and_left]
[GOAL]
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ∃ a,
    F.obj a = F.obj j ∧
      ∃ x x_1,
        HEq
          { fst := F.obj x,
            snd :=
              { fst := (_ : F.obj a ∈ Finset.image F.obj Finset.univ),
                snd := { fst := (_ : F.obj x ∈ Finset.image F.obj Finset.univ), snd := F.map x_1 } } }
          { fst := F.obj j',
            snd :=
              { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
                snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } }
[PROOFSTEP]
exact ⟨j, rfl, j', g, by simp⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
O✝ : Finset C
H✝ : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O✝) ×' (_ : Y ∈ O✝) ×' (X ⟶ Y))
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun X =>
    Finset.biUnion Finset.univ fun Y =>
      Finset.image
        (fun f =>
          { fst := F.obj X,
            snd :=
              { fst := F.obj Y,
                snd :=
                  { fst := (_ : F.obj X ∈ Finset.image F.obj Finset.univ),
                    snd := { fst := (_ : F.obj Y ∈ Finset.image F.obj Finset.univ), snd := F.map f } } } })
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f_1 } } } } ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ HEq
    { fst := F.obj j',
      snd :=
        { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
          snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } }
    { fst := F.obj j',
      snd :=
        { fst := (_ : F.obj j ∈ Finset.image F.obj Finset.univ),
          snd := { fst := (_ : F.obj j' ∈ Finset.image F.obj Finset.univ), snd := F.map g } } }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsFiltered.coeqHom f.unop g.unop).op ≫ f = (IsFiltered.coeqHom f.unop g.unop).op ≫ g
[PROOFSTEP]
rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f = f.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ g = g.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop).op =
    (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop = g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop
[PROOFSTEP]
exact IsFiltered.coeq_condition f.unop g.unop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f ≫ (IsCofiltered.eqHom f.unop g.unop).op = g ≫ (IsCofiltered.eqHom f.unop g.unop).op
[PROOFSTEP]
rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f = f.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ g = g.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop).op =
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop = IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop
[PROOFSTEP]
exact IsCofiltered.eq_condition f.unop g.unop


[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
⊢ Unique (X ⟶ Y)
[PROOFSTEP]
haveI : HasInitial C := HasZeroObject.hasInitial
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ Unique (X ⟶ Y)
[PROOFSTEP]
apply uniqueHomsetOfInitialIsoTerminal _ X Y
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ ⊥_ C ≅ ⊤_ C
[PROOFSTEP]
refine' ⟨default, (default : ⊤_ C ⟶ 0) ≫ default, _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ default ≫ default ≫ default = 𝟙 (⊥_ C)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ (default ≫ default) ≫ default = 𝟙 (⊤_ C)
[PROOFSTEP]
simp