[GOAL]
j : WalkingPair
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) j) = j
[PROOFSTEP]
cases j
[GOAL]
case left
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) left) = left
case right ⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) right) = right
[PROOFSTEP]
repeat rfl
[GOAL]
case left
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) left) = left
case right ⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) right) = right
[PROOFSTEP]
rfl
[GOAL]
case right
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) right) = right
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
j : WalkingPair
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) j) = j
[PROOFSTEP]
cases j
[GOAL]
case left
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) left) = left
case right ⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) right) = right
[PROOFSTEP]
repeat rfl
[GOAL]
case left
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) left) = left
case right ⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) right) = right
[PROOFSTEP]
rfl
[GOAL]
case right
⊢ (fun j => WalkingPair.recOn j right left) ((fun j => WalkingPair.recOn j right left) right) = right
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
j : WalkingPair
⊢ (fun b => Bool.recOn b right left) ((fun j => WalkingPair.recOn j true false) j) = j
[PROOFSTEP]
cases j
[GOAL]
case left
⊢ (fun b => Bool.recOn b right left) ((fun j => WalkingPair.recOn j true false) left) = left
case right ⊢ (fun b => Bool.recOn b right left) ((fun j => WalkingPair.recOn j true false) right) = right
[PROOFSTEP]
repeat rfl
[GOAL]
case left
⊢ (fun b => Bool.recOn b right left) ((fun j => WalkingPair.recOn j true false) left) = left
case right ⊢ (fun b => Bool.recOn b right left) ((fun j => WalkingPair.recOn j true false) right) = right
[PROOFSTEP]
rfl
[GOAL]
case right
⊢ (fun b => Bool.recOn b right left) ((fun j => WalkingPair.recOn j true false) right) = right
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
b : Bool
⊢ (fun j => WalkingPair.recOn j true false) ((fun b => Bool.recOn b right left) b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ (fun j => WalkingPair.recOn j true false) ((fun b => Bool.recOn b right left) false) = false
case true ⊢ (fun j => WalkingPair.recOn j true false) ((fun b => Bool.recOn b right left) true) = true
[PROOFSTEP]
repeat rfl
[GOAL]
case false
⊢ (fun j => WalkingPair.recOn j true false) ((fun b => Bool.recOn b right left) false) = false
case true ⊢ (fun j => WalkingPair.recOn j true false) ((fun b => Bool.recOn b right left) true) = true
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ (fun j => WalkingPair.recOn j true false) ((fun b => Bool.recOn b right left) true) = true
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : Discrete WalkingPair ⥤ C
f : F.obj { as := left } ⟶ G.obj { as := left }
g : F.obj { as := right } ⟶ G.obj { as := right }
x✝² x✝¹ : Discrete WalkingPair
X Y : WalkingPair
x✝ : { as := X } ⟶ { as := Y }
u : { as := X }.as = { as := Y }.as
⊢ F.map { down := { down := u } } ≫ (fun j => Discrete.recOn j fun j => WalkingPair.casesOn j f g) { as := Y } =
    (fun j => Discrete.recOn j fun j => WalkingPair.casesOn j f g) { as := X } ≫ G.map { down := { down := u } }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : Discrete WalkingPair ⥤ C
f✝ : F.obj { as := left } ⟶ G.obj { as := left }
g✝ : F.obj { as := right } ⟶ G.obj { as := right }
f : F.obj { as := left } ≅ G.obj { as := left }
g : F.obj { as := right } ≅ G.obj { as := right }
X✝ Y✝ : Discrete WalkingPair
x✝ : X✝ ⟶ Y✝
u : X✝.as = Y✝.as
⊢ F.map { down := { down := u } } ≫ ((fun j => Discrete.recOn j fun j => WalkingPair.casesOn j f g) Y✝).hom =
    ((fun j => Discrete.recOn j fun j => WalkingPair.casesOn j f g) X✝).hom ≫ G.map { down := { down := u } }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ fst s = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ snd s = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ fst s = f → m ≫ snd s = g → m = lift f g
⊢ ∀ (s_1 : Cone (pair X Y)) (j : Discrete WalkingPair),
    (fun t => lift (fst t) (snd t)) s_1 ≫ NatTrans.app s.π j = NatTrans.app s_1.π j
[PROOFSTEP]
rintro t (rfl | rfl)
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ fst s = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ snd s = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ fst s = f → m ≫ snd s = g → m = lift f g
t : Cone (pair X Y)
⊢ (fun t => lift (fst t) (snd t)) t ≫ NatTrans.app s.π { as := left } = NatTrans.app t.π { as := left }
[PROOFSTEP]
exact hl₁ _ _
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ fst s = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ snd s = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ fst s = f → m ≫ snd s = g → m = lift f g
t : Cone (pair X Y)
⊢ (fun t => lift (fst t) (snd t)) t ≫ NatTrans.app s.π { as := right } = NatTrans.app t.π { as := right }
[PROOFSTEP]
exact hl₂ _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), inl s ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), inr s ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), inl s ≫ m = f → inr s ≫ m = g → m = desc f g
⊢ ∀ (s_1 : Cocone (pair X Y)) (j : Discrete WalkingPair),
    NatTrans.app s.ι j ≫ (fun t => desc (inl t) (inr t)) s_1 = NatTrans.app s_1.ι j
[PROOFSTEP]
rintro t (rfl | rfl)
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), inl s ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), inr s ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), inl s ≫ m = f → inr s ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ NatTrans.app s.ι { as := left } ≫ (fun t => desc (inl t) (inr t)) t = NatTrans.app t.ι { as := left }
[PROOFSTEP]
exact hd₁ _ _
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), inl s ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), inr s ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), inl s ≫ m = f → inr s ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ NatTrans.app s.ι { as := right } ≫ (fun t => desc (inl t) (inr t)) t = NatTrans.app t.ι { as := right }
[PROOFSTEP]
exact hd₂ _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y P : C
π₁ : P ⟶ X
π₂ : P ⟶ Y
x✝ : Discrete WalkingPair
j : WalkingPair
⊢ ((Functor.const (Discrete WalkingPair)).obj P).obj { as := j } ⟶ (pair X Y).obj { as := j }
[PROOFSTEP]
cases j
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
X Y P : C
π₁ : P ⟶ X
π₂ : P ⟶ Y
x✝ : Discrete WalkingPair
⊢ ((Functor.const (Discrete WalkingPair)).obj P).obj { as := left } ⟶ (pair X Y).obj { as := left }
[PROOFSTEP]
simpa
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
X Y P : C
π₁ : P ⟶ X
π₂ : P ⟶ Y
x✝ : Discrete WalkingPair
⊢ ((Functor.const (Discrete WalkingPair)).obj P).obj { as := right } ⟶ (pair X Y).obj { as := right }
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y P : C
ι₁ : X ⟶ P
ι₂ : Y ⟶ P
x✝ : Discrete WalkingPair
j : WalkingPair
⊢ (pair X Y).obj { as := j } ⟶ ((Functor.const (Discrete WalkingPair)).obj P).obj { as := j }
[PROOFSTEP]
cases j
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
X Y P : C
ι₁ : X ⟶ P
ι₂ : Y ⟶ P
x✝ : Discrete WalkingPair
⊢ (pair X Y).obj { as := left } ⟶ ((Functor.const (Discrete WalkingPair)).obj P).obj { as := left }
[PROOFSTEP]
simpa
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
X Y P : C
ι₁ : X ⟶ P
ι₂ : Y ⟶ P
x✝ : Discrete WalkingPair
⊢ (pair X Y).obj { as := right } ⟶ ((Functor.const (Discrete WalkingPair)).obj P).obj { as := right }
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
j : Discrete WalkingPair
⊢ NatTrans.app c.π j = (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π j
[PROOFSTEP]
cases' j with l
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
l : WalkingPair
⊢ NatTrans.app c.π { as := l } =
    (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π { as := l }
[PROOFSTEP]
cases l
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
⊢ NatTrans.app c.π { as := left } =
    (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π { as := left }
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
⊢ NatTrans.app c.π { as := right } =
    (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π { as := right }
[PROOFSTEP]
repeat simp
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
⊢ NatTrans.app c.π { as := left } =
    (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π { as := left }
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
⊢ NatTrans.app c.π { as := right } =
    (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π { as := right }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
⊢ NatTrans.app c.π { as := right } =
    (Iso.refl c.pt).hom ≫ NatTrans.app (BinaryFan.mk (BinaryFan.fst c) (BinaryFan.snd c)).π { as := right }
[PROOFSTEP]
simp
[GOAL]

[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
j : Discrete WalkingPair
⊢ NatTrans.app c.ι j ≫ (Iso.refl c.pt).hom = NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι j
[PROOFSTEP]
cases' j with l
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
l : WalkingPair
⊢ NatTrans.app c.ι { as := l } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι { as := l }
[PROOFSTEP]
cases l
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
⊢ NatTrans.app c.ι { as := left } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι { as := left }
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
⊢ NatTrans.app c.ι { as := right } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι { as := right }
[PROOFSTEP]
repeat simp
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
⊢ NatTrans.app c.ι { as := left } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι { as := left }
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
⊢ NatTrans.app c.ι { as := right } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι { as := right }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
⊢ NatTrans.app c.ι { as := right } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (BinaryCofan.inl c) (BinaryCofan.inr c)).ι { as := right }
[PROOFSTEP]
simp
[GOAL]

[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = CategoryTheory.Limits.BinaryFan.fst s
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = CategoryTheory.Limits.BinaryFan.snd s
uniq :
  ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W),
    m ≫ fst = CategoryTheory.Limits.BinaryFan.fst s → m ≫ snd = CategoryTheory.Limits.BinaryFan.snd s → m = lift s
s : Cone (pair X Y)
j : Discrete WalkingPair
⊢ lift s ≫ NatTrans.app (mk fst snd).π j = NatTrans.app s.π j
[PROOFSTEP]
rcases j with ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = CategoryTheory.Limits.BinaryFan.fst s
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = CategoryTheory.Limits.BinaryFan.snd s
uniq :
  ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W),
    m ≫ fst = CategoryTheory.Limits.BinaryFan.fst s → m ≫ snd = CategoryTheory.Limits.BinaryFan.snd s → m = lift s
s : Cone (pair X Y)
⊢ lift s ≫ NatTrans.app (mk fst snd).π { as := left } = NatTrans.app s.π { as := left }
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = CategoryTheory.Limits.BinaryFan.fst s
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = CategoryTheory.Limits.BinaryFan.snd s
uniq :
  ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W),
    m ≫ fst = CategoryTheory.Limits.BinaryFan.fst s → m ≫ snd = CategoryTheory.Limits.BinaryFan.snd s → m = lift s
s : Cone (pair X Y)
⊢ lift s ≫ NatTrans.app (mk fst snd).π { as := right } = NatTrans.app s.π { as := right }
[PROOFSTEP]
exacts [fac_left s, fac_right s]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = CategoryTheory.Limits.BinaryCofan.inl s
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = CategoryTheory.Limits.BinaryCofan.inr s
uniq :
  ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt),
    inl ≫ m = CategoryTheory.Limits.BinaryCofan.inl s → inr ≫ m = CategoryTheory.Limits.BinaryCofan.inr s → m = desc s
s : Cocone (pair X Y)
j : Discrete WalkingPair
⊢ NatTrans.app (mk inl inr).ι j ≫ desc s = NatTrans.app s.ι j
[PROOFSTEP]
rcases j with ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = CategoryTheory.Limits.BinaryCofan.inl s
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = CategoryTheory.Limits.BinaryCofan.inr s
uniq :
  ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt),
    inl ≫ m = CategoryTheory.Limits.BinaryCofan.inl s → inr ≫ m = CategoryTheory.Limits.BinaryCofan.inr s → m = desc s
s : Cocone (pair X Y)
⊢ NatTrans.app (mk inl inr).ι { as := left } ≫ desc s = NatTrans.app s.ι { as := left }
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = CategoryTheory.Limits.BinaryCofan.inl s
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = CategoryTheory.Limits.BinaryCofan.inr s
uniq :
  ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt),
    inl ≫ m = CategoryTheory.Limits.BinaryCofan.inl s → inr ≫ m = CategoryTheory.Limits.BinaryCofan.inr s → m = desc s
s : Cocone (pair X Y)
⊢ NatTrans.app (mk inl inr).ι { as := right } ≫ desc s = NatTrans.app s.ι { as := right }
[PROOFSTEP]
exacts [fac_left s, fac_right s]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso (fst c)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso (fst c)
[PROOFSTEP]
rintro ⟨H⟩
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
⊢ IsIso (fst c)
[PROOFSTEP]
obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
[GOAL]
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ fst c = 𝟙 X
⊢ IsIso (fst c)
[PROOFSTEP]
exact ⟨⟨l, BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _) (h.hom_ext _ _), hl⟩⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ fst c = 𝟙 X
⊢ (fst c ≫ l) ≫ fst c = 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }) ≫ fst c
[PROOFSTEP]
simpa [hl, -Category.comp_id] using Category.comp_id _
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso (fst c) → Nonempty (IsLimit c)
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
⊢ Nonempty (IsLimit c)
[PROOFSTEP]
exact
  ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by
      simp [← e]⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
T✝ : C
x✝¹ : T✝ ⟶ X
x✝ : T✝ ⟶ Y
⊢ (fun {T} f x => f ≫ inv (fst c)) x✝¹ x✝ ≫ fst c = x✝¹
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
T✝ : C
x✝³ : T✝ ⟶ X
x✝² : T✝ ⟶ Y
x✝¹ : T✝ ⟶ c.pt
e : x✝¹ ≫ fst c = x✝³
x✝ : x✝¹ ≫ snd c = x✝²
⊢ x✝¹ = (fun {T} f x => f ≫ inv (fst c)) x✝³ x✝²
[PROOFSTEP]
simp [← e]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso (snd c)
[PROOFSTEP]
refine' Iff.trans _ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk (snd c) (fst c)))
[PROOFSTEP]
exact
  ⟨fun h => ⟨BinaryFan.isLimitFlip h.some⟩, fun h =>
    ⟨(BinaryFan.isLimitFlip h.some).ofIsoLimit (isoBinaryFanMk c).symm⟩⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ IsLimit (mk (fst c ≫ f) (snd c))
[PROOFSTEP]
fapply BinaryFan.isLimitMk
[GOAL]
case lift
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ (s : BinaryFan X' ((pair X Y).obj { as := right })) →
    s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
[PROOFSTEP]
exact fun s => h.lift (BinaryFan.mk (s.fst ≫ inv f) s.snd)
[GOAL]
case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (mk (fst s ≫ inv f) (snd s)) ≫ fst c ≫ f = fst s
[PROOFSTEP]
intro s
[GOAL]
case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
⊢ IsLimit.lift h (mk (fst s ≫ inv f) (snd s)) ≫ fst c ≫ f = fst s
[PROOFSTEP]
simp only [Category.comp_id, BinaryFan.π_app_left, IsIso.inv_hom_id, BinaryFan.mk_fst, IsLimit.fac_assoc,
  eq_self_iff_true, Category.assoc]
[GOAL]
case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (mk (fst s ≫ inv f) (snd s)) ≫ snd c = snd s
[PROOFSTEP]
intro s
[GOAL]
case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
⊢ IsLimit.lift h (mk (fst s ≫ inv f) (snd s)) ≫ snd c = snd s
[PROOFSTEP]
simp only [BinaryFan.π_app_right, BinaryFan.mk_snd, eq_self_iff_true, IsLimit.fac]
[GOAL]
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ fst c ≫ f = fst s → m ≫ snd c = snd s → m = IsLimit.lift h (mk (fst s ≫ inv f) (snd s))
[PROOFSTEP]
intro s m e₁ e₂
[GOAL]
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ fst c ≫ f = fst s
e₂ : m ≫ snd c = snd s
⊢ m = IsLimit.lift h (mk (fst s ≫ inv f) (snd s))
[PROOFSTEP]
apply BinaryFan.IsLimit.hom_ext h
[GOAL]
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ fst c ≫ f = fst s
e₂ : m ≫ snd c = snd s
⊢ m ≫ fst c = IsLimit.lift h (mk (fst s ≫ inv f) (snd s)) ≫ fst c
[PROOFSTEP]
simpa only [BinaryFan.π_app_left, BinaryFan.mk_fst, Category.assoc, IsLimit.fac, IsIso.eq_comp_inv]
[GOAL]
case uniq.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ fst c ≫ f = fst s
e₂ : m ≫ snd c = snd s
⊢ m ≫ snd c = IsLimit.lift h (mk (fst s ≫ inv f) (snd s)) ≫ snd c
[PROOFSTEP]
simpa only [BinaryFan.π_app_right, BinaryFan.mk_snd, IsLimit.fac]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso (inl c)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso (inl c)
[PROOFSTEP]
rintro ⟨H⟩
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
⊢ IsIso (inl c)
[PROOFSTEP]
obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
[GOAL]
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ IsIso (inl c)
[PROOFSTEP]
refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
[GOAL]
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ inl c ≫ l ≫ inl c = inl c ≫ 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ inl c ≫ l ≫ inl c = inl c
[PROOFSTEP]
have e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c := congrArg (· ≫ inl c) hl
[GOAL]
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c
⊢ inl c ≫ l ≫ inl c = inl c
[PROOFSTEP]
rwa [Category.assoc, Category.id_comp] at e
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso (inl c) → Nonempty (IsColimit c)
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
a✝ : IsIso (inl c)
⊢ Nonempty (IsColimit c)
[PROOFSTEP]
exact
  ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f) (fun _ _ => IsIso.hom_inv_id_assoc _ _)
      (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => (IsIso.eq_inv_comp _).mpr e⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso (inr c)
[PROOFSTEP]
refine' Iff.trans _ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk (inr c) (inl c)))
[PROOFSTEP]
exact
  ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
    ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ IsColimit (mk (f ≫ inl c) (inr c))
[PROOFSTEP]
fapply BinaryCofan.isColimitMk
[GOAL]
case desc
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ (s : BinaryCofan X' ((pair X Y).obj { as := right })) →
    ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
[PROOFSTEP]
exact fun s => h.desc (BinaryCofan.mk (inv f ≫ s.inl) s.inr)
[GOAL]
case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })),
    (f ≫ inl c) ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s)) = inl s
[PROOFSTEP]
intro s
[GOAL]
case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
⊢ (f ≫ inl c) ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s)) = inl s
[PROOFSTEP]
simp only [IsColimit.fac, BinaryCofan.ι_app_left, eq_self_iff_true, Category.assoc, BinaryCofan.mk_inl,
  IsIso.hom_inv_id_assoc]
[GOAL]
case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), inr c ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s)) = inr s
[PROOFSTEP]
intro s
[GOAL]
case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
⊢ inr c ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s)) = inr s
[PROOFSTEP]
simp only [IsColimit.fac, BinaryCofan.ι_app_right, eq_self_iff_true, BinaryCofan.mk_inr]
[GOAL]
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right }))
    (m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt),
    (f ≫ inl c) ≫ m = inl s → inr c ≫ m = inr s → m = IsColimit.desc h (mk (inv f ≫ inl s) (inr s))
[PROOFSTEP]
intro s m e₁ e₂
[GOAL]
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ inl c) ≫ m = inl s
e₂ : inr c ≫ m = inr s
⊢ m = IsColimit.desc h (mk (inv f ≫ inl s) (inr s))
[PROOFSTEP]
apply BinaryCofan.IsColimit.hom_ext h
[GOAL]
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ inl c) ≫ m = inl s
e₂ : inr c ≫ m = inr s
⊢ inl c ≫ m = inl c ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s))
[PROOFSTEP]
rw [← cancel_epi f]
  -- Porting note: simp timed out here too
[GOAL]
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ inl c) ≫ m = inl s
e₂ : inr c ≫ m = inr s
⊢ f ≫ inl c ≫ m = f ≫ inl c ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s))
[PROOFSTEP]
simpa only [IsColimit.fac, BinaryCofan.ι_app_left, eq_self_iff_true, Category.assoc, BinaryCofan.mk_inl,
  IsIso.hom_inv_id_assoc] using e₁
[GOAL]
case uniq.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ inl c) ≫ m = inl s
e₂ : inr c ≫ m = inr s
⊢ inr c ≫ m = inr c ≫ IsColimit.desc h (mk (inv f ≫ inl s) (inr s))
[PROOFSTEP]
simpa only [IsColimit.fac, BinaryCofan.ι_app_right, eq_self_iff_true, BinaryCofan.mk_inr]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ NatTrans.app (limit.cone (pair X Y)).π { as := u } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ NatTrans.app (BinaryFan.mk prod.fst prod.snd).π { as := u }
[PROOFSTEP]
cases u
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ NatTrans.app (limit.cone (pair X Y)).π { as := left } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ NatTrans.app (BinaryFan.mk prod.fst prod.snd).π { as := left }
[PROOFSTEP]
dsimp
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ BinaryFan.fst (limit.cone (pair X Y)) = 𝟙 (limit (pair X Y)) ≫ prod.fst
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ BinaryFan.fst (limit.cone (pair X Y)) = prod.fst
[PROOFSTEP]
rfl
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ NatTrans.app (limit.cone (pair X Y)).π { as := right } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ NatTrans.app (BinaryFan.mk prod.fst prod.snd).π { as := right }
[PROOFSTEP]
dsimp
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ BinaryFan.snd (limit.cone (pair X Y)) = 𝟙 (limit (pair X Y)) ≫ prod.snd
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ BinaryFan.snd (limit.cone (pair X Y)) = prod.snd
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ NatTrans.app (colimit.cocone (pair X Y)).ι { as := u } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    NatTrans.app (BinaryCofan.mk coprod.inl coprod.inr).ι { as := u }
[PROOFSTEP]
cases u
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ NatTrans.app (colimit.cocone (pair X Y)).ι { as := left } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    NatTrans.app (BinaryCofan.mk coprod.inl coprod.inr).ι { as := left }
[PROOFSTEP]
dsimp
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ colimit.ι (pair X Y) { as := left } ≫ 𝟙 (colimit (pair X Y)) = coprod.inl
[PROOFSTEP]
simp only [Category.comp_id]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ NatTrans.app (colimit.cocone (pair X Y)).ι { as := right } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    NatTrans.app (BinaryCofan.mk coprod.inl coprod.inr).ι { as := right }
[PROOFSTEP]
dsimp
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ colimit.ι (pair X Y) { as := right } ≫ 𝟙 (colimit (pair X Y)) = coprod.inr
[PROOFSTEP]
simp only [Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst = lift (f ≫ g) (f ≫ h) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd = lift (f ≫ g) (f ≫ h) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct Y Y
f : X ⟶ Y
⊢ f ≫ diag Y = lift f f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨯ Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ fst = 𝟙 (X ⨯ Y) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd = 𝟙 (X ⨯ Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ fst = 𝟙 (X ⨯ Y) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ map h k = lift (f ≫ h) (g ≫ k)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ fst = lift (f ≫ h) (g ≫ k) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst ≫ g) (snd ≫ g') = map g g'
[PROOFSTEP]
rw [← prod.lift_map]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ map f g ≫ map h k = map (f ≫ h) (g ≫ k)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ (map f g ≫ map h k) ≫ fst = map (f ≫ h) (g ≫ k) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
X Y A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ (map f g ≫ map h k) ≫ snd = map (f ≫ h) (g ≫ k) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryProduct X W
inst✝¹ : HasBinaryProduct Z W
inst✝ : HasBinaryProduct Y W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryProduct W X
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct W Z
⊢ map (𝟙 W) (f ≫ g) = map (𝟙 W) f ≫ map (𝟙 W) g
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.160582, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ i₁ = i₂
[PROOFSTEP]
ext
[GOAL]
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.160582, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ i₁ ≫ fst = i₂ ≫ fst
[PROOFSTEP]
rw [← cancel_mono f]
[GOAL]
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.160582, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ (i₁ ≫ fst) ≫ f = (i₂ ≫ fst) ≫ f
[PROOFSTEP]
simpa using congr_arg (fun f => f ≫ prod.fst) h
[GOAL]
case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.160582, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ i₁ ≫ snd = i₂ ≫ snd
[PROOFSTEP]
rw [← cancel_mono g]
[GOAL]
case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.160582, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ (i₁ ≫ snd) ≫ g = (i₂ ≫ snd) ≫ g
[PROOFSTEP]
simpa using congr_arg (fun f => f ≫ prod.snd) h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ X Y : C
f : X ⟶ Y
inst✝¹ : HasBinaryProduct X X
inst✝ : HasBinaryProduct Y Y
⊢ diag X ≫ map f f = f ≫ diag Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (X ⨯ Y) (X ⨯ Y)
⊢ diag (X ⨯ Y) ≫ map fst snd = 𝟙 (X ⨯ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ diag (X ⨯ X') ≫ map (fst ≫ g) (snd ≫ g') = map g g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ desc g h ≫ f = desc (g ≫ f) (h ≫ f)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ inl ≫ desc g h ≫ f = inl ≫ desc (g ≫ f) (h ≫ f)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ inr ≫ desc g h ≫ f = inr ≫ desc (g ≫ f) (h ≫ f)
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u
inst✝¹ : Category.{u_1, u} C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
Z : C
l : W ⟶ Z
⊢ desc g h ≫ f ≫ l = desc (g ≫ f) (h ≫ f) ≫ l
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X X
f : X ⟶ Y
⊢ codiag X ≫ f = desc f f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨿ Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ map (𝟙 X) (𝟙 Y) = inl ≫ 𝟙 (X ⨿ Y)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ map (𝟙 X) (𝟙 Y) = inr ≫ 𝟙 (X ⨿ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ desc inl inr = 𝟙 (X ⨿ Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ desc inl inr = inl ≫ 𝟙 (X ⨿ Y)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ desc inl inr = inr ≫ 𝟙 (X ⨿ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ map h k ≫ desc f g = desc (h ≫ f) (k ≫ g)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inl ≫ map h k ≫ desc f g = inl ≫ desc (h ≫ f) (k ≫ g)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ inr ≫ map h k ≫ desc f g = inr ≫ desc (h ≫ f) (k ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ desc (g ≫ inl) (g' ≫ inr) = map g g'
[PROOFSTEP]
rw [← coprod.map_desc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ map g g' ≫ desc inl inr = map g g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ map f g ≫ map h k = map (f ≫ h) (g ≫ k)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ inl ≫ map f g ≫ map h k = inl ≫ map (f ≫ h) (g ≫ k)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
X Y A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ inr ≫ map f g ≫ map h k = inr ≫ map (f ≫ h) (g ≫ k)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct Z W
inst✝¹ : HasBinaryCoproduct Y W
inst✝ : HasBinaryCoproduct X W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct W X
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct W Z
⊢ map (𝟙 W) (f ≫ g) = map (𝟙 W) f ≫ map (𝟙 W) g
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.203502, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ i₁ = i₂
[PROOFSTEP]
ext
[GOAL]
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.203502, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ inl ≫ i₁ = inl ≫ i₂
[PROOFSTEP]
rw [← cancel_epi f]
[GOAL]
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.203502, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ f ≫ inl ≫ i₁ = f ≫ inl ≫ i₂
[PROOFSTEP]
simpa using congr_arg (fun f => coprod.inl ≫ f) h
[GOAL]
case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.203502, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ inr ≫ i₁ = inr ≫ i₂
[PROOFSTEP]
rw [← cancel_epi g]
[GOAL]
case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{?u.203502, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ g ≫ inr ≫ i₁ = g ≫ inr ≫ i₂
[PROOFSTEP]
simpa using congr_arg (fun f => coprod.inr ≫ f) h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ X Y : C
f : X ⟶ Y
inst✝¹ : HasBinaryCoproduct X X
inst✝ : HasBinaryCoproduct Y Y
⊢ map f f ≫ codiag Y = codiag X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)
⊢ map inl inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ map (g ≫ inl) (g' ≫ inr) ≫ codiag (Y ⨿ Y') = map g g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
inst✝ : HasBinaryProducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ prod.map f g ≫ (prod.braiding Y W).hom = (prod.braiding X Z).hom ≫ prod.map g f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
inst✝ : HasBinaryProducts C
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨯ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨯ X) Y Z).hom ≫ (associator W X (Y ⨯ Z)).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProducts C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ map (map f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ map f₁ (map f₂ f₃)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ snd ≫ lift (terminal.from P) (𝟙 P) = 𝟙 ((⊤_ C) ⨯ P)
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ (snd ≫ lift (terminal.from P) (𝟙 P)) ≫ fst = 𝟙 ((⊤_ C) ⨯ P) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ (snd ≫ lift (terminal.from P) (𝟙 P)) ≫ snd = 𝟙 ((⊤_ C) ⨯ P) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ lift (terminal.from P) (𝟙 P) ≫ snd = 𝟙 P
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ fst ≫ lift (𝟙 P) (terminal.from P) = 𝟙 (P ⨯ ⊤_ C)
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ (fst ≫ lift (𝟙 P) (terminal.from P)) ≫ fst = 𝟙 (P ⨯ ⊤_ C) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ (fst ≫ lift (𝟙 P) (terminal.from P)) ≫ snd = 𝟙 (P ⨯ ⊤_ C) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ lift (𝟙 P) (terminal.from P) ≫ fst = 𝟙 P
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv
[PROOFSTEP]
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (prod.rightUnitor X).inv ≫ prod.map f (𝟙 (⊤_ C)) = f ≫ (prod.rightUnitor Y).inv
[PROOFSTEP]
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = map (rightUnitor X).hom (𝟙 Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ ((associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom) ≫ fst = map (rightUnitor X).hom (𝟙 Y) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ ((associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom) ≫ snd = map (rightUnitor X).hom (𝟙 Y) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨿ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨿ X) Y Z).hom ≫ (associator W X (Y ⨿ Z)).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ map (map f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ map f₁ (map f₂ f₃)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 ((⊥_ C) ⨿ P)
[PROOFSTEP]
apply coprod.hom_ext
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (initial.to P) (𝟙 P) ≫ inr = inl ≫ 𝟙 ((⊥_ C) ⨿ P)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) ≫ inr = inr ≫ 𝟙 ((⊥_ C) ⨿ P)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) = 𝟙 P
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (P ⨿ ⊥_ C)
[PROOFSTEP]
apply coprod.hom_ext
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) ≫ inl = inl ≫ 𝟙 (P ⨿ ⊥_ C)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (𝟙 P) (initial.to P) ≫ inl = inr ≫ 𝟙 (P ⨿ ⊥_ C)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) = 𝟙 P
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = map (rightUnitor X).hom (𝟙 Y)
[PROOFSTEP]
ext
[GOAL]
case h₁.h₁
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inl ≫ inl ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = inl ≫ inl ≫ map (rightUnitor X).hom (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
case h₁.h₂.w
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
j✝ : Discrete PEmpty
⊢ colimit.ι (Functor.empty C) j✝ ≫ inr ≫ inl ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom =
    colimit.ι (Functor.empty C) j✝ ≫ inr ≫ inl ≫ map (rightUnitor X).hom (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = inr ≫ map (rightUnitor X).hom (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)
[PROOFSTEP]
rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ← F.map_comp,
  prod.map_fst, ← F.map_comp, prod.map_snd]
[GOAL]
C : Type u
inst✝⁷ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F✝ : C ⥤ D
A✝ A' B B' : C
inst✝⁵ : HasBinaryProduct A✝ B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F✝.obj A✝) (F✝.obj B)
inst✝² : HasBinaryProduct (F✝.obj A') (F✝.obj B')
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
F : C ⥤ D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (prod.functor.obj A ⋙ F).map f_1 ≫ (fun B => prodComparison F A B) Y =
      (fun B => prodComparison F A B) f ≫ (F ⋙ prod.functor.obj (F.obj A)).map f_1
[PROOFSTEP]
simp [prodComparison_natural]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁴ : HasBinaryProduct A B
inst✝³ : HasBinaryProduct A' B'
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (F.obj A') (F.obj B')
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map prod.fst = prod.fst
[PROOFSTEP]
simp [IsIso.inv_comp_eq]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁴ : HasBinaryProduct A B
inst✝³ : HasBinaryProduct A' B'
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (F.obj A') (F.obj B')
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map prod.snd = prod.snd
[PROOFSTEP]
simp [IsIso.inv_comp_eq]
[GOAL]
C : Type u
inst✝⁷ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B')
[PROOFSTEP]
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁷ : Category.{w, u₂} D
F : C ⥤ D
A✝ A' B B' : C
inst✝⁶ : HasBinaryProduct A✝ B
inst✝⁵ : HasBinaryProduct A' B'
inst✝⁴ : HasBinaryProduct (F.obj A✝) (F.obj B)
inst✝³ : HasBinaryProduct (F.obj A') (F.obj B')
inst✝² : HasBinaryProducts C
inst✝¹ : HasBinaryProducts D
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ prod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A)
[PROOFSTEP]
refine { @asIso _ _ _ _ _ (?_) with hom := prodComparisonNatTrans F A }
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁷ : Category.{w, u₂} D
F : C ⥤ D
A✝ A' B B' : C
inst✝⁶ : HasBinaryProduct A✝ B
inst✝⁵ : HasBinaryProduct A' B'
inst✝⁴ : HasBinaryProduct (F.obj A✝) (F.obj B)
inst✝³ : HasBinaryProduct (F.obj A') (F.obj B')
inst✝² : HasBinaryProducts C
inst✝¹ : HasBinaryProducts D
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ IsIso (NatTrans.mk fun B => prodComparison F A B)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'
[PROOFSTEP]
rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp, coprod.desc_comp, ← F.map_comp,
  coprod.inl_map, ← F.map_comp, coprod.inr_map]
[GOAL]
C : Type u
inst✝⁷ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F✝ : C ⥤ D
A✝ A' B B' : C
inst✝⁵ : HasBinaryCoproduct A✝ B
inst✝⁴ : HasBinaryCoproduct A' B'
inst✝³ : HasBinaryCoproduct (F✝.obj A✝) (F✝.obj B)
inst✝² : HasBinaryCoproduct (F✝.obj A') (F✝.obj B')
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
F : C ⥤ D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (F ⋙ coprod.functor.obj (F.obj A)).map f_1 ≫ (fun B => coprodComparison F A B) Y =
      (fun B => coprodComparison F A B) f ≫ (coprod.functor.obj A ⋙ F).map f_1
[PROOFSTEP]
simp [coprodComparison_natural]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁴ : HasBinaryCoproduct A B
inst✝³ : HasBinaryCoproduct A' B'
inst✝² : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryCoproduct (F.obj A') (F.obj B')
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl
[PROOFSTEP]
simp [IsIso.inv_comp_eq]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁴ : HasBinaryCoproduct A B
inst✝³ : HasBinaryCoproduct A' B'
inst✝² : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryCoproduct (F.obj A') (F.obj B')
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr
[PROOFSTEP]
simp [IsIso.inv_comp_eq]
[GOAL]
C : Type u
inst✝⁷ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryCoproduct A B
inst✝⁴ : HasBinaryCoproduct A' B'
inst✝³ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝² : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (coprodComparison F A B)
inst✝ : IsIso (coprodComparison F A' B')
⊢ inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
    F.map (coprod.map f g) ≫ inv (coprodComparison F A' B')
[PROOFSTEP]
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁷ : Category.{w, u₂} D
F : C ⥤ D
A✝ A' B B' : C
inst✝⁶ : HasBinaryCoproduct A✝ B
inst✝⁵ : HasBinaryCoproduct A' B'
inst✝⁴ : HasBinaryCoproduct (F.obj A✝) (F.obj B)
inst✝³ : HasBinaryCoproduct (F.obj A') (F.obj B')
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasBinaryCoproducts D
A : C
inst✝ : ∀ (B : C), IsIso (coprodComparison F A B)
⊢ F ⋙ coprod.functor.obj (F.obj A) ≅ coprod.functor.obj A ⋙ F
[PROOFSTEP]
refine { @asIso _ _ _ _ _ (?_) with hom := coprodComparisonNatTrans F A }
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁷ : Category.{w, u₂} D
F : C ⥤ D
A✝ A' B B' : C
inst✝⁶ : HasBinaryCoproduct A✝ B
inst✝⁵ : HasBinaryCoproduct A' B'
inst✝⁴ : HasBinaryCoproduct (F.obj A✝) (F.obj B)
inst✝³ : HasBinaryCoproduct (F.obj A') (F.obj B')
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasBinaryCoproducts D
A : C
inst✝ : ∀ (B : C), IsIso (coprodComparison F A B)
⊢ IsIso (NatTrans.mk fun B => coprodComparison F A B)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k : X✝ ⟶ Y✝
g : Over A
⊢ coprod.map k.left (𝟙 ((𝟭 C).obj g.left)) ≫ (((fun f => coprodObj f) Y✝).obj g).hom =
    (((fun f => coprodObj f) X✝).obj g).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k : X✝ ⟶ Y✝
g : Over A
⊢ coprod.map k.left (𝟙 g.left) ≫ coprod.desc Y✝.hom g.hom = coprod.desc X✝.hom g.hom
[PROOFSTEP]
rw [coprod.map_desc, Category.id_comp, Over.w k]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k✝ : X✝ ⟶ Y✝
f g : Over A
k : f ⟶ g
⊢ ((fun f => coprodObj f) X✝).map k ≫ (fun g => homMk (coprod.map k✝.left (𝟙 ((𝟭 C).obj g.left)))) g =
    (fun g => homMk (coprod.map k✝.left (𝟙 ((𝟭 C).obj g.left)))) f ≫ ((fun f => coprodObj f) Y✝).map k
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k✝ : X✝ ⟶ Y✝
f g : Over A
k : f ⟶ g
⊢ (((fun f => coprodObj f) X✝).map k ≫ (fun g => homMk (coprod.map k✝.left (𝟙 ((𝟭 C).obj g.left)))) g).left =
    ((fun g => homMk (coprod.map k✝.left (𝟙 ((𝟭 C).obj g.left)))) f ≫ ((fun f => coprodObj f) Y✝).map k).left
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k✝ : X✝ ⟶ Y✝
f g : Over A
k : f ⟶ g
⊢ coprod.map (𝟙 X✝.left) k.left ≫ coprod.map k✝.left (𝟙 g.left) =
    coprod.map k✝.left (𝟙 f.left) ≫ coprod.map (𝟙 Y✝.left) k.left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X : Over A
⊢ { obj := fun f => coprodObj f,
          map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun f => coprodObj f,
            map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.obj
        X)
[PROOFSTEP]
ext
[GOAL]
case w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X x✝ : Over A
⊢ (NatTrans.app
        ({ obj := fun f => coprodObj f,
              map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
          (𝟙 X))
        x✝).left =
    (NatTrans.app
        (𝟙
          ({ obj := fun f => coprodObj f,
                map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.obj
            X))
        x✝).left
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X x✝ : Over A
⊢ coprod.map (𝟙 X.left) (𝟙 x✝.left) = 𝟙 (X.left ⨿ x✝.left)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ Z✝ : Over A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun f => coprodObj f,
          map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
      (f ≫ g) =
    { obj := fun f => coprodObj f,
            map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
        f ≫
      { obj := fun f => coprodObj f,
            map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
        g
[PROOFSTEP]
ext
[GOAL]
case w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ Z✝ : Over A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Over A
⊢ (NatTrans.app
        ({ obj := fun f => coprodObj f,
              map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
          (f ≫ g))
        x✝).left =
    (NatTrans.app
        ({ obj := fun f => coprodObj f,
                map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
            f ≫
          { obj := fun f => coprodObj f,
                map := fun {X Y} k => NatTrans.mk fun g => homMk (coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) }.map
            g)
        x✝).left
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ Z✝ : Over A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Over A
⊢ coprod.map (f.left ≫ g.left) (𝟙 x✝.left) = coprod.map f.left (𝟙 x✝.left) ≫ coprod.map g.left (𝟙 x✝.left)
[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 G H I : C ⥤ D
α β : F ⟶ G
h : α = β
X : C
⊢ app α X = app β X
[PROOFSTEP]
rw [h]
[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 G H I : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Mono (app α X)
Z✝ : C ⥤ D
g h : Z✝ ⟶ F
eq : g ≫ α = h ≫ α
⊢ g = h
[PROOFSTEP]
ext X
[GOAL]
case w.h
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 G H I : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Mono (app α X)
Z✝ : C ⥤ D
g h : Z✝ ⟶ F
eq : g ≫ α = h ≫ α
X : C
⊢ app g X = app h X
[PROOFSTEP]
rw [← cancel_mono (α.app X), ← comp_app, eq, comp_app]
[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 G H I : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (app α X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
⊢ g = h
[PROOFSTEP]
ext X
[GOAL]
case w.h
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 G H I : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (app α X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ app g X = app h X
[PROOFSTEP]
rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]
[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 G H✝ I✝ : C ⥤ D
H I : D ⥤ E
α : F ⟶ G
β : H ⟶ I
X Y : C
f : X ⟶ Y
⊢ (F ⋙ H).map f ≫ (fun X => app β (F.obj X) ≫ I.map (app α X)) Y =
    (fun X => app β (F.obj X) ≫ I.map (app α X)) X ≫ (G ⋙ I).map f
[PROOFSTEP]
rw [Functor.comp_map, Functor.comp_map, ← assoc, naturality, assoc, ← map_comp I, naturality, map_comp, assoc]
[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 G H✝ I : C ⥤ D
H : D ⥤ E
α : F ⟶ G
X : C
⊢ app (α ◫ 𝟙 H) X = H.map (app α X)
[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 G H✝ I : C ⥤ D
H : E ⥤ C
α : F ⟶ G
X : E
⊢ app (𝟙 H ◫ α) X = app α (H.obj X)
[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 G H I✝ : C ⥤ D
I J K : D ⥤ E
α : F ⟶ G
β : G ⟶ H
γ : I ⟶ J
δ : J ⟶ K
⊢ (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ
[PROOFSTEP]
aesop_cat
[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✝ G H I : C ⥤ D
F : C ⥤ D ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ app (F.map e.hom) Z ≫ app (F.map e.inv) Z = 𝟙 ((F.obj X).obj Z)
[PROOFSTEP]
simp [← NatTrans.comp_app, ← Functor.map_comp]
[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✝ G H I : C ⥤ D
F : C ⥤ D ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ app (F.map e.inv) Z ≫ app (F.map e.hom) Z = 𝟙 ((F.obj Y).obj Z)
[PROOFSTEP]
simp [← NatTrans.comp_app, ← Functor.map_comp]


[GOAL]
C : Type u₁
inst✝¹ : Category.{u_1, u₁} C
D : Type u₂
inst✝ : Category.{u_2, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : D
h : F.obj Z ⟶ W
⊢ F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h
[PROOFSTEP]
rw [F.map_comp, Category.assoc]
[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
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map (f ≫ g) =
      { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map f ≫
        { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map g
[PROOFSTEP]
intros
[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
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map (f✝ ≫ g✝) =
    { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map f✝ ≫
      { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map g✝
[PROOFSTEP]
dsimp
[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
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ G.map (F.map (f✝ ≫ g✝)) = G.map (F.map f✝) ≫ G.map (F.map g✝)
[PROOFSTEP]
rw [F.map_comp, G.map_comp]
[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
⊢ F ⋙ 𝟭 D = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ mk toPrefunctor✝ ⋙ 𝟭 D = mk toPrefunctor✝
[PROOFSTEP]
rfl
[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
⊢ 𝟭 C ⋙ F = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ 𝟭 C ⋙ mk toPrefunctor✝ = mk toPrefunctor✝
[PROOFSTEP]
rfl
[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
X Y : C
P : Prop
inst✝ : Decidable P
f : P → (X ⟶ Y)
g : ¬P → (X ⟶ Y)
⊢ F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
[PROOFSTEP]
aesop_cat