[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteLimits C
⊢ HasLimitsOfShape J C
[PROOFSTEP]
apply @hasLimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteLimits C
⊢ HasLimitsOfShape (FinCategory.AsType J) C
[PROOFSTEP]
apply HasFiniteLimits.out
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasLimitsOfShape J C
[PROOFSTEP]
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift J)) C
⊢ HasLimitsOfShape J C
[PROOFSTEP]
have l : @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
  @ULiftHomULiftCategory.equiv J hJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift J)) C
l : J ≌ ULiftHom (ULift J)
⊢ HasLimitsOfShape J C
[PROOFSTEP]
apply
  @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
    (@Equivalence.symm J hJ (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l)
    _
      /- Porting note: tried to factor out (@instCategoryULiftHom (ULift J) (@uliftCategory J hJ)
          but when doing that would then find the instance and say it was not definitionally equal to
          the provided one (the same thing factored out) -/
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteColimits C
⊢ HasColimitsOfShape J C
[PROOFSTEP]
refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteColimits C
⊢ HasColimitsOfShape (FinCategory.AsType J) C
[PROOFSTEP]
apply HasFiniteColimits.out
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasColimitsOfShape J C
[PROOFSTEP]
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
⊢ HasColimitsOfShape J C
[PROOFSTEP]
have l : @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
  @ULiftHomULiftCategory.equiv J hJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
l : J ≌ ULiftHom (ULift J)
⊢ HasColimitsOfShape J C
[PROOFSTEP]
apply
  @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
    (@Equivalence.symm J hJ (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
x : WalkingParallelPair
⊢ x ∈ List.toFinset [zero, one]
[PROOFSTEP]
cases x
[GOAL]
case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ zero ∈ List.toFinset [zero, one]
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u
inst✝ : Category.{v, u} C
⊢ one ∈ List.toFinset [zero, one]
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
j j' : WalkingParallelPair
⊢ ∀ (x : WalkingParallelPairHom j j'),
    x ∈
      WalkingParallelPair.recOn j
        (WalkingParallelPair.recOn j' (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
        (WalkingParallelPair.recOn j' ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
⊢ left ∈
    WalkingParallelPair.recOn zero
      (WalkingParallelPair.recOn one (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
      (WalkingParallelPair.recOn one ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
⊢ right ∈
    WalkingParallelPair.recOn zero
      (WalkingParallelPair.recOn one (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
      (WalkingParallelPair.recOn one ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
simp
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
j : WalkingParallelPair
⊢ WalkingParallelPairHom.id j ∈
    WalkingParallelPair.recOn j
      (WalkingParallelPair.recOn j (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
      (WalkingParallelPair.recOn j ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
simp
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
j : WalkingParallelPair
⊢ 𝟙 j ∈
    WalkingParallelPair.rec (WalkingParallelPair.rec {𝟙 zero} {left, right} j) (WalkingParallelPair.rec ∅ {𝟙 one} j) j
[PROOFSTEP]
cases j
[GOAL]
case id.zero
C : Type u
inst✝ : Category.{v, u} C
⊢ 𝟙 zero ∈
    WalkingParallelPair.rec (WalkingParallelPair.rec {𝟙 zero} {left, right} zero)
      (WalkingParallelPair.rec ∅ {𝟙 one} zero) zero
[PROOFSTEP]
simp
[GOAL]
case id.one
C : Type u
inst✝ : Category.{v, u} C
⊢ 𝟙 one ∈
    WalkingParallelPair.rec (WalkingParallelPair.rec {𝟙 zero} {left, right} one) (WalkingParallelPair.rec ∅ {𝟙 one} one)
      one
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteLimits C
⊢ HasEqualizers C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
⊢ HasCoequalizers C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (WidePullbackShape J)
[PROOFSTEP]
rw [WidePullbackShape]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (Option J)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ Finset (j ⟶ j')
[PROOFSTEP]
cases' j' with j'
[GOAL]
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)
[PROOFSTEP]
cases' j with j
[GOAL]
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)
[PROOFSTEP]
exact {Hom.id none}
[GOAL]
case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)
[PROOFSTEP]
exact {Hom.term j}
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
by_cases some j' = j
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
by_cases some j' = j
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
rw [h]
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)
[PROOFSTEP]
exact {Hom.id j}
[GOAL]
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
exact ∅
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn (motive := fun t => j' = t → Finset (j ⟶ j')) j'
        (fun h =>
          (_ : none = j') ▸
            Option.casesOn (motive := fun t => j = t → Finset (j ⟶ none)) j (fun h => (_ : none = j) ▸ {Hom.id none})
              (fun j_1 h => (_ : some j_1 = j) ▸ {Hom.term j_1}) (_ : j = j))
        (fun j'_1 h =>
          (_ : some j'_1 = j') ▸
            if h : some j'_1 = j then Eq.mpr (_ : Finset (j ⟶ some j'_1) = Finset (j ⟶ j)) {Hom.id j} else ∅)
        (_ : j' = j')
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Hom.id j ∈
    Option.casesOn (motive := fun t => j = t → Finset (j ⟶ j)) j
      (fun h =>
        (_ : none = j) ▸
          Option.casesOn (motive := fun t => j = t → Finset (j ⟶ none)) j (fun h => (_ : none = j) ▸ {Hom.id none})
            (fun j_1 h => (_ : some j_1 = j) ▸ {Hom.term j_1}) (_ : j = j))
      (fun j' h =>
        (_ : some j' = j) ▸
          if h : some j' = j then Eq.mpr (_ : Finset (j ⟶ some j') = Finset (j ⟶ j)) {Hom.id j} else ∅)
      (_ : j = j)
[PROOFSTEP]
cases j
[GOAL]
case id.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Hom.id none ∈
    Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
            (fun h => (_ : none = none) ▸ {Hom.id none}) (fun j h => (_ : some j = none) ▸ {Hom.term j})
            (_ : none = none))
      (fun j' h =>
        (_ : some j' = none) ▸
          if h : some j' = none then Eq.mpr (_ : Finset (none ⟶ some j') = Finset (none ⟶ none)) {Hom.id none} else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
case id.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
val✝ : J
⊢ Hom.id (some val✝) ∈
    Option.casesOn (motive := fun t => some val✝ = t → Finset (some val✝ ⟶ some val✝)) (some val✝)
      (fun h =>
        (_ : none = some val✝) ▸
          Option.casesOn (motive := fun t => some val✝ = t → Finset (some val✝ ⟶ none)) (some val✝)
            (fun h => (_ : none = some val✝) ▸ {Hom.id none}) (fun j h => (_ : some j = some val✝) ▸ {Hom.term j})
            (_ : some val✝ = some val✝))
      (fun j' h =>
        (_ : some j' = some val✝) ▸
          if h : some j' = some val✝ then
            Eq.mpr (_ : Finset (some val✝ ⟶ some j') = Finset (some val✝ ⟶ some val✝)) {Hom.id (some val✝)}
          else ∅)
      (_ : some val✝ = some val✝)
[PROOFSTEP]
simp
[GOAL]
case term
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.term j✝ ∈
    Option.casesOn (motive := fun t => none = t → Finset (some j✝ ⟶ none)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => some j✝ = t → Finset (some j✝ ⟶ none)) (some j✝)
            (fun h => (_ : none = some j✝) ▸ {Hom.id none}) (fun j h => (_ : some j = some j✝) ▸ {Hom.term j})
            (_ : some j✝ = some j✝))
      (fun j' h =>
        (_ : some j' = none) ▸
          if h : some j' = some j✝ then
            Eq.mpr (_ : Finset (some j✝ ⟶ some j') = Finset (some j✝ ⟶ some j✝)) {Hom.id (some j✝)}
          else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (WidePushoutShape J)
[PROOFSTEP]
rw [WidePushoutShape]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (Option J)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')
[PROOFSTEP]
cases' j with j
[GOAL]
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')
[PROOFSTEP]
cases' j' with j'
[GOAL]
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)
[PROOFSTEP]
exact {Hom.id none}
[GOAL]
case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')
[PROOFSTEP]
exact {Hom.init j'}
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
by_cases some j = j'
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
by_cases some j = j'
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
rw [h]
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')
[PROOFSTEP]
exact {Hom.id j'}
[GOAL]
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
exact ∅
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn (motive := fun t => j = t → Finset (j ⟶ j')) j
        (fun h =>
          (_ : none = j) ▸
            Option.casesOn (motive := fun t => j' = t → Finset (none ⟶ j')) j'
              (fun h => (_ : none = j') ▸ {Hom.id none}) (fun j'_1 h => (_ : some j'_1 = j') ▸ {Hom.init j'_1})
              (_ : j' = j'))
        (fun j_1 h =>
          (_ : some j_1 = j) ▸
            if h : some j_1 = j' then Eq.mpr (_ : Finset (some j_1 ⟶ j') = Finset (j' ⟶ j')) {Hom.id j'} else ∅)
        (_ : j = j)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePushoutShape J
⊢ Hom.id j ∈
    Option.casesOn (motive := fun t => j = t → Finset (j ⟶ j)) j
      (fun h =>
        (_ : none = j) ▸
          Option.casesOn (motive := fun t => j = t → Finset (none ⟶ j)) j (fun h => (_ : none = j) ▸ {Hom.id none})
            (fun j' h => (_ : some j' = j) ▸ {Hom.init j'}) (_ : j = j))
      (fun j_1 h =>
        (_ : some j_1 = j) ▸
          if h : some j_1 = j then Eq.mpr (_ : Finset (some j_1 ⟶ j) = Finset (j ⟶ j)) {Hom.id j} else ∅)
      (_ : j = j)
[PROOFSTEP]
cases j
[GOAL]
case id.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Hom.id none ∈
    Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
            (fun h => (_ : none = none) ▸ {Hom.id none}) (fun j' h => (_ : some j' = none) ▸ {Hom.init j'})
            (_ : none = none))
      (fun j h =>
        (_ : some j = none) ▸
          if h : some j = none then Eq.mpr (_ : Finset (some j ⟶ none) = Finset (none ⟶ none)) {Hom.id none} else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
case id.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
val✝ : J
⊢ Hom.id (some val✝) ∈
    Option.casesOn (motive := fun t => some val✝ = t → Finset (some val✝ ⟶ some val✝)) (some val✝)
      (fun h =>
        (_ : none = some val✝) ▸
          Option.casesOn (motive := fun t => some val✝ = t → Finset (none ⟶ some val✝)) (some val✝)
            (fun h => (_ : none = some val✝) ▸ {Hom.id none}) (fun j' h => (_ : some j' = some val✝) ▸ {Hom.init j'})
            (_ : some val✝ = some val✝))
      (fun j h =>
        (_ : some j = some val✝) ▸
          if h : some j = some val✝ then
            Eq.mpr (_ : Finset (some j ⟶ some val✝) = Finset (some val✝ ⟶ some val✝)) {Hom.id (some val✝)}
          else ∅)
      (_ : some val✝ = some val✝)
[PROOFSTEP]
simp
[GOAL]
case init
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.init j✝ ∈
    Option.casesOn (motive := fun t => none = t → Finset (none ⟶ some j✝)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => some j✝ = t → Finset (none ⟶ some j✝)) (some j✝)
            (fun h => (_ : none = some j✝) ▸ {Hom.id none}) (fun j' h => (_ : some j' = some j✝) ▸ {Hom.init j'})
            (_ : some j✝ = some j✝))
      (fun j h =>
        (_ : some j = none) ▸
          if h : some j = some j✝ then
            Eq.mpr (_ : Finset (some j ⟶ some j✝) = Finset (some j✝ ⟶ some j✝)) {Hom.id (some j✝)}
          else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
⊢ HasLimitsOfShape (WidePullbackShape J) C
[PROOFSTEP]
cases nonempty_fintype J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
val✝ : Fintype J
⊢ HasLimitsOfShape (WidePullbackShape J) C
[PROOFSTEP]
haveI := @HasFiniteWidePullbacks.out C _ _ J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
val✝ : Fintype J
this : ∀ [inst : Fintype J], HasLimitsOfShape (WidePullbackShape J) C
⊢ HasLimitsOfShape (WidePullbackShape J) C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
⊢ HasColimitsOfShape (WidePushoutShape J) C
[PROOFSTEP]
cases nonempty_fintype J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
val✝ : Fintype J
⊢ HasColimitsOfShape (WidePushoutShape J) C
[PROOFSTEP]
haveI := @HasFiniteWidePushouts.out C _ _ J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
val✝ : Fintype J
this : ∀ [inst : Fintype J], HasColimitsOfShape (WidePushoutShape J) C
⊢ HasColimitsOfShape (WidePushoutShape J) C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
x : WalkingPair
⊢ x ∈ {WalkingPair.left, WalkingPair.right}
[PROOFSTEP]
cases x
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.left ∈ {WalkingPair.left, WalkingPair.right}
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.right ∈ {WalkingPair.left, WalkingPair.right}
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasFiniteWidePullbacks C
⊢ HasPullbacks C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasFiniteWidePushouts C
⊢ HasPushouts C
[PROOFSTEP]
infer_instance
