[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
⊢ ∀ ⦃X Y : StructuredArrow x ι⦄ (f_1 : X ⟶ Y),
    ((Functor.const (StructuredArrow x ι)).obj (G.obj x)).map f_1 ≫ (fun i => G.map i.hom ≫ NatTrans.app f i.right) Y =
      (fun i => G.map i.hom ≫ NatTrans.app f i.right) X ≫ (diagram ι F x).map f_1
[PROOFSTEP]
rintro ⟨⟨il⟩, ir, i⟩ ⟨⟨jl⟩, jr, j⟩ ⟨⟨⟨fl⟩⟩, fr, ff⟩
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
ir : S
il : PUnit
i : (Functor.fromPUnit x).obj { as := il } ⟶ ι.obj ir
jr : S
jl : PUnit
j : (Functor.fromPUnit x).obj { as := jl } ⟶ ι.obj jr
fr : { left := { as := il }, right := ir, hom := i }.right ⟶ { left := { as := jl }, right := jr, hom := j }.right
fl : { left := { as := il }, right := ir, hom := i }.left.as = { left := { as := jl }, right := jr, hom := j }.left.as
ff :
  (Functor.fromPUnit x).map { down := { down := fl } } ≫ { left := { as := jl }, right := jr, hom := j }.hom =
    { left := { as := il }, right := ir, hom := i }.hom ≫ ι.map fr
⊢ ((Functor.const (StructuredArrow x ι)).obj (G.obj x)).map (CommaMorphism.mk { down := { down := fl } } fr) ≫
      (fun i => G.map i.hom ≫ NatTrans.app f i.right) { left := { as := jl }, right := jr, hom := j } =
    (fun i => G.map i.hom ≫ NatTrans.app f i.right) { left := { as := il }, right := ir, hom := i } ≫
      (diagram ι F x).map (CommaMorphism.mk { down := { down := fl } } fr)
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
ir : S
il : PUnit
i : (Functor.fromPUnit x).obj { as := il } ⟶ ι.obj ir
jr : S
jl : PUnit
j : (Functor.fromPUnit x).obj { as := jl } ⟶ ι.obj jr
fr : { left := { as := il }, right := ir, hom := i }.right ⟶ { left := { as := jl }, right := jr, hom := j }.right
fl : { left := { as := il }, right := ir, hom := i }.left.as = { left := { as := jl }, right := jr, hom := j }.left.as
ff :
  (Functor.fromPUnit x).map { down := { down := fl } } ≫ { left := { as := jl }, right := jr, hom := j }.hom =
    { left := { as := il }, right := ir, hom := i }.hom ≫ ι.map fr
⊢ 𝟙 (G.obj x) ≫ G.map j ≫ NatTrans.app f jr = (G.map i ≫ NatTrans.app f ir) ≫ F.map fr
[PROOFSTEP]
dsimp at ff
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
ir : S
il : PUnit
i : (Functor.fromPUnit x).obj { as := il } ⟶ ι.obj ir
jr : S
jl : PUnit
j : (Functor.fromPUnit x).obj { as := jl } ⟶ ι.obj jr
fr : { left := { as := il }, right := ir, hom := i }.right ⟶ { left := { as := jl }, right := jr, hom := j }.right
fl : { left := { as := il }, right := ir, hom := i }.left.as = { left := { as := jl }, right := jr, hom := j }.left.as
ff : 𝟙 x ≫ j = i ≫ ι.map fr
⊢ 𝟙 (G.obj x) ≫ G.map j ≫ NatTrans.app f jr = (G.map i ≫ NatTrans.app f ir) ≫ F.map fr
[PROOFSTEP]
simp only [Category.id_comp, Category.assoc] at *
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
ir : S
il : PUnit
i : (Functor.fromPUnit x).obj { as := il } ⟶ ι.obj ir
jr : S
jl : PUnit
j : (Functor.fromPUnit x).obj { as := jl } ⟶ ι.obj jr
fr : { left := { as := il }, right := ir, hom := i }.right ⟶ { left := { as := jl }, right := jr, hom := j }.right
fl : True
ff : j = i ≫ ι.map fr
⊢ G.map j ≫ NatTrans.app f jr = G.map i ≫ NatTrans.app f ir ≫ F.map fr
[PROOFSTEP]
rw [ff]
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
ir : S
il : PUnit
i : (Functor.fromPUnit x).obj { as := il } ⟶ ι.obj ir
jr : S
jl : PUnit
j : (Functor.fromPUnit x).obj { as := jl } ⟶ ι.obj jr
fr : { left := { as := il }, right := ir, hom := i }.right ⟶ { left := { as := jl }, right := jr, hom := j }.right
fl : True
ff : j = i ≫ ι.map fr
⊢ G.map (i ≫ ι.map fr) ≫ NatTrans.app f jr = G.map i ≫ NatTrans.app f ir ≫ F.map fr
[PROOFSTEP]
have := f.naturality
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : ι ⋙ G ⟶ F
ir : S
il : PUnit
i : (Functor.fromPUnit x).obj { as := il } ⟶ ι.obj ir
jr : S
jl : PUnit
j : (Functor.fromPUnit x).obj { as := jl } ⟶ ι.obj jr
fr : { left := { as := il }, right := ir, hom := i }.right ⟶ { left := { as := jl }, right := jr, hom := j }.right
fl : True
ff : j = i ≫ ι.map fr
this : ∀ ⦃X Y : S⦄ (f_1 : X ⟶ Y), (ι ⋙ G).map f_1 ≫ NatTrans.app f Y = NatTrans.app f X ≫ F.map f_1
⊢ G.map (i ≫ ι.map fr) ≫ NatTrans.app f jr = G.map i ≫ NatTrans.app f ir ≫ F.map fr
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
⊢ ∀ (X : L),
    { obj := fun x => limit (diagram ι F x),
            map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.obj
          X)
[PROOFSTEP]
intro l
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
l : L
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
      (𝟙 l) =
    𝟙
      ({ obj := fun x => limit (diagram ι F x),
            map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.obj
        l)
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map (𝟙 _) ⋙ diagram ι F l) := h _
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
l : L
this : HasLimit (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
      (𝟙 l) =
    𝟙
      ({ obj := fun x => limit (diagram ι F x),
            map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.obj
        l)
[PROOFSTEP]
dsimp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
l : L
this : HasLimit (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
⊢ limit.pre (diagram ι F l) (StructuredArrow.map (𝟙 l)) = 𝟙 (limit (diagram ι F l))
[PROOFSTEP]
ext j
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
l : L
this : HasLimit (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
j : StructuredArrow l ι
⊢ limit.pre (diagram ι F l) (StructuredArrow.map (𝟙 l)) ≫ limit.π (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l) j =
    𝟙 (limit (diagram ι F l)) ≫ limit.π (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l) j
[PROOFSTEP]
simp only [Category.id_comp, limit.pre_π]
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
l : L
this : HasLimit (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
j : StructuredArrow l ι
⊢ limit.π (diagram ι F l) ((StructuredArrow.map (𝟙 l)).obj j) = limit.π (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l) j
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
l : L
this : HasLimit (StructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
j : StructuredArrow l ι
⊢ (StructuredArrow.map (𝟙 l)).obj j = j
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
⊢ ∀ {X Y Z : L} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun x => limit (diagram ι F x),
            map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) =
      { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g
[PROOFSTEP]
intro x y z f g
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
      (f ≫ g) =
    { obj := fun x => limit (diagram ι F x),
            map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        f ≫
      { obj := fun x => limit (diagram ι F x),
            map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        g
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
⊢ ∀ (j : StructuredArrow z ι),
    { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          (f ≫ g) ≫
        limit.π (diagram ι F z) j =
      ({ obj := fun x => limit (diagram ι F x),
                map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
            f ≫
          { obj := fun x => limit (diagram ι F x),
                map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
            g) ≫
        limit.π (diagram ι F z) j
[PROOFSTEP]
intro j
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) ≫
      limit.π (diagram ι F z) j =
    ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g) ≫
      limit.π (diagram ι F z) j
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map f ⋙ diagram ι F _) := h _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) ≫
      limit.π (diagram ι F z) j =
    ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g) ≫
      limit.π (diagram ι F z) j
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map g ⋙ diagram ι F _) := h _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this✝ : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
this : HasLimit (StructuredArrow.map g ⋙ diagram ι F y)
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) ≫
      limit.π (diagram ι F z) j =
    ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g) ≫
      limit.π (diagram ι F z) j
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map (f ≫ g) ⋙ diagram ι F _) := h _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this✝¹ : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
this✝ : HasLimit (StructuredArrow.map g ⋙ diagram ι F y)
this : HasLimit (StructuredArrow.map (f ≫ g) ⋙ diagram ι F x)
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) ≫
      limit.π (diagram ι F z) j =
    ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g) ≫
      limit.π (diagram ι F z) j
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map g ⋙ StructuredArrow.map f ⋙ diagram ι F _) := h _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this✝² : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
this✝¹ : HasLimit (StructuredArrow.map g ⋙ diagram ι F y)
this✝ : HasLimit (StructuredArrow.map (f ≫ g) ⋙ diagram ι F x)
this : HasLimit (StructuredArrow.map g ⋙ StructuredArrow.map f ⋙ diagram ι F x)
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) ≫
      limit.π (diagram ι F z) j =
    ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g) ≫
      limit.π (diagram ι F z) j
[PROOFSTEP]
haveI : HasLimit ((StructuredArrow.map g ⋙ StructuredArrow.map f) ⋙ diagram ι F _) := h _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this✝³ : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
this✝² : HasLimit (StructuredArrow.map g ⋙ diagram ι F y)
this✝¹ : HasLimit (StructuredArrow.map (f ≫ g) ⋙ diagram ι F x)
this✝ : HasLimit (StructuredArrow.map g ⋙ StructuredArrow.map f ⋙ diagram ι F x)
this : HasLimit ((StructuredArrow.map g ⋙ StructuredArrow.map f) ⋙ diagram ι F x)
⊢ { obj := fun x => limit (diagram ι F x), map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
        (f ≫ g) ≫
      limit.π (diagram ι F z) j =
    ({ obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          f ≫
        { obj := fun x => limit (diagram ι F x),
              map := fun {X Y} f => limit.pre (diagram ι F X) (StructuredArrow.map f) }.map
          g) ≫
      limit.π (diagram ι F z) j
[PROOFSTEP]
erw [limit.pre_pre, limit.pre_π, limit.pre_π]
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this✝³ : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
this✝² : HasLimit (StructuredArrow.map g ⋙ diagram ι F y)
this✝¹ : HasLimit (StructuredArrow.map (f ≫ g) ⋙ diagram ι F x)
this✝ : HasLimit (StructuredArrow.map g ⋙ StructuredArrow.map f ⋙ diagram ι F x)
this : HasLimit ((StructuredArrow.map g ⋙ StructuredArrow.map f) ⋙ diagram ι F x)
⊢ limit.π (diagram ι F x) ((StructuredArrow.map (f ≫ g)).obj j) =
    limit.π (diagram ι F x) ((StructuredArrow.map g ⋙ StructuredArrow.map f).obj j)
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
j : StructuredArrow z ι
this✝³ : HasLimit (StructuredArrow.map f ⋙ diagram ι F x)
this✝² : HasLimit (StructuredArrow.map g ⋙ diagram ι F y)
this✝¹ : HasLimit (StructuredArrow.map (f ≫ g) ⋙ diagram ι F x)
this✝ : HasLimit (StructuredArrow.map g ⋙ StructuredArrow.map f ⋙ diagram ι F x)
this : HasLimit ((StructuredArrow.map g ⋙ StructuredArrow.map f) ⋙ diagram ι F x)
⊢ (StructuredArrow.map (f ≫ g)).obj j = (StructuredArrow.map g ⋙ StructuredArrow.map f).obj j
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
⊢ ∀ ⦃X Y : S⦄ (f_1 : X ⟶ Y),
    (((whiskeringLeft S L D).obj ι).obj G).map f_1 ≫
        (fun x => NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))) Y =
      (fun x => NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))) X ≫
        F.map f_1
[PROOFSTEP]
intro x y ff
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
⊢ (((whiskeringLeft S L D).obj ι).obj G).map ff ≫
      (fun x => NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))) y =
    (fun x => NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))) x ≫
      F.map ff
[PROOFSTEP]
dsimp only [whiskeringLeft]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
⊢ (ι ⋙ G).map ff ≫ NatTrans.app f (ι.obj y) ≫ limit.π (diagram ι F (ι.obj y)) (StructuredArrow.mk (𝟙 (ι.obj y))) =
    (NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))) ≫ F.map ff
[PROOFSTEP]
simp only [Functor.comp_map, NatTrans.naturality_assoc, loc_map, Category.assoc]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
⊢ NatTrans.app f (ι.obj x) ≫
      limit.pre (diagram ι F (ι.obj x)) (StructuredArrow.map (ι.map ff)) ≫
        limit.π (diagram ι F (ι.obj y)) (StructuredArrow.mk (𝟙 (ι.obj y))) =
    NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))) ≫ F.map ff
[PROOFSTEP]
congr 1
[GOAL]
case e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
⊢ limit.pre (diagram ι F (ι.obj x)) (StructuredArrow.map (ι.map ff)) ≫
      limit.π (diagram ι F (ι.obj y)) (StructuredArrow.mk (𝟙 (ι.obj y))) =
    limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))) ≫ F.map ff
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map (ι.map ff) ⋙ diagram ι F (ι.obj x)) := h _
[GOAL]
case e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
this : HasLimit (StructuredArrow.map (ι.map ff) ⋙ diagram ι F (ι.obj x))
⊢ limit.pre (diagram ι F (ι.obj x)) (StructuredArrow.map (ι.map ff)) ≫
      limit.π (diagram ι F (ι.obj y)) (StructuredArrow.mk (𝟙 (ι.obj y))) =
    limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))) ≫ F.map ff
[PROOFSTEP]
erw [limit.pre_π]
[GOAL]
case e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
this : HasLimit (StructuredArrow.map (ι.map ff) ⋙ diagram ι F (ι.obj x))
⊢ limit.π (diagram ι F (ι.obj x)) ((StructuredArrow.map (ι.map ff)).obj (StructuredArrow.mk (𝟙 (ι.obj y)))) =
    limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))) ≫ F.map ff
[PROOFSTEP]
let t : StructuredArrow.mk (𝟙 (ι.obj x)) ⟶ (StructuredArrow.map (ι.map ff)).obj (StructuredArrow.mk (𝟙 (ι.obj y))) :=
  StructuredArrow.homMk ff ?_
[GOAL]
case e_a.refine_2
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
this : HasLimit (StructuredArrow.map (ι.map ff) ⋙ diagram ι F (ι.obj x))
t : StructuredArrow.mk (𝟙 (ι.obj x)) ⟶ (StructuredArrow.map (ι.map ff)).obj (StructuredArrow.mk (𝟙 (ι.obj y))) :=
  StructuredArrow.homMk ff
⊢ limit.π (diagram ι F (ι.obj x)) ((StructuredArrow.map (ι.map ff)).obj (StructuredArrow.mk (𝟙 (ι.obj y)))) =
    limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))) ≫ F.map ff
case e_a.refine_1
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
this : HasLimit (StructuredArrow.map (ι.map ff) ⋙ diagram ι F (ι.obj x))
⊢ (StructuredArrow.mk (𝟙 (ι.obj x))).hom ≫ ι.map ff =
    ((StructuredArrow.map (ι.map ff)).obj (StructuredArrow.mk (𝟙 (ι.obj y)))).hom
[PROOFSTEP]
convert (limit.w (diagram ι F (ι.obj x)) t).symm using 1
[GOAL]
case e_a.refine_1
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : G ⟶ loc ι F
x y : S
ff : x ⟶ y
this : HasLimit (StructuredArrow.map (ι.map ff) ⋙ diagram ι F (ι.obj x))
⊢ (StructuredArrow.mk (𝟙 (ι.obj x))).hom ≫ ι.map ff =
    ((StructuredArrow.map (ι.map ff)).obj (StructuredArrow.mk (𝟙 (ι.obj y)))).hom
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : ((whiskeringLeft S L D).obj ι).obj G ⟶ F
⊢ ∀ ⦃X Y : L⦄ (f_1 : X ⟶ Y),
    G.map f_1 ≫ (fun x => limit.lift (diagram ι F x) (cone x f)) Y =
      (fun x => limit.lift (diagram ι F x) (cone x f)) X ≫ (loc ι F).map f_1
[PROOFSTEP]
intro x y ff
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : ((whiskeringLeft S L D).obj ι).obj G ⟶ F
x y : L
ff : x ⟶ y
⊢ G.map ff ≫ (fun x => limit.lift (diagram ι F x) (cone x f)) y =
    (fun x => limit.lift (diagram ι F x) (cone x f)) x ≫ (loc ι F).map ff
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : ((whiskeringLeft S L D).obj ι).obj G ⟶ F
x y : L
ff : x ⟶ y
⊢ ∀ (j : StructuredArrow y ι),
    (G.map ff ≫ (fun x => limit.lift (diagram ι F x) (cone x f)) y) ≫ limit.π (diagram ι F y) j =
      ((fun x => limit.lift (diagram ι F x) (cone x f)) x ≫ (loc ι F).map ff) ≫ limit.π (diagram ι F y) j
[PROOFSTEP]
intros j
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : ((whiskeringLeft S L D).obj ι).obj G ⟶ F
x y : L
ff : x ⟶ y
j : StructuredArrow y ι
⊢ (G.map ff ≫ (fun x => limit.lift (diagram ι F x) (cone x f)) y) ≫ limit.π (diagram ι F y) j =
    ((fun x => limit.lift (diagram ι F x) (cone x f)) x ≫ (loc ι F).map ff) ≫ limit.π (diagram ι F y) j
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map ff ⋙ diagram ι F x) := h _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : ((whiskeringLeft S L D).obj ι).obj G ⟶ F
x y : L
ff : x ⟶ y
j : StructuredArrow y ι
this : HasLimit (StructuredArrow.map ff ⋙ diagram ι F x)
⊢ (G.map ff ≫ (fun x => limit.lift (diagram ι F x) (cone x f)) y) ≫ limit.π (diagram ι F y) j =
    ((fun x => limit.lift (diagram ι F x) (cone x f)) x ≫ (loc ι F).map ff) ≫ limit.π (diagram ι F y) j
[PROOFSTEP]
erw [limit.lift_pre, limit.lift_π, Category.assoc, limit.lift_π (cone _ f) j]
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
f : ((whiskeringLeft S L D).obj ι).obj G ⟶ F
x y : L
ff : x ⟶ y
j : StructuredArrow y ι
this : HasLimit (StructuredArrow.map ff ⋙ diagram ι F x)
⊢ G.map ff ≫ NatTrans.app (cone y f).π j = NatTrans.app (Cone.whisker (StructuredArrow.map ff) (cone x f)).π j
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
⊢ Function.LeftInverse (fun f => NatTrans.mk fun x => limit.lift (diagram ι F x) (cone x f)) fun f =>
    NatTrans.mk fun x => NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))
[PROOFSTEP]
intro x
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
⊢ (fun f => NatTrans.mk fun x => limit.lift (diagram ι F x) (cone x f))
      ((fun f =>
          NatTrans.mk fun x =>
            NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))))
        x) =
    x
[PROOFSTEP]
ext k
[GOAL]
case w.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
⊢ NatTrans.app
      ((fun f => NatTrans.mk fun x => limit.lift (diagram ι F x) (cone x f))
        ((fun f =>
            NatTrans.mk fun x =>
              NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))))
          x))
      k =
    NatTrans.app x k
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
⊢ ∀ (j : StructuredArrow k ι),
    NatTrans.app
          ((fun f => NatTrans.mk fun x => limit.lift (diagram ι F x) (cone x f))
            ((fun f =>
                NatTrans.mk fun x =>
                  NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))))
              x))
          k ≫
        limit.π (diagram ι F k) j =
      NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
intros j
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
⊢ NatTrans.app
        ((fun f => NatTrans.mk fun x => limit.lift (diagram ι F x) (cone x f))
          ((fun f =>
              NatTrans.mk fun x =>
                NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x))))
            x))
        k ≫
      limit.π (diagram ι F k) j =
    NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
dsimp only [cone]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
⊢ limit.lift (diagram ι F k)
        { pt := G.obj k,
          π :=
            NatTrans.mk fun i =>
              G.map i.hom ≫
                NatTrans.app x (ι.obj i.right) ≫
                  limit.π (diagram ι F (ι.obj i.right)) (StructuredArrow.mk (𝟙 (ι.obj i.right))) } ≫
      limit.π (diagram ι F k) j =
    NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
⊢ NatTrans.app
      { pt := G.obj k,
          π :=
            NatTrans.mk fun i =>
              G.map i.hom ≫
                NatTrans.app x (ι.obj i.right) ≫
                  limit.π (diagram ι F (ι.obj i.right)) (StructuredArrow.mk (𝟙 (ι.obj i.right))) }.π
      j =
    NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
simp only [NatTrans.naturality_assoc, loc_map]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
⊢ NatTrans.app x k ≫
      limit.pre (diagram ι F k) (StructuredArrow.map j.hom) ≫
        limit.π (diagram ι F (ι.obj j.right)) (StructuredArrow.mk (𝟙 (ι.obj j.right))) =
    NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
haveI : HasLimit (StructuredArrow.map j.hom ⋙ diagram ι F k) := h _
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
this : HasLimit (StructuredArrow.map j.hom ⋙ diagram ι F k)
⊢ NatTrans.app x k ≫
      limit.pre (diagram ι F k) (StructuredArrow.map j.hom) ≫
        limit.π (diagram ι F (ι.obj j.right)) (StructuredArrow.mk (𝟙 (ι.obj j.right))) =
    NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
erw [limit.pre_π]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
this : HasLimit (StructuredArrow.map j.hom ⋙ diagram ι F k)
⊢ NatTrans.app x k ≫
      limit.π (diagram ι F k) ((StructuredArrow.map j.hom).obj (StructuredArrow.mk (𝟙 (ι.obj j.right)))) =
    NatTrans.app x k ≫ limit.π (diagram ι F k) j
[PROOFSTEP]
congr
[GOAL]
case w.h.w.e_a.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
j : StructuredArrow k ι
this : HasLimit (StructuredArrow.map j.hom ⋙ diagram ι F k)
⊢ (StructuredArrow.map j.hom).obj (StructuredArrow.mk (𝟙 (ι.obj j.right))) = j
[PROOFSTEP]
rcases j with ⟨⟨⟩, _, _⟩
[GOAL]
case w.h.w.e_a.h.e_7.h.mk.mk
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
x : G ⟶ loc ι F
k : L
right✝ : S
as✝ : PUnit
hom✝ : (Functor.fromPUnit k).obj { as := as✝ } ⟶ ι.obj right✝
this : HasLimit (StructuredArrow.map { left := { as := as✝ }, right := right✝, hom := hom✝ }.hom ⋙ diagram ι F k)
⊢ (StructuredArrow.map { left := { as := as✝ }, right := right✝, hom := hom✝ }.hom).obj
      (StructuredArrow.mk (𝟙 (ι.obj { left := { as := as✝ }, right := right✝, hom := hom✝ }.right))) =
    { left := { as := as✝ }, right := right✝, hom := hom✝ }
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
h : ∀ (x : L), HasLimit (diagram ι F x)
G : L ⥤ D
⊢ Function.RightInverse (fun f => NatTrans.mk fun x => limit.lift (diagram ι F x) (cone x f)) fun f =>
    NatTrans.mk fun x => NatTrans.app f (ι.obj x) ≫ limit.π (diagram ι F (ι.obj x)) (StructuredArrow.mk (𝟙 (ι.obj x)))
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
⊢ ∀ (X' X : L ⥤ D) (Y : S ⥤ D) (f : X' ⟶ X) (g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y),
    ↑((fun F G => (Ran.equiv ι G F).symm) X' Y) (((whiskeringLeft S L D).obj ι).map f ≫ g) =
      f ≫ ↑((fun F G => (Ran.equiv ι G F).symm) X Y) g
[PROOFSTEP]
{
  -- Porting note: was `tidy`
  intros X' X Y f g
  ext t
  apply limit.hom_ext
  intros j
  dsimp [Ran.equiv]
  simp
}
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
⊢ ∀ (X' X : L ⥤ D) (Y : S ⥤ D) (f : X' ⟶ X) (g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y),
    ↑((fun F G => (Ran.equiv ι G F).symm) X' Y) (((whiskeringLeft S L D).obj ι).map f ≫ g) =
      f ≫ ↑((fun F G => (Ran.equiv ι G F).symm) X Y) g
[PROOFSTEP]
intros X' X Y f g
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
X' X : L ⥤ D
Y : S ⥤ D
f : X' ⟶ X
g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y
⊢ ↑((fun F G => (Ran.equiv ι G F).symm) X' Y) (((whiskeringLeft S L D).obj ι).map f ≫ g) =
    f ≫ ↑((fun F G => (Ran.equiv ι G F).symm) X Y) g
[PROOFSTEP]
ext t
[GOAL]
case w.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
X' X : L ⥤ D
Y : S ⥤ D
f : X' ⟶ X
g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y
t : L
⊢ NatTrans.app (↑((fun F G => (Ran.equiv ι G F).symm) X' Y) (((whiskeringLeft S L D).obj ι).map f ≫ g)) t =
    NatTrans.app (f ≫ ↑((fun F G => (Ran.equiv ι G F).symm) X Y) g) t
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
X' X : L ⥤ D
Y : S ⥤ D
f : X' ⟶ X
g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y
t : L
⊢ ∀ (j : StructuredArrow t ι),
    NatTrans.app (↑((fun F G => (Ran.equiv ι G F).symm) X' Y) (((whiskeringLeft S L D).obj ι).map f ≫ g)) t ≫
        limit.π (Ran.diagram ι Y t) j =
      NatTrans.app (f ≫ ↑((fun F G => (Ran.equiv ι G F).symm) X Y) g) t ≫ limit.π (Ran.diagram ι Y t) j
[PROOFSTEP]
intros j
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
X' X : L ⥤ D
Y : S ⥤ D
f : X' ⟶ X
g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y
t : L
j : StructuredArrow t ι
⊢ NatTrans.app (↑((fun F G => (Ran.equiv ι G F).symm) X' Y) (((whiskeringLeft S L D).obj ι).map f ≫ g)) t ≫
      limit.π (Ran.diagram ι Y t) j =
    NatTrans.app (f ≫ ↑((fun F G => (Ran.equiv ι G F).symm) X Y) g) t ≫ limit.π (Ran.diagram ι Y t) j
[PROOFSTEP]
dsimp [Ran.equiv]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
X' X : L ⥤ D
Y : S ⥤ D
f : X' ⟶ X
g : ((whiskeringLeft S L D).obj ι).obj X ⟶ Y
t : L
j : StructuredArrow t ι
⊢ limit.lift (Ran.diagram ι Y t)
        { pt := X'.obj t,
          π := NatTrans.mk fun i => X'.map i.hom ≫ NatTrans.app f (ι.obj i.right) ≫ NatTrans.app g i.right } ≫
      limit.π (Ran.diagram ι Y t) j =
    (NatTrans.app f t ≫
        limit.lift (Ran.diagram ι Y t)
          { pt := X.obj t, π := NatTrans.mk fun i => X.map i.hom ≫ NatTrans.app g i.right }) ≫
      limit.π (Ran.diagram ι Y t) j
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
⊢ IsIso (adjunction D ι).counit
[PROOFSTEP]
suffices : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).counit X)
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
this : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).counit X)
⊢ IsIso (adjunction D ι).counit
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
⊢ ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).counit X)
[PROOFSTEP]
intro F
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
F : S ⥤ D
⊢ IsIso (NatTrans.app (adjunction D ι).counit F)
[PROOFSTEP]
suffices : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).counit F) X)
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
F : S ⥤ D
this : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).counit F) X)
⊢ IsIso (NatTrans.app (adjunction D ι).counit F)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
F : S ⥤ D
⊢ ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).counit F) X)
[PROOFSTEP]
intro X
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
F : S ⥤ D
X : S
⊢ IsIso (NatTrans.app (NatTrans.app (adjunction D ι).counit F) X)
[PROOFSTEP]
dsimp [adjunction, equiv]
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
F : S ⥤ D
X : S
⊢ IsIso (𝟙 (limit (diagram ι F (ι.obj X))) ≫ limit.π (diagram ι F (ι.obj X)) (StructuredArrow.mk (𝟙 (ι.obj X))))
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasLimitsOfShape (StructuredArrow X ι) D
F : S ⥤ D
X : S
⊢ IsIso (limit.π (diagram ι F (ι.obj X)) (StructuredArrow.mk (𝟙 (ι.obj X))))
[PROOFSTEP]
exact IsIso.of_iso ((limit.isLimit _).conePointUniqueUpToIso (limitOfDiagramInitial StructuredArrow.mkIdInitial _))
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : F ⟶ ι ⋙ G
⊢ ∀ ⦃X Y : CostructuredArrow ι x⦄ (f_1 : X ⟶ Y),
    (diagram ι F x).map f_1 ≫ (fun i => NatTrans.app f i.left ≫ G.map i.hom) Y =
      (fun i => NatTrans.app f i.left ≫ G.map i.hom) X ≫ ((Functor.const (CostructuredArrow ι x)).obj (G.obj x)).map f_1
[PROOFSTEP]
rintro ⟨ir, ⟨il⟩, i⟩ ⟨jl, ⟨jr⟩, j⟩ ⟨fl, ⟨⟨fl⟩⟩, ff⟩
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : F ⟶ ι ⋙ G
ir : S
il : PUnit
i : ι.obj ir ⟶ (Functor.fromPUnit x).obj { as := il }
jl : S
jr : PUnit
j : ι.obj jl ⟶ (Functor.fromPUnit x).obj { as := jr }
fl✝ : { left := ir, right := { as := il }, hom := i }.left ⟶ { left := jl, right := { as := jr }, hom := j }.left
fl : { left := ir, right := { as := il }, hom := i }.right.as = { left := jl, right := { as := jr }, hom := j }.right.as
ff :
  ι.map fl✝ ≫ { left := jl, right := { as := jr }, hom := j }.hom =
    { left := ir, right := { as := il }, hom := i }.hom ≫ (Functor.fromPUnit x).map { down := { down := fl } }
⊢ (diagram ι F x).map (CommaMorphism.mk fl✝ { down := { down := fl } }) ≫
      (fun i => NatTrans.app f i.left ≫ G.map i.hom) { left := jl, right := { as := jr }, hom := j } =
    (fun i => NatTrans.app f i.left ≫ G.map i.hom) { left := ir, right := { as := il }, hom := i } ≫
      ((Functor.const (CostructuredArrow ι x)).obj (G.obj x)).map (CommaMorphism.mk fl✝ { down := { down := fl } })
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : F ⟶ ι ⋙ G
ir : S
il : PUnit
i : ι.obj ir ⟶ (Functor.fromPUnit x).obj { as := il }
jl : S
jr : PUnit
j : ι.obj jl ⟶ (Functor.fromPUnit x).obj { as := jr }
fl✝ : { left := ir, right := { as := il }, hom := i }.left ⟶ { left := jl, right := { as := jr }, hom := j }.left
fl : { left := ir, right := { as := il }, hom := i }.right.as = { left := jl, right := { as := jr }, hom := j }.right.as
ff :
  ι.map fl✝ ≫ { left := jl, right := { as := jr }, hom := j }.hom =
    { left := ir, right := { as := il }, hom := i }.hom ≫ (Functor.fromPUnit x).map { down := { down := fl } }
⊢ F.map fl✝ ≫ NatTrans.app f jl ≫ G.map j = (NatTrans.app f ir ≫ G.map i) ≫ 𝟙 (G.obj x)
[PROOFSTEP]
simp only [Functor.comp_map, Category.comp_id, NatTrans.naturality_assoc]
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : F ⟶ ι ⋙ G
ir : S
il : PUnit
i : ι.obj ir ⟶ (Functor.fromPUnit x).obj { as := il }
jl : S
jr : PUnit
j : ι.obj jl ⟶ (Functor.fromPUnit x).obj { as := jr }
fl✝ : { left := ir, right := { as := il }, hom := i }.left ⟶ { left := jl, right := { as := jr }, hom := j }.left
fl : { left := ir, right := { as := il }, hom := i }.right.as = { left := jl, right := { as := jr }, hom := j }.right.as
ff :
  ι.map fl✝ ≫ { left := jl, right := { as := jr }, hom := j }.hom =
    { left := ir, right := { as := il }, hom := i }.hom ≫ (Functor.fromPUnit x).map { down := { down := fl } }
⊢ NatTrans.app f ir ≫ G.map (ι.map fl✝) ≫ G.map j = NatTrans.app f ir ≫ G.map i
[PROOFSTEP]
rw [← G.map_comp, ff]
[GOAL]
case mk.mk.mk.mk.mk.up.up
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
G : L ⥤ D
x : L
f : F ⟶ ι ⋙ G
ir : S
il : PUnit
i : ι.obj ir ⟶ (Functor.fromPUnit x).obj { as := il }
jl : S
jr : PUnit
j : ι.obj jl ⟶ (Functor.fromPUnit x).obj { as := jr }
fl✝ : { left := ir, right := { as := il }, hom := i }.left ⟶ { left := jl, right := { as := jr }, hom := j }.left
fl : { left := ir, right := { as := il }, hom := i }.right.as = { left := jl, right := { as := jr }, hom := j }.right.as
ff :
  ι.map fl✝ ≫ { left := jl, right := { as := jr }, hom := j }.hom =
    { left := ir, right := { as := il }, hom := i }.hom ≫ (Functor.fromPUnit x).map { down := { down := fl } }
⊢ NatTrans.app f ir ≫
      G.map
        ({ left := ir, right := { as := il }, hom := i }.hom ≫ (Functor.fromPUnit x).map { down := { down := fl } }) =
    NatTrans.app f ir ≫ G.map i
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
⊢ ∀ (X : L),
    { obj := fun x => colimit (diagram ι F x),
            map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun x => colimit (diagram ι F x),
              map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.obj
          X)
[PROOFSTEP]
intro l
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
l : L
⊢ { obj := fun x => colimit (diagram ι F x),
          map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
      (𝟙 l) =
    𝟙
      ({ obj := fun x => colimit (diagram ι F x),
            map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.obj
        l)
[PROOFSTEP]
dsimp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
l : L
⊢ colimit.pre (diagram ι F l) (CostructuredArrow.map (𝟙 l)) = 𝟙 (colimit (diagram ι F l))
[PROOFSTEP]
haveI : HasColimit (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l) := I _
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
l : L
this : HasColimit (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
⊢ colimit.pre (diagram ι F l) (CostructuredArrow.map (𝟙 l)) = 𝟙 (colimit (diagram ι F l))
[PROOFSTEP]
ext j
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
l : L
this : HasColimit (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
j : CostructuredArrow ι l
⊢ colimit.ι (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l) j ≫
      colimit.pre (diagram ι F l) (CostructuredArrow.map (𝟙 l)) =
    colimit.ι (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l) j ≫ 𝟙 (colimit (diagram ι F l))
[PROOFSTEP]
erw [colimit.ι_pre, Category.comp_id]
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
l : L
this : HasColimit (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
j : CostructuredArrow ι l
⊢ colimit.ι (diagram ι F l) ((CostructuredArrow.map (𝟙 l)).obj j) =
    colimit.ι (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l) j
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
l : L
this : HasColimit (CostructuredArrow.map (𝟙 l) ⋙ diagram ι F l)
j : CostructuredArrow ι l
⊢ (CostructuredArrow.map (𝟙 l)).obj j = j
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
⊢ ∀ {X Y Z : L} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun x => colimit (diagram ι F x),
            map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
        (f ≫ g) =
      { obj := fun x => colimit (diagram ι F x),
              map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
          f ≫
        { obj := fun x => colimit (diagram ι F x),
              map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
          g
[PROOFSTEP]
intro x y z f g
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
⊢ { obj := fun x => colimit (diagram ι F x),
          map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
      (f ≫ g) =
    { obj := fun x => colimit (diagram ι F x),
            map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
        f ≫
      { obj := fun x => colimit (diagram ι F x),
            map := fun {x y} f => colimit.pre (diagram ι F y) (CostructuredArrow.map f) }.map
        g
[PROOFSTEP]
dsimp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
⊢ colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
haveI : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) := I _
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
⊢ colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
ext j
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
let ff : CostructuredArrow ι _ ⥤ _ := CostructuredArrow.map f
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
let gg : CostructuredArrow ι _ ⥤ _ := CostructuredArrow.map g
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
let dd := diagram ι F z
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
haveI : HasColimit (ff ⋙ gg ⋙ dd) := I _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this✝ : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
this : HasColimit (ff ⋙ gg ⋙ dd)
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
haveI : HasColimit ((ff ⋙ gg) ⋙ dd) := I _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this✝¹ : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
this✝ : HasColimit (ff ⋙ gg ⋙ dd)
this : HasColimit ((ff ⋙ gg) ⋙ dd)
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
haveI : HasColimit (gg ⋙ dd) := I _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this✝² : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
this✝¹ : HasColimit (ff ⋙ gg ⋙ dd)
this✝ : HasColimit ((ff ⋙ gg) ⋙ dd)
this : HasColimit (gg ⋙ dd)
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
change _ = colimit.ι ((ff ⋙ gg) ⋙ dd) j ≫ _ ≫ _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this✝² : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
this✝¹ : HasColimit (ff ⋙ gg ⋙ dd)
this✝ : HasColimit ((ff ⋙ gg) ⋙ dd)
this : HasColimit (gg ⋙ dd)
⊢ colimit.ι (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z) j ≫
      colimit.pre (diagram ι F z) (CostructuredArrow.map (f ≫ g)) =
    colimit.ι ((ff ⋙ gg) ⋙ dd) j ≫
      colimit.pre (diagram ι F y) (CostructuredArrow.map f) ≫ colimit.pre (diagram ι F z) (CostructuredArrow.map g)
[PROOFSTEP]
erw [colimit.pre_pre dd gg ff, colimit.ι_pre, colimit.ι_pre]
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this✝² : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
this✝¹ : HasColimit (ff ⋙ gg ⋙ dd)
this✝ : HasColimit ((ff ⋙ gg) ⋙ dd)
this : HasColimit (gg ⋙ dd)
⊢ colimit.ι (diagram ι F z) ((CostructuredArrow.map (f ≫ g)).obj j) = colimit.ι dd ((ff ⋙ gg).obj j)
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
x y z : L
f : x ⟶ y
g : y ⟶ z
this✝² : HasColimit (CostructuredArrow.map (f ≫ g) ⋙ diagram ι F z)
j : CostructuredArrow ι x
ff : CostructuredArrow ι x ⥤ CostructuredArrow ι y := CostructuredArrow.map f
gg : CostructuredArrow ι y ⥤ CostructuredArrow ι z := CostructuredArrow.map g
dd : CostructuredArrow ι z ⥤ D := diagram ι F z
this✝¹ : HasColimit (ff ⋙ gg ⋙ dd)
this✝ : HasColimit ((ff ⋙ gg) ⋙ dd)
this : HasColimit (gg ⋙ dd)
⊢ (CostructuredArrow.map (f ≫ g)).obj j = (ff ⋙ gg).obj j
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
⊢ ∀ ⦃X Y : S⦄ (f_1 : X ⟶ Y),
    F.map f_1 ≫
        (fun x => colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)) Y =
      (fun x => colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)) X ≫
        (((whiskeringLeft S L D).obj ι).obj G).map f_1
[PROOFSTEP]
intro x y ff
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
⊢ F.map ff ≫
      (fun x => colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)) y =
    (fun x => colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)) x ≫
      (((whiskeringLeft S L D).obj ι).obj G).map ff
[PROOFSTEP]
dsimp only [whiskeringLeft]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
⊢ F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y))) ≫ NatTrans.app f (ι.obj y) =
    (colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)) ≫ (ι ⋙ G).map ff
[PROOFSTEP]
simp only [Functor.comp_map, Category.assoc]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
⊢ F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y))) ≫ NatTrans.app f (ι.obj y) =
    colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x) ≫ G.map (ι.map ff)
[PROOFSTEP]
rw [← f.naturality (ι.map ff), ← Category.assoc, ← Category.assoc]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    (colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ (loc ι F).map (ι.map ff)) ≫
      NatTrans.app f (ι.obj y)
[PROOFSTEP]
let fff : CostructuredArrow ι _ ⥤ _ :=
  CostructuredArrow.map
    (ι.map ff)
      -- same issue :-(
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    (colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ (loc ι F).map (ι.map ff)) ≫
      NatTrans.app f (ι.obj y)
[PROOFSTEP]
haveI : HasColimit (fff ⋙ diagram ι F (ι.obj y)) := I _
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff ⋙ diagram ι F (ι.obj y))
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    (colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ (loc ι F).map (ι.map ff)) ≫
      NatTrans.app f (ι.obj y)
[PROOFSTEP]
erw [colimit.ι_pre (diagram ι F (ι.obj y)) fff (CostructuredArrow.mk (𝟙 _))]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff ⋙ diagram ι F (ι.obj y))
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    colimit.ι (diagram ι F (ι.obj y)) (fff.obj (CostructuredArrow.mk (𝟙 (ι.obj x)))) ≫ NatTrans.app f (ι.obj y)
[PROOFSTEP]
let xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    colimit.ι (diagram ι F (ι.obj y)) (fff.obj (CostructuredArrow.mk (𝟙 (ι.obj x)))) ≫ NatTrans.app f (ι.obj y)
[PROOFSTEP]
let yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 _)
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 (ι.obj y))
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    colimit.ι (diagram ι F (ι.obj y)) (fff.obj (CostructuredArrow.mk (𝟙 (ι.obj x)))) ≫ NatTrans.app f (ι.obj y)
[PROOFSTEP]
let fff : xx ⟶ yy :=
  CostructuredArrow.homMk ff
    (by
      simp only [CostructuredArrow.mk_hom_eq_self]
      erw [Category.comp_id])
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 (ι.obj y))
⊢ ι.map ff ≫ yy.hom = xx.hom
[PROOFSTEP]
simp only [CostructuredArrow.mk_hom_eq_self]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 (ι.obj y))
⊢ ι.map ff ≫ 𝟙 (ι.obj y) = ι.map ff
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff✝ : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff✝ ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 (ι.obj y))
fff : xx ⟶ yy := CostructuredArrow.homMk ff
⊢ (F.map ff ≫ colimit.ι (diagram ι F (ι.obj y)) (CostructuredArrow.mk (𝟙 (ι.obj y)))) ≫ NatTrans.app f (ι.obj y) =
    colimit.ι (diagram ι F (ι.obj y)) (fff✝.obj (CostructuredArrow.mk (𝟙 (ι.obj x)))) ≫ NatTrans.app f (ι.obj y)
[PROOFSTEP]
erw [colimit.w (diagram ι F (ι.obj y)) fff]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff✝ : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff✝ ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 (ι.obj y))
fff : xx ⟶ yy := CostructuredArrow.homMk ff
⊢ colimit.ι (diagram ι F (ι.obj y)) xx ≫ NatTrans.app f (ι.obj y) =
    colimit.ι (diagram ι F (ι.obj y)) (fff✝.obj (CostructuredArrow.mk (𝟙 (ι.obj x)))) ≫ NatTrans.app f (ι.obj y)
[PROOFSTEP]
congr
[GOAL]
case e_a.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : loc ι F ⟶ G
x y : S
ff : x ⟶ y
fff✝ : CostructuredArrow ι (ι.obj x) ⥤ CostructuredArrow ι (ι.obj y) := CostructuredArrow.map (ι.map ff)
this : HasColimit (fff✝ ⋙ diagram ι F (ι.obj y))
xx : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (ι.map ff)
yy : CostructuredArrow ι (ι.obj y) := CostructuredArrow.mk (𝟙 (ι.obj y))
fff : xx ⟶ yy := CostructuredArrow.homMk ff
⊢ xx = fff✝.obj (CostructuredArrow.mk (𝟙 (ι.obj x)))
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : F ⟶ ((whiskeringLeft S L D).obj ι).obj G
⊢ ∀ ⦃X Y : L⦄ (f_1 : X ⟶ Y),
    (loc ι F).map f_1 ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) Y =
      (fun x => colimit.desc (diagram ι F x) (cocone x f)) X ≫ G.map f_1
[PROOFSTEP]
intro x y ff
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : F ⟶ ((whiskeringLeft S L D).obj ι).obj G
x y : L
ff : x ⟶ y
⊢ (loc ι F).map ff ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) y =
    (fun x => colimit.desc (diagram ι F x) (cocone x f)) x ≫ G.map ff
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : F ⟶ ((whiskeringLeft S L D).obj ι).obj G
x y : L
ff : x ⟶ y
⊢ ∀ (j : CostructuredArrow ι x),
    colimit.ι (diagram ι F x) j ≫ (loc ι F).map ff ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) y =
      colimit.ι (diagram ι F x) j ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) x ≫ G.map ff
[PROOFSTEP]
intros j
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : F ⟶ ((whiskeringLeft S L D).obj ι).obj G
x y : L
ff : x ⟶ y
j : CostructuredArrow ι x
⊢ colimit.ι (diagram ι F x) j ≫ (loc ι F).map ff ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) y =
    colimit.ι (diagram ι F x) j ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) x ≫ G.map ff
[PROOFSTEP]
haveI : HasColimit (CostructuredArrow.map ff ⋙ diagram ι F y) := I _
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : F ⟶ ((whiskeringLeft S L D).obj ι).obj G
x y : L
ff : x ⟶ y
j : CostructuredArrow ι x
this : HasColimit (CostructuredArrow.map ff ⋙ diagram ι F y)
⊢ colimit.ι (diagram ι F x) j ≫ (loc ι F).map ff ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) y =
    colimit.ι (diagram ι F x) j ≫ (fun x => colimit.desc (diagram ι F x) (cocone x f)) x ≫ G.map ff
[PROOFSTEP]
erw [colimit.pre_desc, ← Category.assoc, colimit.ι_desc, colimit.ι_desc]
[GOAL]
case w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
f : F ⟶ ((whiskeringLeft S L D).obj ι).obj G
x y : L
ff : x ⟶ y
j : CostructuredArrow ι x
this : HasColimit (CostructuredArrow.map ff ⋙ diagram ι F y)
⊢ NatTrans.app (Cocone.whisker (CostructuredArrow.map ff) (cocone y f)).ι j = NatTrans.app (cocone x f).ι j ≫ G.map ff
[PROOFSTEP]
simp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
⊢ Function.LeftInverse (fun f => NatTrans.mk fun x => colimit.desc (diagram ι F x) (cocone x f)) fun f =>
    NatTrans.mk fun x =>
      colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)
[PROOFSTEP]
intros x
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
⊢ (fun f => NatTrans.mk fun x => colimit.desc (diagram ι F x) (cocone x f))
      ((fun f =>
          NatTrans.mk fun x =>
            colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x))
        x) =
    x
[PROOFSTEP]
dsimp
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
⊢ (NatTrans.mk fun x_1 =>
      colimit.desc (diagram ι F x_1)
        { pt := G.obj x_1,
          ι :=
            NatTrans.mk fun i =>
              (colimit.ι (diagram ι F (ι.obj i.left)) (CostructuredArrow.mk (𝟙 (ι.obj i.left))) ≫
                  NatTrans.app x (ι.obj i.left)) ≫
                G.map i.hom }) =
    x
[PROOFSTEP]
ext k
[GOAL]
case w.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
⊢ NatTrans.app
      (NatTrans.mk fun x_1 =>
        colimit.desc (diagram ι F x_1)
          { pt := G.obj x_1,
            ι :=
              NatTrans.mk fun i =>
                (colimit.ι (diagram ι F (ι.obj i.left)) (CostructuredArrow.mk (𝟙 (ι.obj i.left))) ≫
                    NatTrans.app x (ι.obj i.left)) ≫
                  G.map i.hom })
      k =
    NatTrans.app x k
[PROOFSTEP]
dsimp
[GOAL]
case w.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
⊢ colimit.desc (diagram ι F k)
      { pt := G.obj k,
        ι :=
          NatTrans.mk fun i =>
            (colimit.ι (diagram ι F (ι.obj i.left)) (CostructuredArrow.mk (𝟙 (ι.obj i.left))) ≫
                NatTrans.app x (ι.obj i.left)) ≫
              G.map i.hom } =
    NatTrans.app x k
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
⊢ ∀ (j : CostructuredArrow ι k),
    colimit.ι (diagram ι F k) j ≫
        colimit.desc (diagram ι F k)
          { pt := G.obj k,
            ι :=
              NatTrans.mk fun i =>
                (colimit.ι (diagram ι F (ι.obj i.left)) (CostructuredArrow.mk (𝟙 (ι.obj i.left))) ≫
                    NatTrans.app x (ι.obj i.left)) ≫
                  G.map i.hom } =
      colimit.ι (diagram ι F k) j ≫ NatTrans.app x k
[PROOFSTEP]
intros j
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
⊢ colimit.ι (diagram ι F k) j ≫
      colimit.desc (diagram ι F k)
        { pt := G.obj k,
          ι :=
            NatTrans.mk fun i =>
              (colimit.ι (diagram ι F (ι.obj i.left)) (CostructuredArrow.mk (𝟙 (ι.obj i.left))) ≫
                  NatTrans.app x (ι.obj i.left)) ≫
                G.map i.hom } =
    colimit.ι (diagram ι F k) j ≫ NatTrans.app x k
[PROOFSTEP]
rw [colimit.ι_desc]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
⊢ NatTrans.app
      { pt := G.obj k,
          ι :=
            NatTrans.mk fun i =>
              (colimit.ι (diagram ι F (ι.obj i.left)) (CostructuredArrow.mk (𝟙 (ι.obj i.left))) ≫
                  NatTrans.app x (ι.obj i.left)) ≫
                G.map i.hom }.ι
      j =
    colimit.ι (diagram ι F k) j ≫ NatTrans.app x k
[PROOFSTEP]
dsimp only [cocone]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
⊢ (colimit.ι (diagram ι F (ι.obj j.left)) (CostructuredArrow.mk (𝟙 (ι.obj j.left))) ≫ NatTrans.app x (ι.obj j.left)) ≫
      G.map j.hom =
    colimit.ι (diagram ι F k) j ≫ NatTrans.app x k
[PROOFSTEP]
rw [Category.assoc, ← x.naturality j.hom, ← Category.assoc]
[GOAL]
case w.h.w
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
⊢ (colimit.ι (diagram ι F (ι.obj j.left)) (CostructuredArrow.mk (𝟙 (ι.obj j.left))) ≫ (loc ι F).map j.hom) ≫
      NatTrans.app x ((Functor.fromPUnit k).obj j.right) =
    colimit.ι (diagram ι F k) j ≫ NatTrans.app x k
[PROOFSTEP]
congr 1
[GOAL]
case w.h.w.e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
⊢ colimit.ι (diagram ι F (ι.obj j.left)) (CostructuredArrow.mk (𝟙 (ι.obj j.left))) ≫ (loc ι F).map j.hom =
    colimit.ι (diagram ι F k) j
[PROOFSTEP]
dsimp [loc]
[GOAL]
case w.h.w.e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
⊢ colimit.ι (diagram ι F (ι.obj j.left)) (CostructuredArrow.mk (𝟙 (ι.obj j.left))) ≫
      colimit.pre (diagram ι F k) (CostructuredArrow.map j.hom) =
    colimit.ι (diagram ι F k) j
[PROOFSTEP]
haveI : HasColimit (CostructuredArrow.map j.hom ⋙ diagram ι F k) := I _
[GOAL]
case w.h.w.e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
this : HasColimit (CostructuredArrow.map j.hom ⋙ diagram ι F k)
⊢ colimit.ι (diagram ι F (ι.obj j.left)) (CostructuredArrow.mk (𝟙 (ι.obj j.left))) ≫
      colimit.pre (diagram ι F k) (CostructuredArrow.map j.hom) =
    colimit.ι (diagram ι F k) j
[PROOFSTEP]
erw [colimit.ι_pre (diagram ι F k) (CostructuredArrow.map j.hom)]
[GOAL]
case w.h.w.e_a
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
this : HasColimit (CostructuredArrow.map j.hom ⋙ diagram ι F k)
⊢ colimit.ι (diagram ι F k) ((CostructuredArrow.map j.hom).obj (CostructuredArrow.mk (𝟙 (ι.obj j.left)))) =
    colimit.ι (diagram ι F k) j
[PROOFSTEP]
congr
[GOAL]
case w.h.w.e_a.h.e_7.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
j : CostructuredArrow ι k
this : HasColimit (CostructuredArrow.map j.hom ⋙ diagram ι F k)
⊢ (CostructuredArrow.map j.hom).obj (CostructuredArrow.mk (𝟙 (ι.obj j.left))) = j
[PROOFSTEP]
rcases j with ⟨_, ⟨⟩, _⟩
[GOAL]
case w.h.w.e_a.h.e_7.h.mk.mk
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
left✝ : S
as✝ : PUnit
hom✝ : ι.obj left✝ ⟶ (Functor.fromPUnit k).obj { as := as✝ }
this : HasColimit (CostructuredArrow.map { left := left✝, right := { as := as✝ }, hom := hom✝ }.hom ⋙ diagram ι F k)
⊢ (CostructuredArrow.map { left := left✝, right := { as := as✝ }, hom := hom✝ }.hom).obj
      (CostructuredArrow.mk (𝟙 (ι.obj { left := left✝, right := { as := as✝ }, hom := hom✝ }.left))) =
    { left := left✝, right := { as := as✝ }, hom := hom✝ }
[PROOFSTEP]
simp only [CostructuredArrow.map_mk, Category.id_comp]
[GOAL]
case w.h.w.e_a.h.e_7.h.mk.mk
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
x : loc ι F ⟶ G
k : L
left✝ : S
as✝ : PUnit
hom✝ : ι.obj left✝ ⟶ (Functor.fromPUnit k).obj { as := as✝ }
this : HasColimit (CostructuredArrow.map { left := left✝, right := { as := as✝ }, hom := hom✝ }.hom ⋙ diagram ι F k)
⊢ CostructuredArrow.mk hom✝ = { left := left✝, right := { as := as✝ }, hom := hom✝ }
[PROOFSTEP]
rfl
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝² : Category.{v₁, u₁} S
inst✝¹ : Category.{v₂, u₂} L
inst✝ : Category.{v₃, u₃} D
ι : S ⥤ L
F : S ⥤ D
I : ∀ (x : L), HasColimit (diagram ι F x)
G : L ⥤ D
⊢ Function.RightInverse (fun f => NatTrans.mk fun x => colimit.desc (diagram ι F x) (cocone x f)) fun f =>
    NatTrans.mk fun x =>
      colimit.ι (diagram ι F (ι.obj x)) (CostructuredArrow.mk (𝟙 (ι.obj x))) ≫ NatTrans.app f (ι.obj x)
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ ∀ (X : S ⥤ D) (Y Y' : L ⥤ D) (g : Y ⟶ Y') (h : Lan.loc ι X ⟶ Y),
    ↑((fun F G => Lan.equiv ι F G) X Y') (h ≫ g) =
      ↑((fun F G => Lan.equiv ι F G) X Y) h ≫ ((whiskeringLeft S L D).obj ι).map g
[PROOFSTEP]
{ intros X' X Y f g
  ext
  simp [Lan.equiv]
}
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ ∀ (X : S ⥤ D) (Y Y' : L ⥤ D) (g : Y ⟶ Y') (h : Lan.loc ι X ⟶ Y),
    ↑((fun F G => Lan.equiv ι F G) X Y') (h ≫ g) =
      ↑((fun F G => Lan.equiv ι F G) X Y) h ≫ ((whiskeringLeft S L D).obj ι).map g
[PROOFSTEP]
intros X' X Y f g
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
X' : S ⥤ D
X Y : L ⥤ D
f : X ⟶ Y
g : Lan.loc ι X' ⟶ X
⊢ ↑((fun F G => Lan.equiv ι F G) X' Y) (g ≫ f) =
    ↑((fun F G => Lan.equiv ι F G) X' X) g ≫ ((whiskeringLeft S L D).obj ι).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
S : Type u₁
L : Type u₂
D : Type u₃
inst✝³ : Category.{v₁, u₁} S
inst✝² : Category.{v₂, u₂} L
inst✝¹ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
X' : S ⥤ D
X Y : L ⥤ D
f : X ⟶ Y
g : Lan.loc ι X' ⟶ X
x✝ : S
⊢ NatTrans.app (↑((fun F G => Lan.equiv ι F G) X' Y) (g ≫ f)) x✝ =
    NatTrans.app (↑((fun F G => Lan.equiv ι F G) X' X) g ≫ ((whiskeringLeft S L D).obj ι).map f) x✝
[PROOFSTEP]
simp [Lan.equiv]
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ IsIso (adjunction D ι).unit
[PROOFSTEP]
suffices : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).unit X)
[GOAL]
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
this : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).unit X)
⊢ IsIso (adjunction D ι).unit
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).unit X)
[PROOFSTEP]
intro F
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
⊢ IsIso (NatTrans.app (adjunction D ι).unit F)
[PROOFSTEP]
suffices : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X)
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
this : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X)
⊢ IsIso (NatTrans.app (adjunction D ι).unit F)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
⊢ ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X)
[PROOFSTEP]
intro X
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X)
[PROOFSTEP]
dsimp [adjunction, equiv]
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (colimit.ι (diagram ι F (ι.obj X)) (CostructuredArrow.mk (𝟙 (ι.obj X))) ≫ 𝟙 (colimit (diagram ι F (ι.obj X))))
[PROOFSTEP]
simp only [Category.comp_id]
[GOAL]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category.{v₁, u₁} S
inst✝⁴ : Category.{v₂, u₂} L
inst✝³ : Category.{v₃, u₃} D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (colimit.ι (diagram ι F (ι.obj X)) (CostructuredArrow.mk (𝟙 (ι.obj X))))
[PROOFSTEP]
exact
  IsIso.of_iso
    ((colimit.isColimit _).coconePointUniqueUpToIso (colimitOfDiagramTerminal CostructuredArrow.mkIdTerminal _)).symm