[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inl (PullbackCone.op (cone p)) ≫ (Iso.refl (PullbackCone.op (cone p)).pt).hom =
    PushoutCocone.inl (cocone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inr (PullbackCone.op (cone p)) ≫ (Iso.refl (PullbackCone.op (cone p)).pt).hom =
    PushoutCocone.inr (cocone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.fst (PushoutCocone.op (cocone p)) =
    (Iso.refl (PushoutCocone.op (cocone p)).pt).hom ≫ PullbackCone.fst (cone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.snd (PushoutCocone.op (cocone p)) =
    (Iso.refl (PushoutCocone.op (cocone p)).pt).hom ≫ PullbackCone.snd (cone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inl (PullbackCone.unop (cone p)) ≫ (Iso.refl (PullbackCone.unop (cone p)).pt).hom =
    PushoutCocone.inl (cocone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inr (PullbackCone.unop (cone p)) ≫ (Iso.refl (PullbackCone.unop (cone p)).pt).hom =
    PushoutCocone.inr (cocone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.fst (PushoutCocone.unop (cocone p)) =
    (Iso.refl (PushoutCocone.unop (cocone p)).pt).hom ≫ PullbackCone.fst (cone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.snd (PushoutCocone.unop (cocone p)) =
    (Iso.refl (PushoutCocone.unop (cocone p)).pt).hom ≫ PullbackCone.snd (cone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ PullbackCone.fst c =
    (Iso.refl c.pt).hom ≫
      PullbackCone.fst
        (PullbackCone.mk (PullbackCone.fst c) (PullbackCone.snd c)
          (_ : PullbackCone.fst c ≫ f = PullbackCone.snd c ≫ g))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ PullbackCone.snd c =
    (Iso.refl c.pt).hom ≫
      PullbackCone.snd
        (PullbackCone.mk (PullbackCone.fst c) (PullbackCone.snd c)
          (_ : PullbackCone.fst c ≫ f = PullbackCone.snd c ≫ g))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app c.π j =
      (Iso.refl c.pt).hom ≫
        NatTrans.app (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ NatTrans.app c.π { as := WalkingPair.left } =
    (Iso.refl c.pt).hom ≫
      NatTrans.app (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π
        { as := WalkingPair.left }
[PROOFSTEP]
dsimp
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ BinaryFan.fst c = 𝟙 c.pt ≫ BinaryFan.fst c
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ NatTrans.app c.π { as := WalkingPair.right } =
    (Iso.refl c.pt).hom ≫
      NatTrans.app (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π
        { as := WalkingPair.right }
[PROOFSTEP]
dsimp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ BinaryFan.snd c = 𝟙 c.pt ≫ BinaryFan.snd c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPullback prod.fst prod.snd 0 0
[PROOFSTEP]
convert @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).hom ≫ pullback.fst = fst
[PROOFSTEP]
dsimp [isoPullback, cone, CommSq.cone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd (_ : fst ≫ f = snd ≫ g), isLimit := isLimit h }).inv ≫
      pullback.fst =
    fst
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).hom ≫ pullback.snd = snd
[PROOFSTEP]
dsimp [isoPullback, cone, CommSq.cone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd (_ : fst ≫ f = snd ≫ g), isLimit := isLimit h }).inv ≫
      pullback.snd =
    snd
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).inv ≫ fst = pullback.fst
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).inv ≫ snd = pullback.snd
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ IsLimit (CommSq.cone sq)
[PROOFSTEP]
refine' PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by aesop_cat) (fun s => _) (by aesop_cat)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g), (fun s => PullbackCone.fst s ≫ inv fst) s ≫ fst = PullbackCone.fst s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P),
    m ≫ fst = PullbackCone.fst s → m ≫ snd = PullbackCone.snd s → m = (fun s => PullbackCone.fst s ≫ inv fst) s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun s => PullbackCone.fst s ≫ inv fst) s ≫ snd = PullbackCone.snd s
[PROOFSTEP]
simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : PushoutCocone f g
h : IsColimit c
⊢ PushoutCocone.inl c ≫ (Iso.refl c.pt).hom =
    PushoutCocone.inl
      (PushoutCocone.mk (PushoutCocone.inl c) (PushoutCocone.inr c)
        (_ : f ≫ PushoutCocone.inl c = g ≫ PushoutCocone.inr c))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : PushoutCocone f g
h : IsColimit c
⊢ PushoutCocone.inr c ≫ (Iso.refl c.pt).hom =
    PushoutCocone.inr
      (PushoutCocone.mk (PushoutCocone.inl c) (PushoutCocone.inr c)
        (_ : f ≫ PushoutCocone.inl c = g ≫ PushoutCocone.inr c))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app c.ι j ≫ (Iso.refl c.pt).hom =
      NatTrans.app (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ NatTrans.app c.ι { as := WalkingPair.left } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι
      { as := WalkingPair.left }
[PROOFSTEP]
dsimp
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ BinaryCofan.inl c ≫ 𝟙 c.pt = BinaryCofan.inl c
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ NatTrans.app c.ι { as := WalkingPair.right } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι
      { as := WalkingPair.right }
[PROOFSTEP]
dsimp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ BinaryCofan.inr c ≫ 𝟙 c.pt = BinaryCofan.inr c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPushout 0 0 coprod.inl coprod.inr
[PROOFSTEP]
convert @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl ≫ (isoPushout h).inv = inl
[PROOFSTEP]
dsimp [isoPushout, cocone, CommSq.cocone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr (_ : f ≫ inl = g ≫ inr), isColimit := isColimit h }).hom =
    inl
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫ (isoPushout h).inv = inr
[PROOFSTEP]
dsimp [isoPushout, cocone, CommSq.cocone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr (_ : f ≫ inl = g ≫ inr), isColimit := isColimit h }).hom =
    inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ inl ≫ (isoPushout h).hom = pushout.inl
[PROOFSTEP]
simp [← Iso.eq_comp_inv]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ inr ≫ (isoPushout h).hom = pushout.inr
[PROOFSTEP]
simp [← Iso.eq_comp_inv]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 𝟙 X = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ ∀ (j : WalkingCospan),
    (fun s => 0) s ≫ NatTrans.app (PullbackCone.mk 0 0 (_ : 0 ≫ 𝟙 X = 0 ≫ 0)).π j = NatTrans.app s.π j
[PROOFSTEP]
simpa using @PullbackCone.equalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simpa using (PullbackCone.condition s).symm)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ 0 ≫ PullbackCone.fst s = 𝟙 s.pt ≫ PullbackCone.fst s
[PROOFSTEP]
simpa using (PullbackCone.condition s).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 (𝟙 X) 0 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.fst = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.snd = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback b.fst b.snd 0 0
[PROOFSTEP]
convert IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback b.inl 0 b.snd 0
[PROOFSTEP]
refine' of_right _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ b.inl ≫ b.snd = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback (b.inl ≫ b.fst) 0 0 (0 ≫ 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback b.inr 0 b.fst 0
[PROOFSTEP]
apply flip
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback 0 b.inr 0 b.fst
[PROOFSTEP]
refine' of_bot _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ 0 ≫ 0 = b.inr ≫ b.fst
[PROOFSTEP]
simp
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback 0 (b.inr ≫ b.snd) (0 ≫ 0) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback 0 0 b.inl b.inr
[PROOFSTEP]
refine' IsPullback.of_right _ (by simp) (IsPullback.inl_snd' h).flip
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ 0 ≫ b.inl = 0 ≫ b.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι j ≫ (fun s => 0) s = NatTrans.app s.ι j
[PROOFSTEP]
have c := @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simp) (by simpa using PushoutCocone.condition s)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inl s ≫ 0 = PushoutCocone.inl s ≫ 𝟙 s.pt
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt
[PROOFSTEP]
simpa using PushoutCocone.condition s
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), NatTrans.app s.ι j ≫ 0 = NatTrans.app s.ι j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι j ≫ (fun s => 0) s = NatTrans.app s.ι j
[PROOFSTEP]
dsimp at c
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), NatTrans.app s.ι j ≫ 0 = NatTrans.app s.ι j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι j ≫ (fun s => 0) s = NatTrans.app s.ι j
[PROOFSTEP]
simpa using c
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 0 (𝟙 X) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 𝟙 X ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inl
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout 0 0 b.inl b.inr
[PROOFSTEP]
convert IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout b.inl 0 b.snd 0
[PROOFSTEP]
apply flip
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout 0 b.inl 0 b.snd
[PROOFSTEP]
refine' of_right _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ 0 ≫ 0 = b.inl ≫ b.snd
[PROOFSTEP]
simp
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout b.inr 0 b.fst 0
[PROOFSTEP]
refine' of_bot _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ b.inr ≫ b.fst = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout 0 (0 ≫ 0) (b.inl ≫ b.fst) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout b.fst b.snd 0 0
[PROOFSTEP]
refine' IsPushout.of_right _ (by simp) (IsPushout.inl_snd' h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ b.fst ≫ 0 = b.snd ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout (b.inl ≫ b.fst) 0 0 (0 ≫ 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit (CommSq.cocone sq)
[PROOFSTEP]
refine' PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => _) (by aesop_cat) (by aesop_cat)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g), inr ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inr s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt),
    inl ≫ m = PushoutCocone.inl s → inr ≫ m = PushoutCocone.inr s → m = (fun s => inv inr ≫ PushoutCocone.inr s) s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inl s
[PROOFSTEP]
simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ IsLimit (Fork.ofι f (_ : f ≫ g = f ≫ g'))
[PROOFSTEP]
fapply Fork.IsLimit.mk
[GOAL]
case lift
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ (s : Fork g g') → s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
[PROOFSTEP]
exact fun s => H.isLimit.lift (PullbackCone.mk s.ι s.ι s.condition)
[GOAL]
case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'),
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
        Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) =
      Fork.ι s
[PROOFSTEP]
exact fun s => H.isLimit.fac _ WalkingCospan.left
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt),
    m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s →
      m = IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g'))
[PROOFSTEP]
intro s m e
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ m = IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g'))
[PROOFSTEP]
apply PullbackCone.IsLimit.hom_ext H.isLimit
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ m ≫ PullbackCone.fst (cone H) =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.fst (cone H)
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ m ≫ PullbackCone.snd (cone H) =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.snd (cone H)
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ Fork.ι s =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.fst (cone H)
[PROOFSTEP]
symm
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ Fork.ι s =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.snd (cone H)
[PROOFSTEP]
symm
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.fst (cone H) =
    Fork.ι s
[PROOFSTEP]
exact H.isLimit.fac _ _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.snd (cone H) =
    Fork.ι s
[PROOFSTEP]
exact H.isLimit.fac _ _
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ IsColimit (Cofork.ofπ g (_ : f ≫ g = f' ≫ g))
[PROOFSTEP]
fapply Cofork.IsColimit.mk
[GOAL]
case desc
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ (s : Cofork f f') → (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
[PROOFSTEP]
exact fun s => H.isColimit.desc (PushoutCocone.mk s.π s.π s.condition)
[GOAL]
case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'),
    Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫
        IsColimit.desc (isColimit H)
          (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s)) =
      Cofork.π s
[PROOFSTEP]
exact fun s => H.isColimit.fac _ WalkingSpan.left
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt),
    Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s →
      m =
        IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
intro s m e
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ m = IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
apply PushoutCocone.IsColimit.hom_ext H.isColimit
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inl (cocone H) ≫ m =
    PushoutCocone.inl (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inr (cocone H) ≫ m =
    PushoutCocone.inr (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ Cofork.π s =
    PushoutCocone.inl (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
symm
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ Cofork.π s =
    PushoutCocone.inr (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
symm
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inl (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s)) =
    Cofork.π s
[PROOFSTEP]
exact H.isColimit.fac _ _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inr (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s)) =
    Cofork.π s
[PROOFSTEP]
exact H.isColimit.fac _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq biprod.fst biprod.snd 0 0
[PROOFSTEP]
convert of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq 0 0 biprod.inl biprod.inr
[PROOFSTEP]
convert of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
[PROOFSTEP]
refine'
  IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext _ _ _) (isLimitOfPreserves F s.isLimit))
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt ≅
    (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).pt
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ NatTrans.app ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π
      WalkingCospan.left =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      NatTrans.app (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).π WalkingCospan.left
[PROOFSTEP]
simp
[GOAL]
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ NatTrans.app ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π
      WalkingCospan.right =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      NatTrans.app (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).π WalkingCospan.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
[PROOFSTEP]
refine'
  IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext _ _ _) (isColimitOfPreserves F s.isColimit))
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt ≅
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).pt
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ NatTrans.app ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι
        WalkingCospan.left ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt).hom =
    NatTrans.app (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι WalkingCospan.left
[PROOFSTEP]
simp
[GOAL]
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ NatTrans.app ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι
        WalkingCospan.right ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt).hom =
    NatTrans.app (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι WalkingCospan.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPullback f g h i
[PROOFSTEP]
refine' ⟨⟨e⟩, ⟨isLimitOfReflects F <| _⟩⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsLimit (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))
[PROOFSTEP]
refine' (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext _ _ _)).symm H.isLimit
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).pt ≅
    (cone H).pt
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ NatTrans.app
      ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π
      WalkingCospan.left =
    ?refine'_1.hom ≫ NatTrans.app (cone H).π WalkingCospan.left
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ NatTrans.app
      ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π
      WalkingCospan.right =
    ?refine'_1.hom ≫ NatTrans.app (cone H).π WalkingCospan.right
[PROOFSTEP]
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _).symm,
  (Category.comp_id _).trans (Category.id_comp _).symm]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsLimit (cospan h i) F
inst✝ : Faithful F
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)
[PROOFSTEP]
simpa only [F.map_comp] using H.w
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPushout f g h i
[PROOFSTEP]
refine' ⟨⟨e⟩, ⟨isColimitOfReflects F <| _⟩⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))
[PROOFSTEP]
refine' (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext _ _ _)).symm H.isColimit
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))).pt ≅
    (cocone H).pt
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ NatTrans.app
        ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))).ι
        WalkingCospan.left ≫
      ?refine'_1.hom =
    NatTrans.app (cocone H).ι WalkingCospan.left
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ NatTrans.app
        ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))).ι
        WalkingCospan.right ≫
      ?refine'_1.hom =
    NatTrans.app (cocone H).ι WalkingCospan.right
[PROOFSTEP]
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _), (Category.comp_id _).trans (Category.id_comp _)]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsColimit (span f g) F
inst✝ : Faithful F
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)
[PROOFSTEP]
simpa only [F.map_comp] using H.w


[GOAL]
R : Type u_1
inst✝⁸ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁷ : Category.{?u.28793, u_2} C
inst✝⁶ : Category.{?u.28797, u_3} D
inst✝⁵ : Preadditive C
inst✝⁴ : Linear R C
inst✝³ : Preadditive D
inst✝² : Linear R D
e : C ≌ D
inst✝¹ : Functor.Additive e.functor
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.inverse.map (f • r) = f • e.inverse.map r
[PROOFSTEP]
apply e.functor.map_injective
[GOAL]
case a
R : Type u_1
inst✝⁸ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁷ : Category.{?u.28793, u_2} C
inst✝⁶ : Category.{?u.28797, u_3} D
inst✝⁵ : Preadditive C
inst✝⁴ : Linear R C
inst✝³ : Preadditive D
inst✝² : Linear R D
e : C ≌ D
inst✝¹ : Functor.Additive e.functor
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.functor.map (e.inverse.map (f • r)) = e.functor.map (f • e.inverse.map r)
[PROOFSTEP]
simp


[GOAL]
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ : c ⟶ c
⊢ (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ
[PROOFSTEP]
simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ
[PROOFSTEP]
simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ₁ γ₂ : c ⟶ c
⊢ Equiv.toFun
      { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f,
        left_inv := (_ : ∀ (γ : c ⟶ c), (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ),
        right_inv := (_ : ∀ (δ : d ⟶ d), (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ) }
      (γ₁ * γ₂) =
    Equiv.toFun
        { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f,
          left_inv := (_ : ∀ (γ : c ⟶ c), (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ),
          right_inv := (_ : ∀ (δ : d ⟶ d), (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ) }
        γ₁ *
      Equiv.toFun
        { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f,
          left_inv := (_ : ∀ (γ : c ⟶ c), (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ),
          right_inv := (_ : ∀ (δ : d ⟶ d), (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ) }
        γ₂
[PROOFSTEP]
simp only [vertexGroup_mul, inv_eq_inv, Category.assoc, IsIso.hom_inv_id_assoc]


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
j : Discrete α
⊢ j ∈ {j}
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ m =
    (fun s =>
        colimit.desc (liftToFinset F) { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x })
      s
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ ∀ (j : Finset (Discrete α)),
    colimit.ι (liftToFinset F) j ≫ m =
      colimit.ι (liftToFinset F) j ≫
        (fun s =>
            colimit.desc (liftToFinset F)
              { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x })
          s
[PROOFSTEP]
rintro t
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
⊢ colimit.ι (liftToFinset F) t ≫ m =
    colimit.ι (liftToFinset F) t ≫
      (fun s =>
          colimit.desc (liftToFinset F)
            { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x })
        s
[PROOFSTEP]
dsimp [liftToFinset]
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
⊢ colimit.ι
        (Functor.mk
          { obj := fun s => ∐ fun x => F.obj ↑x,
            map := fun {x Y} h =>
              Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
        t ≫
      m =
    colimit.ι
        (Functor.mk
          { obj := fun s => ∐ fun x => F.obj ↑x,
            map := fun {x Y} h =>
              Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
        t ≫
      colimit.desc
        (Functor.mk
          { obj := fun s => ∐ fun x => F.obj ↑x,
            map := fun {x Y} h =>
              Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
        { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x }
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w.w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
⊢ ∀ (j : Discrete { x // x ∈ t }),
    colimit.ι (Discrete.functor fun x => F.obj ↑x) j ≫
        colimit.ι
            (Functor.mk
              { obj := fun s => ∐ fun x => F.obj ↑x,
                map := fun {x Y} h =>
                  Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
            t ≫
          m =
      colimit.ι (Discrete.functor fun x => F.obj ↑x) j ≫
        colimit.ι
            (Functor.mk
              { obj := fun s => ∐ fun x => F.obj ↑x,
                map := fun {x Y} h =>
                  Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
            t ≫
          colimit.desc
            (Functor.mk
              { obj := fun s => ∐ fun x => F.obj ↑x,
                map := fun {x Y} h =>
                  Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
            { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x }
[PROOFSTEP]
rintro ⟨⟨j, hj⟩⟩
[GOAL]
case w.w.mk.mk
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        m =
    colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        colimit.desc
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x }
[PROOFSTEP]
convert h j using 1
[GOAL]
case h.e'_2.h
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x => F.obj ↑x).obj { as := { val := j, property := hj } } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        m =
    NatTrans.app
        { pt := colimit (liftToFinset F),
            ι :=
              Discrete.natTrans fun j =>
                Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.ι
        j ≫
      m
[PROOFSTEP]
simp [← colimit.w (liftToFinset F) ⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩]
[GOAL]
case h.e'_2.h
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x => F.obj ↑x).obj { as := { val := j, property := hj } } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        m =
    Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : ↑{ val := j, property := (_ : j ∈ {j}) } ∈ t) } ≫
      colimit.ι (liftToFinset F) t ≫ m
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x => F.obj ↑x).obj { as := { val := j, property := hj } } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        colimit.desc
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x } =
    NatTrans.app s.ι j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α✝ : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C
[PROOFSTEP]
classical exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α✝ : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C
[PROOFSTEP]
exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩


[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
A✝ B✝ : C
f : A✝ ⟶ B✝
i : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 A✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
A✝ B✝ : C
f : A✝ ⟶ B✝
i : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 B✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : ReflectsIsomorphisms F
inst✝ : ReflectsIsomorphisms G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (G.map (F.map f))
⊢ IsIso f
[PROOFSTEP]
haveI := isIso_of_reflects_iso (F.map f) G
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : ReflectsIsomorphisms F
inst✝ : ReflectsIsomorphisms G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (G.map (F.map f))
this : IsIso (F.map f)
⊢ IsIso f
[PROOFSTEP]
exact isIso_of_reflects_iso f F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : ReflectsMonomorphisms F
inst✝ : ReflectsEpimorphisms F
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
⊢ IsIso f
[PROOFSTEP]
haveI : Epi f := epi_of_epi_map F inferInstance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : ReflectsMonomorphisms F
inst✝ : ReflectsEpimorphisms F
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
this : Epi f
⊢ IsIso f
[PROOFSTEP]
haveI : Mono f := mono_of_mono_map F inferInstance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : ReflectsMonomorphisms F
inst✝ : ReflectsEpimorphisms F
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
this✝ : Epi f
this : Mono f
⊢ IsIso f
[PROOFSTEP]
exact isIso_of_mono_of_epi f


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
r : ℕ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.rightComp X g).map_nsmul f r
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
f : X ⟶ Y
r : ℕ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.leftComp Z f).map_nsmul g r
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
r : ℤ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.rightComp X g).map_zsmul f r
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
f : X ⟶ Y
r : ℤ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.leftComp Z f).map_zsmul g r
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X : C
⊢ Module R (End X)
[PROOFSTEP]
dsimp [End]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X : C
⊢ Module R (X ⟶ X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (x y : Y ⟶ Z), (fun g => f ≫ g) (x + y) = (fun g => f ≫ g) x + (fun g => f ≫ g) y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (r : R) (x : Y ⟶ Z),
    AddHom.toFun { toFun := fun g => f ≫ g, map_add' := (_ : ∀ (a a_1 : Y ⟶ Z), f ≫ (a + a_1) = f ≫ a + f ≫ a_1) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := fun g => f ≫ g, map_add' := (_ : ∀ (a a_1 : Y ⟶ Z), f ≫ (a + a_1) = f ≫ a + f ≫ a_1) } x
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (x y : X ⟶ Y), (fun f => f ≫ g) (x + y) = (fun f => f ≫ g) x + (fun f => f ≫ g) y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (r : R) (x : X ⟶ Y),
    AddHom.toFun { toFun := fun f => f ≫ g, map_add' := (_ : ∀ (a a_1 : X ⟶ Y), (a + a_1) ≫ g = a ≫ g + a_1 ≫ g) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := fun f => f ≫ g, map_add' := (_ : ∀ (a a_1 : X ⟶ Y), (a + a_1) ≫ g = a ≫ g + a_1 ≫ g) } x
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ g = g'
[PROOFSTEP]
rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • g = r • g'
⊢ g = g'
[PROOFSTEP]
simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ g = g'
[PROOFSTEP]
rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : r • g = r • g'
⊢ g = g'
[PROOFSTEP]
simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H
[GOAL]
C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{?u.35990, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
src✝ : (X ⟶ W) →ₗ[k] Y ⟶ Z := comp (rightComp k Y f₂.hom) (leftComp k W f₁.symm.hom)
x : X ⟶ W
⊢ ↑(comp (leftComp k W f₁.hom) (rightComp k Y f₂.symm.hom))
      (AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : k) (x : X ⟶ W),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id k) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
simp only [Iso.symm_hom, LinearMap.toFun_eq_coe, LinearMap.coe_comp, Function.comp_apply, leftComp_apply,
  rightComp_apply, Category.assoc, Iso.hom_inv_id, Category.comp_id, Iso.hom_inv_id_assoc]
[GOAL]
C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{?u.35990, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
src✝ : (X ⟶ W) →ₗ[k] Y ⟶ Z := comp (rightComp k Y f₂.hom) (leftComp k W f₁.symm.hom)
x : Y ⟶ Z
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : k) (x : X ⟶ W),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id k) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(comp (leftComp k W f₁.hom) (rightComp k Y f₂.symm.hom)) x) =
    x
[PROOFSTEP]
simp only [Iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, rightComp_apply, leftComp_apply,
  LinearMap.toFun_eq_coe, Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (x y : X ⟶ Y), (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
x✝ y✝ : X ⟶ Y
⊢ (fun f => leftComp S Z f) (x✝ + y✝) = (fun f => leftComp S Z f) x✝ + (fun f => leftComp S Z f) y✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
x✝¹ y✝ : X ⟶ Y
x✝ : Y ⟶ Z
⊢ ↑((fun f => leftComp S Z f) (x✝¹ + y✝)) x✝ = ↑((fun f => leftComp S Z f) x✝¹ + (fun f => leftComp S Z f) y✝) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (r : S) (x : X ⟶ Y),
    AddHom.toFun
        { toFun := fun f => leftComp S Z f,
          map_add' :=
            (_ :
              ∀ (x y : X ⟶ Y),
                (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
        (r • x) =
      ↑(RingHom.id S) r •
        AddHom.toFun
          { toFun := fun f => leftComp S Z f,
            map_add' :=
              (_ :
                ∀ (x y : X ⟶ Y),
                  (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
          x
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
r✝ : S
x✝ : X ⟶ Y
⊢ AddHom.toFun
      { toFun := fun f => leftComp S Z f,
        map_add' :=
          (_ :
            ∀ (x y : X ⟶ Y),
              (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
      (r✝ • x✝) =
    ↑(RingHom.id S) r✝ •
      AddHom.toFun
        { toFun := fun f => leftComp S Z f,
          map_add' :=
            (_ :
              ∀ (x y : X ⟶ Y),
                (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
r✝ : S
x✝¹ : X ⟶ Y
x✝ : Y ⟶ Z
⊢ ↑(AddHom.toFun
          { toFun := fun f => leftComp S Z f,
            map_add' :=
              (_ :
                ∀ (x y : X ⟶ Y),
                  (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
          (r✝ • x✝¹))
      x✝ =
    ↑(↑(RingHom.id S) r✝ •
          AddHom.toFun
            { toFun := fun f => leftComp S Z f,
              map_add' :=
                (_ :
                  ∀ (x y : X ⟶ Y),
                    (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
            x✝¹)
      x✝
[PROOFSTEP]
simp


[GOAL]
V✝ : Type u
inst✝² : Quiver V✝
V : Type ?u.991
inst✝¹ : Quiver V
inst✝ : Nonempty V
⊢ Nonempty (FreeGroupoid V)
[PROOFSTEP]
inhabit V
[GOAL]
V✝ : Type u
inst✝² : Quiver V✝
V : Type ?u.991
inst✝¹ : Quiver V
inst✝ : Nonempty V
inhabited_h : Inhabited V
⊢ Nonempty (FreeGroupoid V)
[PROOFSTEP]
exact ⟨⟨@default V _⟩⟩
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p q : X ⟶ Y
⊢ Quotient.CompClosure redStep p q → Quotient.CompClosure redStep (Quiver.Path.reverse p) (Quiver.Path.reverse q)
[PROOFSTEP]
rintro ⟨XW, pp, qq, WY, _, Z, f⟩
[GOAL]
case intro.step
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY))
    (Quiver.Path.reverse (XW ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ WY))
[PROOFSTEP]
have :
  Quotient.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
    (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) :=
  by
  constructor
  constructor
[GOAL]
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse WY ≫ 𝟙 (Paths.of.obj X✝) ≫ Quiver.Path.reverse XW)
    (Quiver.Path.reverse WY ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse XW)
[PROOFSTEP]
constructor
[GOAL]
case h
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
⊢ redStep (𝟙 (Paths.of.obj X✝)) (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
[PROOFSTEP]
constructor
[GOAL]
case intro.step
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
this :
  Quotient.CompClosure redStep (Quiver.Path.reverse WY ≫ 𝟙 (Paths.of.obj X✝) ≫ Quiver.Path.reverse XW)
    (Quiver.Path.reverse WY ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse XW)
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY))
    (Quiver.Path.reverse (XW ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ WY))
[PROOFSTEP]
simpa only [CategoryStruct.comp, CategoryStruct.id, Quiver.Path.reverse, Quiver.Path.nil_comp, Quiver.Path.reverse_comp,
  Quiver.reverse_reverse, Quiver.Path.reverse_toPath, Quiver.Path.comp_assoc] using this
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (p ≫ Quiver.Path.reverse p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 X)
[PROOFSTEP]
apply Quot.EqvGen_sound
[GOAL]
case H
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ EqvGen (Quotient.CompClosure redStep) (p ≫ Quiver.Path.reverse p) (𝟙 X)
[PROOFSTEP]
induction' p with a b q f ih
[GOAL]
case H.nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.nil ≫ Quiver.Path.reverse Quiver.Path.nil) (𝟙 X)
[PROOFSTEP]
apply EqvGen.refl
[GOAL]
case H.cons
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.cons q f ≫ Quiver.Path.reverse (Quiver.Path.cons q f)) (𝟙 X)
[PROOFSTEP]
simp only [Quiver.Path.reverse]
[GOAL]
case H.cons
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q)) (𝟙 X)
[PROOFSTEP]
fapply EqvGen.trans
[GOAL]
case H.cons.y
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ X ⟶ X
[PROOFSTEP]
exact q ≫ Quiver.Path.reverse q
[GOAL]
case H.cons.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
    (q ≫ Quiver.Path.reverse q)
[PROOFSTEP]
apply EqvGen.symm
[GOAL]
case H.cons.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
apply EqvGen.rel
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
have :
  Quotient.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q) :=
  by
  apply Quotient.CompClosure.intro
  apply redStep.step
[GOAL]
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
[PROOFSTEP]
apply Quotient.CompClosure.intro
[GOAL]
case h
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ redStep (𝟙 a) (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
[PROOFSTEP]
apply redStep.step
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
simp only [Category.assoc, Category.id_comp] at this ⊢
  -- Porting note : `simp` cannot see how `Quiver.Path.comp_assoc` is relevant, so change to
        -- category notation
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
change
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
[PROOFSTEP]
simp only [← Category.assoc] at this ⊢
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (((q ≫ Quiver.Hom.toPath f) ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    ((Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
[PROOFSTEP]
exact this
[GOAL]
case H.cons.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
[PROOFSTEP]
exact ih
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
[PROOFSTEP]
nth_rw 2 [← Quiver.Path.reverse_reverse p]
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ Quiver.Path.reverse (Quiver.Path.reverse p)) =
    Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
[PROOFSTEP]
apply congr_comp_reverse
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ ∀ (x y : Paths (Quiver.Symmetrify V)) (f₁ f₂ : x ⟶ y),
    redStep f₁ f₂ → (Paths.lift (Quiver.Symmetrify.lift φ)).map f₁ = (Paths.lift (Quiver.Symmetrify.lift φ)).map f₂
[PROOFSTEP]
rintro _ _ _ _
  ⟨X, Y, f⟩
      -- Porting note: `simp` does not work, so manually `rewrite`
[GOAL]
case step
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
X✝ Y✝ : Paths (Quiver.Symmetrify V)
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ (Paths.lift (Quiver.Symmetrify.lift φ)).map (𝟙 (Paths.of.obj X)) =
    (Paths.lift (Quiver.Symmetrify.lift φ)).map (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
[PROOFSTEP]
erw [Paths.lift_nil, Paths.lift_cons, Quiver.Path.comp_nil, Paths.lift_toPath, Quiver.Symmetrify.lift_reverse]
[GOAL]
case step
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
X✝ Y✝ : Paths (Quiver.Symmetrify V)
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Quiver.Symmetrify.lift φ).obj (Paths.of.obj X)) =
    (Quiver.Symmetrify.lift φ).map f ≫ Quiver.reverse ((Quiver.Symmetrify.lift φ).map f)
[PROOFSTEP]
symm
[GOAL]
case step
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
X✝ Y✝ : Paths (Quiver.Symmetrify V)
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ (Quiver.Symmetrify.lift φ).map f ≫ Quiver.reverse ((Quiver.Symmetrify.lift φ).map f) =
    𝟙 ((Quiver.Symmetrify.lift φ).obj (Paths.of.obj X))
[PROOFSTEP]
apply Groupoid.comp_inv
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ of V ⋙q (lift φ).toPrefunctor = φ
[PROOFSTEP]
rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ lift φ).toPrefunctor) = φ
[PROOFSTEP]
dsimp [lift]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q
      (Paths.of ⋙q
        (Quotient.functor redStep ⋙
            Quotient.lift redStep (Paths.lift (Quiver.Symmetrify.lift φ))
              (_ :
                ∀ (x y : Paths (Quiver.Symmetrify V)) (f₁ f₂ : x ⟶ y),
                  redStep f₁ f₂ →
                    (Paths.lift (Quiver.Symmetrify.lift φ)).map f₁ =
                      (Paths.lift (Quiver.Symmetrify.lift φ)).map f₂)).toPrefunctor) =
    φ
[PROOFSTEP]
rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ
[PROOFSTEP]
apply Quotient.lift_unique
[GOAL]
case hΦ
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Quotient.functor redStep ⋙ Φ = Paths.lift (Quiver.Symmetrify.lift φ)
[PROOFSTEP]
apply Paths.lift_unique
[GOAL]
case hΦ.hΦ
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Quiver.Symmetrify.lift φ
[PROOFSTEP]
fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ
[PROOFSTEP]
rw [← Functor.toPrefunctor_comp]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q ((Quotient.functor redStep).toPrefunctor ⋙q Φ.toPrefunctor)) = φ
[PROOFSTEP]
exact hΦ
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ ∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y),
    (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (Quiver.reverse f) =
      Quiver.reverse ((Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
[PROOFSTEP]
rintro X Y f
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (Quiver.reverse f) =
    Quiver.reverse ((Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
[PROOFSTEP]
simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map, inv_eq_inv]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath (Quiver.reverse f))) =
    Quiver.reverse (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
change
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ Φ.map (inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
this :
  Φ.map (CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
⊢ Φ.map (inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_8
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
this :
  Φ.map (CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
⊢ inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f)) =
    CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))
[PROOFSTEP]
simp only [inv_eq_inv]
[GOAL]
case h.e'_3
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
this :
  Φ.map (CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
⊢ inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
simp only [inv_eq_inv]
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ freeGroupoidFunctor (𝟭q V) = 𝟭 (FreeGroupoid V)
[PROOFSTEP]
dsimp only [freeGroupoidFunctor]
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ lift (𝟭q V ⋙q of V) = 𝟭 (FreeGroupoid V)
[PROOFSTEP]
symm
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ 𝟭 (FreeGroupoid V) = lift (𝟭q V ⋙q of V)
[PROOFSTEP]
apply lift_unique
[GOAL]
case hΦ
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ of V ⋙q (𝟭 (FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ freeGroupoidFunctor (φ ⋙q φ') = freeGroupoidFunctor φ ⋙ freeGroupoidFunctor φ'
[PROOFSTEP]
dsimp only [freeGroupoidFunctor]
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')
[PROOFSTEP]
symm
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
[PROOFSTEP]
apply lift_unique
[GOAL]
case hΦ
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
[PROOFSTEP]
rfl