[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ (e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g
[PROOFSTEP]
rw [Category.assoc, equalizer.condition]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
    prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g
[PROOFSTEP]
rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ NatTrans.app (BinaryFan.mk (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right)).π
        { as := WalkingPair.left } ≫
      f =
    NatTrans.app (BinaryFan.mk (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right)).π
        { as := WalkingPair.right } ≫
      g
[PROOFSTEP]
exact PullbackCone.condition _
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        e ≫ π₁ =
      PullbackCone.fst s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        e ≫ π₂ =
      PullbackCone.snd s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ m =
    (fun s =>
        equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
          (_ :
            prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
              prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
      s
[PROOFSTEP]
ext
[GOAL]
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    ((fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst
[PROOFSTEP]
dsimp
[GOAL]
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ (m ≫ equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g)) ≫ prod.fst =
    (equalizer.lift (prod.lift (PullbackCone.fst s) (PullbackCone.snd s))
          (_ :
            prod.lift (PullbackCone.fst s) (PullbackCone.snd s) ≫ prod.fst ≫ f =
              prod.lift (PullbackCone.fst s) (PullbackCone.snd s) ≫ prod.snd ≫ g) ≫
        equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g)) ≫
      prod.fst
[PROOFSTEP]
simpa using h₁
[GOAL]
case h.h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
    ((fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.snd
[PROOFSTEP]
simpa using h₂
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, coequalizer.condition]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
    (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)
[PROOFSTEP]
rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ f ≫
      NatTrans.app (BinaryCofan.mk (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)).ι
        { as := WalkingPair.left } =
    g ≫
      NatTrans.app (BinaryCofan.mk (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)).ι
        { as := WalkingPair.right }
[PROOFSTEP]
exact PushoutCocone.condition _
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ ∀ (s : PushoutCocone f g),
    (ι₁ ≫ c) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s =
      PushoutCocone.inl s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ ∀ (s : PushoutCocone f g),
    (ι₂ ≫ c) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s =
      PushoutCocone.inr s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = PushoutCocone.inl s
h₂ : (ι₂ ≫ c) ≫ m = PushoutCocone.inr s
⊢ m =
    (fun s =>
        coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
          (_ :
            (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
              (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
      s
[PROOFSTEP]
ext
[GOAL]
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = PushoutCocone.inl s
h₂ : (ι₂ ≫ c) ≫ m = PushoutCocone.inr s
⊢ coprod.inl ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inl ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s
[PROOFSTEP]
simpa using h₁
[GOAL]
case h.h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = PushoutCocone.inl s
h₂ : (ι₂ ≫ c) ≫ m = PushoutCocone.inr s
⊢ coprod.inr ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inr ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s
[PROOFSTEP]
simpa using h₂
