J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ (NatTrans.removeLeftOp c.π).app j = (c.π.app j.op).op
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ (coconeOfConeLeftOp c).ι.app j = (c.π.app j.op).op
dsimp only [coconeOfConeLeftOp]
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ (NatTrans.removeLeftOp c.π).app j = (c.π.app j.op).op
simp