[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ ((Functor.const J).obj i.pt).map f ≫ (fun j => Fork.ι i ≫ NatTrans.app c₁.π { as := j }) j₂ =
    (fun j => Fork.ι i ≫ NatTrans.app c₁.π { as := j }) j₁ ≫ F.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ 𝟙 i.pt ≫ Fork.ι i ≫ NatTrans.app c₁.π { as := j₂ } = (Fork.ι i ≫ NatTrans.app c₁.π { as := j₁ }) ≫ F.map f
[PROOFSTEP]
rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ q.pt ⟶ (buildLimit s t hs ht i).pt
[PROOFSTEP]
refine' hi.lift (Fork.ofι _ _)
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ q.1 ⟶ c₁.pt
[PROOFSTEP]
refine' t₁.lift (Fan.mk _ fun j => _)
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
j : J
⊢ q.1 ⟶ F.obj j
[PROOFSTEP]
apply q.π.app j
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ s =
    IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ t
[PROOFSTEP]
apply t₂.hom_ext
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ ∀ (j : Discrete ((p : J × J) × (p.fst ⟶ p.snd))),
    (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ s) ≫ NatTrans.app c₂.π j =
      (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ t) ≫ NatTrans.app c₂.π j
[PROOFSTEP]
intro ⟨j⟩
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
j : (p : J × J) × (p.fst ⟶ p.snd)
⊢ (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ s) ≫ NatTrans.app c₂.π { as := j } =
    (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ t) ≫ NatTrans.app c₂.π { as := j }
[PROOFSTEP]
simp [hs, ht]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s✝ t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s✝ ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s✝ t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
s : Cone F
j : J
⊢ (fun q =>
          IsLimit.lift hi
            (Fork.ofι (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j))
              (_ :
                IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ s✝ =
                  IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ t)))
        s ≫
      NatTrans.app (buildLimit s✝ t hs ht i).π j =
    NatTrans.app s.π j
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
m : q.pt ⟶ (buildLimit s t hs ht i).pt
w : ∀ (j : J), m ≫ NatTrans.app (buildLimit s t hs ht i).π j = NatTrans.app q.π j
j : Discrete J
⊢ (m ≫ Fork.ι i) ≫ NatTrans.app c₁.π j =
    ((fun q =>
            IsLimit.lift hi
              (Fork.ofι (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j))
                (_ :
                  IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ s =
                    IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ t)))
          q ≫
        Fork.ι i) ≫
      NatTrans.app c₁.π j
[PROOFSTEP]
cases' j with j
[GOAL]
case mk
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f => F.obj f.fst.snd
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.fst } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), t ≫ NatTrans.app c₂.π { as := f } = NatTrans.app c₁.π { as := f.fst.snd }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
m : q.pt ⟶ (buildLimit s t hs ht i).pt
w : ∀ (j : J), m ≫ NatTrans.app (buildLimit s t hs ht i).π j = NatTrans.app q.π j
j : J
⊢ (m ≫ Fork.ι i) ≫ NatTrans.app c₁.π { as := j } =
    ((fun q =>
            IsLimit.lift hi
              (Fork.ofι (IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j))
                (_ :
                  IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ s =
                    IsLimit.lift t₁ (Fan.mk q.1 fun j => NatTrans.app q.π j) ≫ t)))
          q ≫
        Fork.ι i) ≫
      NatTrans.app c₁.π { as := j }
[PROOFSTEP]
simpa using w j
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : HasLimit (Discrete.functor F.obj)
inst✝¹ : HasLimit (Discrete.functor fun f => F.obj f.fst.snd)
inst✝ : HasEqualizers C
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    (Pi.lift fun f => limit.π (Discrete.functor F.obj) { as := f.fst.1 } ≫ F.map f.snd) ≫
        NatTrans.app (limit.cone (Discrete.functor fun f => F.obj f.fst.snd)).π { as := f } =
      NatTrans.app (limit.cone (Discrete.functor F.obj)).π { as := f.fst.fst } ≫ F.map f.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : HasLimit (Discrete.functor F.obj)
inst✝¹ : HasLimit (Discrete.functor fun f => F.obj f.fst.snd)
inst✝ : HasEqualizers C
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    (Pi.lift fun f => limit.π (Discrete.functor F.obj) { as := f.fst.snd }) ≫
        NatTrans.app (limit.cone (Discrete.functor fun f => F.obj f.fst.snd)).π { as := f } =
      NatTrans.app (limit.cone (Discrete.functor F.obj)).π { as := f.fst.snd }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
⊢ PreservesLimit K G
[PROOFSTEP]
let P := ∏ K.obj
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
⊢ PreservesLimit K G
[PROOFSTEP]
let Q := ∏ fun f : Σ p : J × J, p.fst ⟶ p.snd => K.obj f.1.2
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
⊢ PreservesLimit K G
[PROOFSTEP]
let s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) ⟨_⟩ ≫ K.map f.2
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
⊢ PreservesLimit K G
[PROOFSTEP]
let t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) ⟨f.1.2⟩
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
⊢ PreservesLimit K G
[PROOFSTEP]
let I := equalizer s t
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
⊢ PreservesLimit K G
[PROOFSTEP]
let i : I ⟶ P := equalizer.ι s t
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ PreservesLimit K G
[PROOFSTEP]
apply
  preservesLimitOfPreservesLimitCone
    (buildIsLimit s t (by simp) (by simp) (limit.isLimit _) (limit.isLimit _) (limit.isLimit _))
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    s ≫ NatTrans.app (limit.cone (Discrete.functor fun f => K.obj f.fst.snd)).π { as := f } =
      NatTrans.app (limit.cone (Discrete.functor K.obj)).π { as := f.fst.fst } ≫ K.map f.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    t ≫ NatTrans.app (limit.cone (Discrete.functor fun f => K.obj f.fst.snd)).π { as := f } =
      NatTrans.app (limit.cone (Discrete.functor K.obj)).π { as := f.fst.snd }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit
    (G.mapCone
      (buildLimit s t
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                  (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd) ≫
                limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
              limit.π (Discrete.functor K.obj) { as := a.fst.fst } ≫ K.map a.snd)
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                  (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }) ≫
                limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
              limit.π (Discrete.functor K.obj) { as := a.fst.snd })
        (limit.cone (parallelPair s t))))
[PROOFSTEP]
refine' IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
[GOAL]
case refine'_1
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ Fan (K ⋙ G).toPrefunctor.obj
[PROOFSTEP]
exact Fan.mk _ fun j => G.map (Pi.π _ j)
[GOAL]
case refine'_2
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ Fan fun f => (K ⋙ G).obj f.fst.snd
[PROOFSTEP]
exact Fan.mk (G.obj Q) fun f => G.map (Pi.π _ f)
[GOAL]
case refine'_3
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).pt ⟶
    (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).pt
[PROOFSTEP]
apply G.map s
[GOAL]
case refine'_4
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).pt ⟶
    (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).pt
[PROOFSTEP]
apply G.map t
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    G.map s ≫ NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
      NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
          { as := f.fst.fst } ≫
        (K ⋙ G).map f.snd
[PROOFSTEP]
intro f
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map s ≫ NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
    NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
        { as := f.fst.fst } ≫
      (K ⋙ G).map f.snd
[PROOFSTEP]
dsimp [Fan.mk]
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd) ≫
      G.map (Pi.π (fun f => K.obj f.fst.snd) f) =
    G.map (Pi.π (fun j => K.obj j) f.fst.fst) ≫ G.map (K.map f.snd)
[PROOFSTEP]
simp only [← G.map_comp, limit.lift_π]
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map
      (NatTrans.app (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd).π
        { as := f }) =
    G.map (Pi.π (fun j => K.obj j) f.fst.fst ≫ K.map f.snd)
[PROOFSTEP]
congr
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    G.map t ≫ NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
      NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
        { as := f.fst.snd }
[PROOFSTEP]
intro f
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map t ≫ NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
    NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π { as := f.fst.snd }
[PROOFSTEP]
dsimp [Fan.mk]
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }) ≫
      G.map (Pi.π (fun f => K.obj f.fst.snd) f) =
    G.map (Pi.π (fun j => K.obj j) f.fst.snd)
[PROOFSTEP]
simp only [← G.map_comp, limit.lift_π]
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map (NatTrans.app (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }).π { as := f }) =
    G.map (Pi.π (fun j => K.obj j) f.fst.snd)
[PROOFSTEP]
apply congrArg G.map
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ NatTrans.app (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }).π { as := f } =
    Pi.π (fun j => K.obj j) f.fst.snd
[PROOFSTEP]
dsimp
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ Fork (G.map s) (G.map t)
[PROOFSTEP]
apply Fork.ofι (G.map i)
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ G.map i ≫ G.map s = G.map i ≫ G.map t
[PROOFSTEP]
rw [← G.map_comp, ← G.map_comp]
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ G.map (i ≫ s) = G.map (i ≫ t)
[PROOFSTEP]
apply congrArg G.map
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ i ≫ s = i ≫ t
[PROOFSTEP]
exact equalizer.condition s t
[GOAL]
case refine'_8
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j))
[PROOFSTEP]
apply isLimitOfHasProductOfPreservesLimit
[GOAL]
case refine'_9
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f))
[PROOFSTEP]
apply isLimitOfHasProductOfPreservesLimit
[GOAL]
case refine'_10
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit (Fork.ofι (G.map i) (_ : G.map i ≫ G.map s = G.map i ≫ G.map t))
[PROOFSTEP]
apply isLimitForkMapOfIsLimit
[GOAL]
case refine'_10.l
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit (Fork.ofι i ?refine'_10.w)
case refine'_10.w
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ i ≫ s = i ≫ t
[PROOFSTEP]
apply equalizerIsEqualizer
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ buildLimit (G.map s) (G.map t)
      (_ :
        ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
          G.map s ≫ NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
            NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                { as := f.fst.fst } ≫
              (K ⋙ G).map f.snd)
      (_ :
        ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
          G.map t ≫ NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
            NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
              { as := f.fst.snd })
      (Fork.ofι (G.map i) (_ : G.map i ≫ G.map s = G.map i ≫ G.map t)) ≅
    G.mapCone
      (buildLimit s t
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                  (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd) ≫
                limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
              limit.π (Discrete.functor K.obj) { as := a.fst.fst } ≫ K.map a.snd)
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                  (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }) ≫
                limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
              limit.π (Discrete.functor K.obj) { as := a.fst.snd })
        (limit.cone (parallelPair s t)))
[PROOFSTEP]
refine Cones.ext (Iso.refl _) ?_
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (j : J),
    NatTrans.app
        (buildLimit (G.map s) (G.map t)
            (_ :
              ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                G.map s ≫
                    NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
                  NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                      { as := f.fst.fst } ≫
                    (K ⋙ G).map f.snd)
            (_ :
              ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                G.map t ≫
                    NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
                  NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                    { as := f.fst.snd })
            (Fork.ofι (G.map i) (_ : G.map i ≫ G.map s = G.map i ≫ G.map t))).π
        j =
      (Iso.refl
            (buildLimit (G.map s) (G.map t)
                (_ :
                  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                    G.map s ≫
                        NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π
                          { as := f } =
                      NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                          { as := f.fst.fst } ≫
                        (K ⋙ G).map f.snd)
                (_ :
                  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                    G.map t ≫
                        NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π
                          { as := f } =
                      NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                        { as := f.fst.snd })
                (Fork.ofι (G.map i) (_ : G.map i ≫ G.map s = G.map i ≫ G.map t))).pt).hom ≫
        NatTrans.app
          (G.mapCone
              (buildLimit s t
                (_ :
                  ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                    limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                          (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd) ≫
                        limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
                      limit.π (Discrete.functor K.obj) { as := a.fst.fst } ≫ K.map a.snd)
                (_ :
                  ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                    limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                          (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }) ≫
                        limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
                      limit.π (Discrete.functor K.obj) { as := a.fst.snd })
                (limit.cone (parallelPair s t)))).π
          j
[PROOFSTEP]
intro j
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ NatTrans.app
      (buildLimit (G.map s) (G.map t)
          (_ :
            ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
              G.map s ≫
                  NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
                NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                    { as := f.fst.fst } ≫
                  (K ⋙ G).map f.snd)
          (_ :
            ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
              G.map t ≫
                  NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
                NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                  { as := f.fst.snd })
          (Fork.ofι (G.map i) (_ : G.map i ≫ G.map s = G.map i ≫ G.map t))).π
      j =
    (Iso.refl
          (buildLimit (G.map s) (G.map t)
              (_ :
                ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                  G.map s ≫
                      NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
                    NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                        { as := f.fst.fst } ≫
                      (K ⋙ G).map f.snd)
              (_ :
                ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                  G.map t ≫
                      NatTrans.app (Fan.mk (G.obj Q) fun f => G.map (Pi.π (fun f => K.obj f.fst.snd) f)).π { as := f } =
                    NatTrans.app (Fan.mk (G.obj (∏ fun j => K.obj j)) fun j => G.map (Pi.π (fun j => K.obj j) j)).π
                      { as := f.fst.snd })
              (Fork.ofι (G.map i) (_ : G.map i ≫ G.map s = G.map i ≫ G.map t))).pt).hom ≫
      NatTrans.app
        (G.mapCone
            (buildLimit s t
              (_ :
                ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                  limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                        (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd) ≫
                      limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
                    limit.π (Discrete.functor K.obj) { as := a.fst.fst } ≫ K.map a.snd)
              (_ :
                ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                  limit.lift (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b)
                        (Fan.mk (∏ K.obj) fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }) ≫
                      limit.π (Discrete.functor fun b => (fun f => K.obj f.fst.snd) b) { as := a } =
                    limit.π (Discrete.functor K.obj) { as := a.fst.snd })
              (limit.cone (parallelPair s t)))).π
        j
[PROOFSTEP]
dsimp
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∏ K.obj
Q : C := ∏ fun f => K.obj f.fst.snd
s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ G.map
        (equalizer.ι (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd)
          (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd })) ≫
      G.map (Pi.π (fun j => K.obj j) j) =
    𝟙
        (G.obj
          (equalizer (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd)
            (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }))) ≫
      G.map
        (equalizer.ι (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd)
            (Pi.lift fun f => limit.π (Discrete.functor K.obj) { as := f.fst.snd }) ≫
          limit.π (Discrete.functor K.obj) { as := j })
[PROOFSTEP]
simp
  -- See note [dsimp, simp].
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
⊢ (J : Type) → [inst : SmallCategory J] → [inst_1 : FinCategory J] → PreservesLimitsOfShape J G
[PROOFSTEP]
intro J sJ fJ
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J G
[PROOFSTEP]
haveI : Fintype J := inferInstance
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : Fintype J
⊢ PreservesLimitsOfShape J G
[PROOFSTEP]
haveI : Fintype ((p : J × J) × (p.fst ⟶ p.snd)) := inferInstance
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ PreservesLimitsOfShape J G
[PROOFSTEP]
apply @preservesLimitOfPreservesEqualizersAndProduct _ _ _ sJ _ _ ?_ ?_ _ G _ ?_ ?_
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ HasLimitsOfShape (Discrete J) C
[PROOFSTEP]
apply hasLimitsOfShape_discrete _ _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ HasLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
[PROOFSTEP]
apply hasLimitsOfShape_discrete _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ PreservesLimitsOfShape (Discrete J) G
[PROOFSTEP]
apply PreservesFiniteProducts.preserves _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ PreservesLimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
[PROOFSTEP]
apply PreservesFiniteProducts.preserves _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
⊢ PreservesFiniteLimits G
[PROOFSTEP]
haveI : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this : HasFiniteLimits C
⊢ PreservesFiniteLimits G
[PROOFSTEP]
haveI : PreservesLimitsOfShape (Discrete WalkingPair) G := preservesBinaryProductsOfPreservesTerminalAndPullbacks G
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝ : HasFiniteLimits C
this : PreservesLimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteLimits G
[PROOFSTEP]
haveI : PreservesLimitsOfShape WalkingParallelPair G := preservesEqualizersOfPreservesPullbacksAndBinaryProducts G
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteLimits G
[PROOFSTEP]
apply @preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts _ _ _ _ _ _ G _ ?_
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteProducts G
[PROOFSTEP]
apply PreservesFiniteProducts.mk
[GOAL]
case preserves
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ (J : Type) → [inst : Fintype J] → PreservesLimitsOfShape (Discrete J) G
[PROOFSTEP]
apply preservesFiniteProductsOfPreservesBinaryAndTerminal G
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F.map f ≫ (fun j => NatTrans.app c₂.ι { as := j } ≫ Cofork.π i) j₂ =
    (fun j => NatTrans.app c₂.ι { as := j } ≫ Cofork.π i) j₁ ≫ ((Functor.const J).obj i.pt).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F.map f ≫ NatTrans.app c₂.ι { as := j₂ } ≫ Cofork.π i = (NatTrans.app c₂.ι { as := j₁ } ≫ Cofork.π i) ≫ 𝟙 i.pt
[PROOFSTEP]
have reassoced (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} {h : _ ⟶ W} :
  c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h := by simp only [← Category.assoc, eq_whisker (hs f)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
j₁ j₂ : J
f✝ : j₁ ⟶ j₂
f : (p : J × J) × (p.fst ⟶ p.snd)
W : C
h : c₂.pt ⟶ W
⊢ NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
[PROOFSTEP]
simp only [← Category.assoc, eq_whisker (hs f)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} {h : c₂.pt ⟶ W},
    NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
⊢ F.map f ≫ NatTrans.app c₂.ι { as := j₂ } ≫ Cofork.π i = (NatTrans.app c₂.ι { as := j₁ } ≫ Cofork.π i) ≫ 𝟙 i.pt
[PROOFSTEP]
rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.assoc, ht]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ (buildColimit s t hs ht i).pt ⟶ q.pt
[PROOFSTEP]
refine' hi.desc (Cofork.ofπ _ _)
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ c₂.pt ⟶ q.1
[PROOFSTEP]
refine' t₂.desc (Cofan.mk _ fun j => _)
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : J
⊢ F.obj j ⟶ q.1
[PROOFSTEP]
apply q.ι.app j
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
    t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j)
[PROOFSTEP]
apply t₁.hom_ext
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ ∀ (j : Discrete ((p : J × J) × (p.fst ⟶ p.snd))),
    NatTrans.app c₁.ι j ≫ s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
      NatTrans.app c₁.ι j ≫ t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j)
[PROOFSTEP]
intro j
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : Discrete ((p : J × J) × (p.fst ⟶ p.snd))
⊢ NatTrans.app c₁.ι j ≫ s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
    NatTrans.app c₁.ι j ≫ t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j)
[PROOFSTEP]
cases' j with j
[GOAL]
case refine'_2.mk
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.fst ⟶ p.snd)
⊢ NatTrans.app c₁.ι { as := j } ≫ s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
    NatTrans.app c₁.ι { as := j } ≫ t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j)
[PROOFSTEP]
have reassoced_s (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
  c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h :=
  by
  simp only [← Category.assoc]
  apply eq_whisker (hs f)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j f : (p : J × J) × (p.fst ⟶ p.snd)
W : C
h : c₂.pt ⟶ W
⊢ NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j f : (p : J × J) × (p.fst ⟶ p.snd)
W : C
h : c₂.pt ⟶ W
⊢ (NatTrans.app c₁.ι { as := f } ≫ s) ≫ h = (F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }) ≫ h
[PROOFSTEP]
apply eq_whisker (hs f)
[GOAL]
case refine'_2.mk
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.fst ⟶ p.snd)
reassoced_s :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : c₂.pt ⟶ W),
    NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
⊢ NatTrans.app c₁.ι { as := j } ≫ s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
    NatTrans.app c₁.ι { as := j } ≫ t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j)
[PROOFSTEP]
have reassoced_t (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
  c₁.ι.app ⟨f⟩ ≫ t ≫ h = c₂.ι.app ⟨f.fst.fst⟩ ≫ h :=
  by
  simp only [← Category.assoc]
  apply eq_whisker (ht f)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.fst ⟶ p.snd)
reassoced_s :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : c₂.pt ⟶ W),
    NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
f : (p : J × J) × (p.fst ⟶ p.snd)
W : C
h : c₂.pt ⟶ W
⊢ NatTrans.app c₁.ι { as := f } ≫ t ≫ h = NatTrans.app c₂.ι { as := f.fst.fst } ≫ h
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.fst ⟶ p.snd)
reassoced_s :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : c₂.pt ⟶ W),
    NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
f : (p : J × J) × (p.fst ⟶ p.snd)
W : C
h : c₂.pt ⟶ W
⊢ (NatTrans.app c₁.ι { as := f } ≫ t) ≫ h = NatTrans.app c₂.ι { as := f.fst.fst } ≫ h
[PROOFSTEP]
apply eq_whisker (ht f)
[GOAL]
case refine'_2.mk
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.fst ⟶ p.snd)
reassoced_s :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : c₂.pt ⟶ W),
    NatTrans.app c₁.ι { as := f } ≫ s ≫ h = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd } ≫ h
reassoced_t :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : c₂.pt ⟶ W),
    NatTrans.app c₁.ι { as := f } ≫ t ≫ h = NatTrans.app c₂.ι { as := f.fst.fst } ≫ h
⊢ NatTrans.app c₁.ι { as := j } ≫ s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
    NatTrans.app c₁.ι { as := j } ≫ t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j)
[PROOFSTEP]
simp [reassoced_s, reassoced_t]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s✝ t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s✝ = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s✝ t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
s : Cocone F
j : J
⊢ NatTrans.app (buildColimit s✝ t hs ht i).ι j ≫
      (fun q =>
          IsColimit.desc hi
            (Cofork.ofπ (IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j))
              (_ :
                s✝ ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
                  t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j))))
        s =
    NatTrans.app s.ι j
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
m : (buildColimit s t hs ht i).pt ⟶ q.pt
w : ∀ (j : J), NatTrans.app (buildColimit s t hs ht i).ι j ≫ m = NatTrans.app q.ι j
j : Discrete J
⊢ NatTrans.app c₂.ι j ≫ Cofork.π i ≫ m =
    NatTrans.app c₂.ι j ≫
      Cofork.π i ≫
        (fun q =>
            IsColimit.desc hi
              (Cofork.ofπ (IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j))
                (_ :
                  s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
                    t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j))))
          q
[PROOFSTEP]
cases' j with j
[GOAL]
case mk
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f => F.obj f.fst.fst
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app c₁.ι { as := f } ≫ s = F.map f.snd ≫ NatTrans.app c₂.ι { as := f.fst.snd }
ht : ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)), NatTrans.app c₁.ι { as := f } ≫ t = NatTrans.app c₂.ι { as := f.fst.fst }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
m : (buildColimit s t hs ht i).pt ⟶ q.pt
w : ∀ (j : J), NatTrans.app (buildColimit s t hs ht i).ι j ≫ m = NatTrans.app q.ι j
j : J
⊢ NatTrans.app c₂.ι { as := j } ≫ Cofork.π i ≫ m =
    NatTrans.app c₂.ι { as := j } ≫
      Cofork.π i ≫
        (fun q =>
            IsColimit.desc hi
              (Cofork.ofπ (IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j))
                (_ :
                  s ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j) =
                    t ≫ IsColimit.desc t₂ (Cofan.mk q.1 fun j => NatTrans.app q.ι j))))
          q
[PROOFSTEP]
simpa using w j
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : SmallCategory J
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : J ⥤ C
inst✝² : HasColimit (Discrete.functor F.obj)
inst✝¹ : HasColimit (Discrete.functor fun f => F.obj f.fst.fst)
inst✝ : HasCoequalizers C
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    (NatTrans.app (colimit.cocone (Discrete.functor fun f => F.obj f.fst.fst)).ι { as := f } ≫
        Sigma.desc fun f => F.map f.snd ≫ colimit.ι (Discrete.functor F.obj) { as := f.fst.snd }) =
      F.map f.snd ≫ NatTrans.app (colimit.cocone (Discrete.functor F.obj)).ι { as := f.fst.snd }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : SmallCategory J
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : J ⥤ C
inst✝² : HasColimit (Discrete.functor F.obj)
inst✝¹ : HasColimit (Discrete.functor fun f => F.obj f.fst.fst)
inst✝ : HasCoequalizers C
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    (NatTrans.app (colimit.cocone (Discrete.functor fun f => F.obj f.fst.fst)).ι { as := f } ≫
        Sigma.desc fun f => colimit.ι (Discrete.functor F.obj) { as := f.fst.fst }) =
      NatTrans.app (colimit.cocone (Discrete.functor F.obj)).ι { as := f.fst.fst }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
⊢ PreservesColimit K G
[PROOFSTEP]
let P := ∐ K.obj
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
⊢ PreservesColimit K G
[PROOFSTEP]
let Q := ∐ fun f : Σ p : J × J, p.fst ⟶ p.snd => K.obj f.1.1
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
⊢ PreservesColimit K G
[PROOFSTEP]
let s : Q ⟶ P := Sigma.desc fun f => K.map f.2 ≫ colimit.ι (Discrete.functor K.obj) ⟨_⟩
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
⊢ PreservesColimit K G
[PROOFSTEP]
let t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) ⟨f.1.1⟩
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
⊢ PreservesColimit K G
[PROOFSTEP]
let I := coequalizer s t
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
⊢ PreservesColimit K G
[PROOFSTEP]
let i : P ⟶ I := coequalizer.π s t
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ PreservesColimit K G
[PROOFSTEP]
apply
  preservesColimitOfPreservesColimitCocone
    (buildIsColimit s t (by simp) (by simp) (colimit.isColimit _) (colimit.isColimit _) (colimit.isColimit _))
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app (colimit.cocone (Discrete.functor fun f => K.obj f.fst.fst)).ι { as := f } ≫ s =
      K.map f.snd ≫ NatTrans.app (colimit.cocone (Discrete.functor K.obj)).ι { as := f.fst.snd }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app (colimit.cocone (Discrete.functor fun f => K.obj f.fst.fst)).ι { as := f } ≫ t =
      NatTrans.app (colimit.cocone (Discrete.functor K.obj)).ι { as := f.fst.fst }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit
    (G.mapCocone
      (buildColimit s t
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                  (Cofan.mk (∐ K.obj) fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }) =
              K.map a.snd ≫ colimit.ι (Discrete.functor K.obj) { as := a.fst.snd })
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                  (Cofan.mk (∐ K.obj) fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }) =
              colimit.ι (Discrete.functor K.obj) { as := a.fst.fst })
        (colimit.cocone (parallelPair s t))))
[PROOFSTEP]
refine' IsColimit.ofIsoColimit (buildIsColimit _ _ _ _ _ _ _) _
[GOAL]
case refine'_1
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ Cofan fun f => (K ⋙ G).obj f.fst.fst
[PROOFSTEP]
refine Cofan.mk (G.obj Q) fun j => G.map ?_
[GOAL]
case refine'_1
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
j : (p : J × J) × (p.fst ⟶ p.snd)
⊢ K.obj j.fst.fst ⟶ Q
[PROOFSTEP]
apply Sigma.ι _ j
[GOAL]
case refine'_2
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ Cofan (K ⋙ G).toPrefunctor.obj
[PROOFSTEP]
exact Cofan.mk _ fun f => G.map (Sigma.ι _ f)
[GOAL]
case refine'_3
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).pt ⟶
    (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).pt
[PROOFSTEP]
apply G.map s
[GOAL]
case refine'_4
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).pt ⟶
    (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).pt
[PROOFSTEP]
apply G.map t
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫ G.map s =
      (K ⋙ G).map f.snd ≫
        NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.snd }
[PROOFSTEP]
intro f
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫ G.map s =
    (K ⋙ G).map f.snd ≫ NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.snd }
[PROOFSTEP]
dsimp [Cofan.mk]
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map (Sigma.ι (fun j => K.obj j.fst.fst) f) ≫
      G.map (Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }) =
    G.map (K.map f.snd) ≫ G.map (Sigma.ι K.obj f.fst.snd)
[PROOFSTEP]
simp only [← G.map_comp, colimit.ι_desc]
[GOAL]
case refine'_5
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map
      (NatTrans.app (Cofan.mk (∐ K.obj) fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }).ι
        { as := f }) =
    G.map (K.map f.snd ≫ Sigma.ι K.obj f.fst.snd)
[PROOFSTEP]
congr
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
    NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫ G.map t =
      NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst }
[PROOFSTEP]
intro f
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫ G.map t =
    NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst }
[PROOFSTEP]
dsimp [Cofan.mk]
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map (Sigma.ι (fun j => K.obj j.fst.fst) f) ≫
      G.map (Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }) =
    G.map (Sigma.ι K.obj f.fst.fst)
[PROOFSTEP]
simp only [← G.map_comp, colimit.ι_desc]
[GOAL]
case refine'_6
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.fst ⟶ p.snd)
⊢ G.map
      (NatTrans.app (Cofan.mk (∐ K.obj) fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }).ι
        { as := f }) =
    G.map (Sigma.ι K.obj f.fst.fst)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ Cofork (G.map s) (G.map t)
[PROOFSTEP]
refine Cofork.ofπ (G.map i) ?_
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ G.map s ≫ G.map i = G.map t ≫ G.map i
[PROOFSTEP]
rw [← G.map_comp, ← G.map_comp]
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ G.map (s ≫ i) = G.map (t ≫ i)
[PROOFSTEP]
apply congrArg G.map
[GOAL]
case refine'_7
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ s ≫ i = t ≫ i
[PROOFSTEP]
apply coequalizer.condition
[GOAL]
case refine'_8
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j))
[PROOFSTEP]
apply isColimitOfHasCoproductOfPreservesColimit
[GOAL]
case refine'_9
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f))
[PROOFSTEP]
apply isColimitOfHasCoproductOfPreservesColimit
[GOAL]
case refine'_10
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit (Cofork.ofπ (G.map i) (_ : G.map s ≫ G.map i = G.map t ≫ G.map i))
[PROOFSTEP]
apply isColimitCoforkMapOfIsColimit
[GOAL]
case refine'_10.l
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit (Cofork.ofπ i ?refine'_10.w)
case refine'_10.w
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ s ≫ i = t ≫ i
[PROOFSTEP]
apply coequalizerIsCoequalizer
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ buildColimit (G.map s) (G.map t)
      (_ :
        ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
          NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫
              G.map s =
            (K ⋙ G).map f.snd ≫
              NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.snd })
      (_ :
        ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
          NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫
              G.map t =
            NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst })
      (Cofork.ofπ (G.map i) (_ : G.map s ≫ G.map i = G.map t ≫ G.map i)) ≅
    G.mapCocone
      (buildColimit s t
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                  (Cofan.mk (∐ K.obj) fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }) =
              K.map a.snd ≫ colimit.ι (Discrete.functor K.obj) { as := a.fst.snd })
        (_ :
          ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
            colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                  (Cofan.mk (∐ K.obj) fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }) =
              colimit.ι (Discrete.functor K.obj) { as := a.fst.fst })
        (colimit.cocone (parallelPair s t)))
[PROOFSTEP]
refine' Cocones.ext (Iso.refl _) _
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (j : J),
    NatTrans.app
          (buildColimit (G.map s) (G.map t)
              (_ :
                ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                  NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι
                        { as := f } ≫
                      G.map s =
                    (K ⋙ G).map f.snd ≫
                      NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.snd })
              (_ :
                ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                  NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι
                        { as := f } ≫
                      G.map t =
                    NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst })
              (Cofork.ofπ (G.map i) (_ : G.map s ≫ G.map i = G.map t ≫ G.map i))).ι
          j ≫
        (Iso.refl
            (buildColimit (G.map s) (G.map t)
                (_ :
                  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                    NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι
                          { as := f } ≫
                        G.map s =
                      (K ⋙ G).map f.snd ≫
                        NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι
                          { as := f.fst.snd })
                (_ :
                  ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                    NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι
                          { as := f } ≫
                        G.map t =
                      NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst })
                (Cofork.ofπ (G.map i) (_ : G.map s ≫ G.map i = G.map t ≫ G.map i))).pt).hom =
      NatTrans.app
        (G.mapCocone
            (buildColimit s t
              (_ :
                ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                  colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                      colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                        (Cofan.mk (∐ K.obj) fun f =>
                          K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }) =
                    K.map a.snd ≫ colimit.ι (Discrete.functor K.obj) { as := a.fst.snd })
              (_ :
                ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                  colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                      colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                        (Cofan.mk (∐ K.obj) fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }) =
                    colimit.ι (Discrete.functor K.obj) { as := a.fst.fst })
              (colimit.cocone (parallelPair s t)))).ι
        j
[PROOFSTEP]
intro j
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
j : J
⊢ NatTrans.app
        (buildColimit (G.map s) (G.map t)
            (_ :
              ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫
                    G.map s =
                  (K ⋙ G).map f.snd ≫
                    NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.snd })
            (_ :
              ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι { as := f } ≫
                    G.map t =
                  NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst })
            (Cofork.ofπ (G.map i) (_ : G.map s ≫ G.map i = G.map t ≫ G.map i))).ι
        j ≫
      (Iso.refl
          (buildColimit (G.map s) (G.map t)
              (_ :
                ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                  NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι
                        { as := f } ≫
                      G.map s =
                    (K ⋙ G).map f.snd ≫
                      NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.snd })
              (_ :
                ∀ (f : (p : J × J) × (p.fst ⟶ p.snd)),
                  NatTrans.app (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.fst) j)).ι
                        { as := f } ≫
                      G.map t =
                    NatTrans.app (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι { as := f.fst.fst })
              (Cofork.ofπ (G.map i) (_ : G.map s ≫ G.map i = G.map t ≫ G.map i))).pt).hom =
    NatTrans.app
      (G.mapCocone
          (buildColimit s t
            (_ :
              ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                    colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                      (Cofan.mk (∐ K.obj) fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }) =
                  K.map a.snd ≫ colimit.ι (Discrete.functor K.obj) { as := a.fst.snd })
            (_ :
              ∀ (a : (p : J × J) × (p.fst ⟶ p.snd)),
                colimit.ι (Discrete.functor fun f => K.obj f.fst.fst) { as := a } ≫
                    colimit.desc (Discrete.functor fun f => K.obj f.fst.fst)
                      (Cofan.mk (∐ K.obj) fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }) =
                  colimit.ι (Discrete.functor K.obj) { as := a.fst.fst })
            (colimit.cocone (parallelPair s t)))).ι
      j
[PROOFSTEP]
dsimp
[GOAL]
case refine'_11
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.fst
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
j : J
⊢ (G.map (Sigma.ι K.obj j) ≫
        G.map
          (coequalizer.π (Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 })
            (Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }))) ≫
      𝟙
        (G.obj
          (coequalizer (Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 })
            (Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }))) =
    G.map
      (colimit.ι (Discrete.functor K.obj) { as := j } ≫
        coequalizer.π (Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 })
          (Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.fst }))
[PROOFSTEP]
simp
  -- See note [dsimp, simp].
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
⊢ (J : Type) → [inst : SmallCategory J] → [inst_1 : FinCategory J] → PreservesColimitsOfShape J G
[PROOFSTEP]
intro J sJ fJ
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J G
[PROOFSTEP]
haveI : Fintype J := inferInstance
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : Fintype J
⊢ PreservesColimitsOfShape J G
[PROOFSTEP]
haveI : Fintype ((p : J × J) × (p.fst ⟶ p.snd)) := inferInstance
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ PreservesColimitsOfShape J G
[PROOFSTEP]
apply @preservesColimitOfPreservesCoequalizersAndCoproduct _ _ _ sJ _ _ ?_ ?_ _ G _ ?_ ?_
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ HasColimitsOfShape (Discrete J) C
[PROOFSTEP]
apply hasColimitsOfShape_discrete _ _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ HasColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) C
[PROOFSTEP]
apply hasColimitsOfShape_discrete _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ PreservesColimitsOfShape (Discrete J) G
[PROOFSTEP]
apply PreservesFiniteCoproducts.preserves _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type w
inst✝⁵ : SmallCategory J✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this✝ : Fintype J
this : Fintype ((p : J × J) × (p.fst ⟶ p.snd))
⊢ PreservesColimitsOfShape (Discrete ((p : J × J) × (p.fst ⟶ p.snd))) G
[PROOFSTEP]
apply PreservesFiniteCoproducts.preserves _
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
⊢ PreservesFiniteColimits G
[PROOFSTEP]
haveI : HasFiniteColimits C := hasFiniteColimits_of_hasInitial_and_pushouts
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this : HasFiniteColimits C
⊢ PreservesFiniteColimits G
[PROOFSTEP]
haveI : PreservesColimitsOfShape (Discrete WalkingPair) G := preservesBinaryCoproductsOfPreservesInitialAndPushouts G
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝ : HasFiniteColimits C
this : PreservesColimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteColimits G
[PROOFSTEP]
haveI : PreservesColimitsOfShape (WalkingParallelPair) G :=
  (preservesCoequalizersOfPreservesPushoutsAndBinaryCoproducts G)
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteColimits G
[PROOFSTEP]
refine @preservesFiniteColimitsOfPreservesCoequalizersAndFiniteCoproducts _ _ _ _ _ _ G _ ?_
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteCoproducts G
[PROOFSTEP]
apply PreservesFiniteCoproducts.mk
[GOAL]
case preserves
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
inst✝⁵ : SmallCategory J
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ (J : Type) → [inst : Fintype J] → PreservesColimitsOfShape (Discrete J) G
[PROOFSTEP]
apply preservesFiniteCoproductsOfPreservesBinaryAndInitial G