[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
⊢ ∀ ⦃X Y : Discrete PUnit⦄ (f : X ⟶ Y),
    ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f ≫
        (fun x =>
            match x with
            | { as := PUnit.unit } =>
              𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
          Y =
      (fun x =>
            match x with
            | { as := PUnit.unit } =>
              𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
          X ≫
        F.map f
[PROOFSTEP]
intro X Y f
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
⊢ ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        Y =
    (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        X ≫
      F.map f
[PROOFSTEP]
match X, Y, f with
| .mk A, .mk B, .up g => aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
A B : PUnit
g : PLift ({ as := A }.as = { as := B }.as)
⊢ ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map { down := g } ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        { as := B } =
    (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        { as := A } ≫
      F.map { down := g }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ NatTrans.app c.π j ≫ F.map f = NatTrans.app c.π j'
[PROOFSTEP]
rw [← c.π.naturality f]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ ((const J).obj c.pt).map f ≫ NatTrans.app c.π j' = NatTrans.app c.π j'
[PROOFSTEP]
apply id_comp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
⊢ ∀ ⦃X Y : Discrete PUnit⦄ (f : X ⟶ Y),
    F.map f ≫
        (fun x =>
            match x with
            | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
          Y =
      (fun x =>
            match x with
            | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
          X ≫
        ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f
[PROOFSTEP]
intro X Y f
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
⊢ F.map f ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        Y =
    (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        X ≫
      ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f
[PROOFSTEP]
match X, Y, f with
| .mk A, .mk B, .up g => aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
A B : PUnit
g : PLift ({ as := A }.as = { as := B }.as)
⊢ F.map { down := g } ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        { as := B } =
    (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        { as := A } ≫
      ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map { down := g }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ NatTrans.app c.ι j' = NatTrans.app c.ι j
[PROOFSTEP]
rw [c.ι.naturality f]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ NatTrans.app c.ι j ≫ ((const J).obj c.pt).map f = NatTrans.app c.ι j
[PROOFSTEP]
apply comp_id
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { fst := op c.pt, snd := c.π }) ≫ fun c => { pt := c.fst.unop, π := c.snd }) = 𝟙 (Cone F)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : Cone F
⊢ ((fun c => { fst := op c.pt, snd := c.π }) ≫ fun c => { pt := c.fst.unop, π := c.snd }) X = 𝟙 (Cone F) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
⊢ ((fun c => { fst := op c.pt, snd := c.π }) ≫ fun c => { pt := c.fst.unop, π := c.snd }) { pt := pt✝, π := π✝ } =
    𝟙 (Cone F) { pt := pt✝, π := π✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { pt := c.fst.unop, π := c.snd }) ≫ fun c => { fst := op c.pt, snd := c.π }) =
    𝟙 ((X : Cᵒᵖ) × (Functor.cones F).obj X)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × (Functor.cones F).obj X
⊢ ((fun c => { pt := c.fst.unop, π := c.snd }) ≫ fun c => { fst := op c.pt, snd := c.π }) X =
    𝟙 ((X : Cᵒᵖ) × (Functor.cones F).obj X) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
fst✝ : Cᵒᵖ
snd✝ : (Functor.cones F).obj fst✝
⊢ ((fun c => { pt := c.fst.unop, π := c.snd }) ≫ fun c => { fst := op c.pt, snd := c.π }) { fst := fst✝, snd := snd✝ } =
    𝟙 ((X : Cᵒᵖ) × (Functor.cones F).obj X) { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { fst := c.pt, snd := c.ι }) ≫ fun c => { pt := c.fst, ι := c.snd }) = 𝟙 (Cocone F)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : Cocone F
⊢ ((fun c => { fst := c.pt, snd := c.ι }) ≫ fun c => { pt := c.fst, ι := c.snd }) X = 𝟙 (Cocone F) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
⊢ ((fun c => { fst := c.pt, snd := c.ι }) ≫ fun c => { pt := c.fst, ι := c.snd }) { pt := pt✝, ι := ι✝ } =
    𝟙 (Cocone F) { pt := pt✝, ι := ι✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { pt := c.fst, ι := c.snd }) ≫ fun c => { fst := c.pt, snd := c.ι }) =
    𝟙 ((X : C) × (Functor.cocones F).obj X)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : (X : C) × (Functor.cocones F).obj X
⊢ ((fun c => { pt := c.fst, ι := c.snd }) ≫ fun c => { fst := c.pt, snd := c.ι }) X =
    𝟙 ((X : C) × (Functor.cocones F).obj X) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
fst✝ : C
snd✝ : (Functor.cocones F).obj fst✝
⊢ ((fun c => { pt := c.fst, ι := c.snd }) ≫ fun c => { fst := c.pt, snd := c.ι }) { fst := fst✝, snd := snd✝ } =
    𝟙 ((X : C) × (Functor.cocones F).obj X) { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.Hom = g.Hom
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ NatTrans.app c'.π j = NatTrans.app c.π j
w : (mk Hom✝).Hom = g.Hom
⊢ mk Hom✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
Hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), Hom✝¹ ≫ NatTrans.app c'.π j = NatTrans.app c.π j
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ NatTrans.app c'.π j = NatTrans.app c.π j
w : (mk Hom✝¹).Hom = (mk Hom✝).Hom
⊢ mk Hom✝¹ = mk Hom✝
[PROOFSTEP]
congr
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F K : J ⥤ C
c d : Cone K
f : c ⟶ d
i : IsIso f.Hom
⊢ f ≫ ConeMorphism.mk (inv f.Hom) = 𝟙 c ∧ ConeMorphism.mk (inv f.Hom) ≫ f = 𝟙 d
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
⊢ ∀ (j : K),
    NatTrans.app
        (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj s).π j =
      (Iso.refl
            (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj
                s).pt).hom ≫
        NatTrans.app ((𝟭 (Cone (e.functor ⋙ F))).obj s).π j
[PROOFSTEP]
intro k
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
k : K
⊢ NatTrans.app
      (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj s).π k =
    (Iso.refl
          (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj
              s).pt).hom ≫
      NatTrans.app ((𝟭 (Cone (e.functor ⋙ F))).obj s).π k
[PROOFSTEP]
simpa [e.counit_app_functor] using s.w (e.unitInv.app k)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((const J).obj (G.obj A.pt)).map f ≫ (fun j => G.map (NatTrans.app A.π j)) Y =
      (fun j => G.map (NatTrans.app A.π j)) X ≫ (F ⋙ G).map f
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ ((const J).obj (G.obj A.pt)).map f✝ ≫ (fun j => G.map (NatTrans.app A.π j)) Y✝ =
    (fun j => G.map (NatTrans.app A.π j)) X✝ ≫ (F ⋙ G).map f✝
[PROOFSTEP]
erw [← G.map_comp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ ((const J).obj (G.obj A.pt)).map f✝ ≫ (fun j => G.map (NatTrans.app A.π j)) Y✝ =
    G.map (NatTrans.app A.π X✝ ≫ F.map f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ G.map f.Hom ≫
      NatTrans.app ((fun A => { pt := G.obj A.pt, π := NatTrans.mk fun j => G.map (NatTrans.app A.π j) }) Y✝).π j =
    NatTrans.app ((fun A => { pt := G.obj A.pt, π := NatTrans.mk fun j => G.map (NatTrans.app A.π j) }) X✝).π j
[PROOFSTEP]
simp [-ConeMorphism.w, ← f.w j]
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝¹ : Full G
inst✝ : Faithful G
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (G.preimage t.Hom ≫ NatTrans.app Y✝.π j) = G.map (NatTrans.app X✝.π j)
[PROOFSTEP]
simpa using t.w j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
c c' : Cone F
f g : c ⟶ c'
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f = g
[PROOFSTEP]
apply ConeMorphism.ext f g
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
c c' : Cone F
f g : c ⟶ c'
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f.Hom = g.Hom
[PROOFSTEP]
let f := ConeMorphism.mk.inj e
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
c c' : Cone F
f✝ g : c ⟶ c'
e : (functoriality F G).map f✝ = (functoriality F G).map g
f : G.map f✝.Hom = G.map g.Hom := ConeMorphism.mk.inj e
⊢ f✝.Hom = g.Hom
[PROOFSTEP]
apply G.map_injective f
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ReflectsIsomorphisms (functoriality K F)
[PROOFSTEP]
constructor
[GOAL]
case reflects
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ∀ {A B : Cone K} (f : A ⟶ B) [inst : IsIso ((functoriality K F).map f)], IsIso f
[PROOFSTEP]
intro A B f _
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f
[PROOFSTEP]
haveI : IsIso (F.map f.Hom) := (Cones.forget (K ⋙ F)).map_isIso ((Cones.functoriality K F).map f)
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this : IsIso (F.map f.Hom)
⊢ IsIso f
[PROOFSTEP]
haveI := ReflectsIsomorphisms.reflects F f.Hom
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this✝ : IsIso (F.map f.Hom)
this : IsIso f.Hom
⊢ IsIso f
[PROOFSTEP]
apply cone_iso_of_hom_iso
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cocone F
f g : c ⟶ c'
w : f.Hom = g.Hom
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cocone F
g : c ⟶ c'
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), NatTrans.app c.ι j ≫ Hom✝ = NatTrans.app c'.ι j
w : (mk Hom✝).Hom = g.Hom
⊢ mk Hom✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cocone F
Hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), NatTrans.app c.ι j ≫ Hom✝¹ = NatTrans.app c'.ι j
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), NatTrans.app c.ι j ≫ Hom✝ = NatTrans.app c'.ι j
w : (mk Hom✝¹).Hom = (mk Hom✝).Hom
⊢ mk Hom✝¹ = mk Hom✝
[PROOFSTEP]
congr
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F K : J ⥤ C
c d : Cocone K
f : c ⟶ d
i : IsIso f.Hom
⊢ f ≫ CoconeMorphism.mk (inv f.Hom) = 𝟙 c ∧ CoconeMorphism.mk (inv f.Hom) ≫ f = 𝟙 d
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
e : K ≌ J
s : Cocone (e.functor ⋙ F)
k : K
⊢ NatTrans.app
        (((whiskering e.inverse ⋙
                  precompose
                    ((leftUnitor F).inv ≫ whiskerRight e.counitIso.inv F ≫ (associator e.inverse e.functor F).inv)) ⋙
                whiskering e.functor).obj
            s).ι
        k ≫
      (Iso.refl
          (((whiskering e.inverse ⋙
                    precompose
                      ((leftUnitor F).inv ≫ whiskerRight e.counitIso.inv F ≫ (associator e.inverse e.functor F).inv)) ⋙
                  whiskering e.functor).obj
              s).pt).hom =
    NatTrans.app ((𝟭 (Cocone (e.functor ⋙ F))).obj s).ι k
[PROOFSTEP]
simpa [e.counitInv_app_functor k] using s.w (e.unit.app k)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cocone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (F ⋙ G).map f ≫ (fun j => G.map (NatTrans.app A.ι j)) Y =
      (fun j => G.map (NatTrans.app A.ι j)) X ≫ ((const J).obj (G.obj A.pt)).map f
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cocone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).map f✝ ≫ (fun j => G.map (NatTrans.app A.ι j)) Y✝ =
    (fun j => G.map (NatTrans.app A.ι j)) X✝ ≫ ((const J).obj (G.obj A.pt)).map f✝
[PROOFSTEP]
erw [← G.map_comp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cocone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ G.map (F.map f✝ ≫ NatTrans.app A.ι Y✝) =
    (fun j => G.map (NatTrans.app A.ι j)) X✝ ≫ ((const J).obj (G.obj A.pt)).map f✝
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
X✝ Y✝ : Cocone F
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) X✝).ι j ≫
        G.map f.Hom =
      NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) Y✝).ι j
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
X✝ Y✝ : Cocone F
f : X✝ ⟶ Y✝
j✝ : J
⊢ NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) X✝).ι j✝ ≫
      G.map f.Hom =
    NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) Y✝).ι j✝
[PROOFSTEP]
rw [← Functor.map_comp, CoconeMorphism.w]
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝¹ : Full G
inst✝ : Faithful G
X✝ Y✝ : Cocone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (NatTrans.app X✝.ι j ≫ G.preimage t.Hom) = G.map (NatTrans.app Y✝.ι j)
[PROOFSTEP]
simpa using t.w j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
X Y : Cocone F
f g : X ⟶ Y
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f = g
[PROOFSTEP]
apply CoconeMorphism.ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
X Y : Cocone F
f g : X ⟶ Y
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f.Hom = g.Hom
[PROOFSTEP]
let h := CoconeMorphism.mk.inj e
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
X Y : Cocone F
f g : X ⟶ Y
e : (functoriality F G).map f = (functoriality F G).map g
h : G.map f.Hom = G.map g.Hom := CoconeMorphism.mk.inj e
⊢ f.Hom = g.Hom
[PROOFSTEP]
apply G.map_injective h
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
e : C ≌ D
f : (F ⋙ e.functor) ⋙ e.inverse ≅ F :=
  associator F e.functor e.inverse ≪≫ isoWhiskerLeft F e.unitIso.symm ≪≫ rightUnitor F
c : Cocone (F ⋙ e.functor)
j : J
⊢ NatTrans.app
        (((functoriality (F ⋙ e.functor) e.inverse ⋙ (precomposeEquivalence f.symm).functor) ⋙
                functoriality F e.functor).obj
            c).ι
        j ≫
      (e.counitIso.app c.pt).hom =
    NatTrans.app ((𝟭 (Cocone (F ⋙ e.functor))).obj c).ι j
[PROOFSTEP]
simp [← Equivalence.counitInv_app_functor]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ReflectsIsomorphisms (functoriality K F)
[PROOFSTEP]
constructor
[GOAL]
case reflects
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ∀ {A B : Cocone K} (f : A ⟶ B) [inst : IsIso ((functoriality K F).map f)], IsIso f
[PROOFSTEP]
intro A B f _
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cocone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f
[PROOFSTEP]
haveI : IsIso (F.map f.Hom) := (Cocones.forget (K ⋙ F)).map_isIso ((Cocones.functoriality K F).map f)
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cocone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this : IsIso (F.map f.Hom)
⊢ IsIso f
[PROOFSTEP]
haveI := ReflectsIsomorphisms.reflects F f.Hom
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cocone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this✝ : IsIso (F.map f.Hom)
this : IsIso f.Hom
⊢ IsIso f
[PROOFSTEP]
apply cocone_iso_of_hom_iso
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ f.Hom.op ≫ NatTrans.app (Cocone.op X).π j = NatTrans.app (Cocone.op Y).π j
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ (f.Hom.op ≫ NatTrans.app (Cocone.op X).π j).unop = (NatTrans.app (Cocone.op Y).π j).unop
[PROOFSTEP]
dsimp
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ NatTrans.app X.ι j.unop ≫ f.Hom = NatTrans.app Y.ι j.unop
[PROOFSTEP]
apply CoconeMorphism.w
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ NatTrans.app ((fun c => Cone.unop c.unop) X).ι j ≫ f.unop.Hom.unop = NatTrans.app ((fun c => Cone.unop c.unop) Y).ι j
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ (NatTrans.app ((fun c => Cone.unop c.unop) X).ι j ≫ f.unop.Hom.unop).op =
    (NatTrans.app ((fun c => Cone.unop c.unop) Y).ι j).op
[PROOFSTEP]
dsimp
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ f.unop.Hom ≫ NatTrans.app X.unop.π (op j) = NatTrans.app Y.unop.π (op j)
[PROOFSTEP]
apply ConeMorphism.w
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : (Cone F.op)ᵒᵖ
⊢ (Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop } ⋙
          Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
      c ≅
    (𝟭 (Cone F.op)ᵒᵖ).obj c
[PROOFSTEP]
induction c
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ : Cone F.op
⊢ (Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop } ⋙
          Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
      (op X✝) ≅
    (𝟭 (Cone F.op)ᵒᵖ).obj (op X✝)
[PROOFSTEP]
apply Iso.op
[GOAL]
case h.α
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ : Cone F.op
⊢ X✝ ≅
    Cocone.op
      ((Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop }).obj
        (op X✝))
[PROOFSTEP]
exact Cones.ext (Iso.refl _)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
⊢ ((Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop } ⋙
                Functor.mk
                  { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
            f ≫
          ((fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c) Y).hom).unop.Hom =
    (((fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c) X).hom ≫
          (𝟭 (Cone F.op)ᵒᵖ).map f).unop.Hom
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ (Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
        (NatTrans.app (NatIso.ofComponents fun c => Cocones.ext (Iso.refl ((𝟭 (Cocone F)).obj c).pt)).hom c) ≫
      NatTrans.app (NatIso.ofComponents fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c).hom
        ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj c) =
    𝟙 ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj c)
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
          (NatTrans.app (NatIso.ofComponents fun c => Cocones.ext (Iso.refl ((𝟭 (Cocone F)).obj c).pt)).hom c) ≫
        NatTrans.app (NatIso.ofComponents fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c).hom
          ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
            c)).unop =
    (𝟙
        ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
          c)).unop
[PROOFSTEP]
apply ConeMorphism.ext
[GOAL]
case a.w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
            (NatTrans.app (NatIso.ofComponents fun c => Cocones.ext (Iso.refl ((𝟭 (Cocone F)).obj c).pt)).hom c) ≫
          NatTrans.app (NatIso.ofComponents fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c).hom
            ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
              c)).unop.Hom =
    (𝟙
          ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
            c)).unop.Hom
[PROOFSTEP]
dsimp
[GOAL]
case a.w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ 𝟙 (op c.pt) ≫ 𝟙 (op c.pt) = 𝟙 (op c.pt)
[PROOFSTEP]
apply comp_id
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ NatTrans.app (coconeOfConeLeftOp c).ι j = (NatTrans.app c.π (op j)).op
[PROOFSTEP]
dsimp only [coconeOfConeLeftOp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ NatTrans.app (NatTrans.removeLeftOp c.π) j = (NatTrans.app c.π (op j)).op
[PROOFSTEP]
simp
