[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map
          f ≫
        (fun j => homMk (NatTrans.app c.π j)) Y =
      (fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f
[PROOFSTEP]
intro X Y f
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
      (fun j => homMk (NatTrans.app c.π j)) Y =
    (fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        (fun j => homMk (NatTrans.app c.π j)) Y).left =
    ((fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f).left
[PROOFSTEP]
simpa using (c.w f).symm
[GOAL]
case right
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        (fun j => homMk (NatTrans.app c.π j)) Y).right =
    ((fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f).right
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
⊢ (forget B).mapCone (raiseCone c) = c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
⊢ m = (fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s
[PROOFSTEP]
ext1
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
⊢ m.left = ((fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s).left
[PROOFSTEP]
apply t.hom_ext
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J),
    m.left ≫ NatTrans.app c.π j = ((fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s).left ≫ NatTrans.app c.π j
[PROOFSTEP]
intro j
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
j : J
⊢ m.left ≫ NatTrans.app c.π j = ((fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s).left ≫ NatTrans.app c.π j
[PROOFSTEP]
simp [← K j]
