-- Mathlib/CategoryTheory/Limits/Indization/LocallySmall.lean
theorem colimitYonedaHomEquiv_π_apply (η : colimit (F ⋙ yoneda) ⟶ G) (i : Iᵒᵖ) :
    limit.π (F.op ⋙ G) i (colimitYonedaHomEquiv F G η) =
      η.app (op (F.obj i.unop)) ((colimit.ι (F ⋙ yoneda) i.unop).app _ (𝟙 _))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    limit.π (F.op ⋙ G) i ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv a).down =
      (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i a).down
⊢ limit.π (F.op ⋙ G) i
      ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv
          ((HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom
            ((colimitYonedaHomIsoLimitOp F G).hom η))).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Tactic:
rw [this, ← types_comp_apply (HasLimit.isoOfNatIso _).hom (limit.π _ _),
  HasLimit.isoOfNatIso_hom_π]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    limit.π (F.op ⋙ G) i ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv a).down =
      (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i a).down
⊢ ((limit.π (F.op ⋙ G ⋙ uliftFunctor.{u, v}) i ≫ (F.op.associator G uliftFunctor.{u, v}).symm.hom.app i)
        ((colimitYonedaHomIsoLimitOp F G).hom η)).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ limit.π (F.op ⋙ G) i
      ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv
          ((HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom
            ((colimitYonedaHomIsoLimitOp F G).hom η))).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Tactic:
have (a) := congrArg ULift.down
  (congrFun (preservesLimitIso_inv_π uliftFunctor.{u, v} (F.op ⋙ G) i) a)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    (((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)) a).down =
      (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i a).down
⊢ limit.π (F.op ⋙ G) i
      ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv
          ((HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom
            ((colimitYonedaHomIsoLimitOp F G).hom η))).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    (((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)) a).down =
      (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i a).down
⊢ limit.π (F.op ⋙ G) i
      ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv
          ((HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom
            ((colimitYonedaHomIsoLimitOp F G).hom η))).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Tactic:
dsimp at this

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    limit.π (F.op ⋙ G) i ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv a).down =
      (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i a).down
⊢ limit.π (F.op ⋙ G) i
      ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv
          ((HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom
            ((colimitYonedaHomIsoLimitOp F G).hom η))).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ limit.π (F.op ⋙ G) i ((colimitYonedaHomEquiv F G) η) =
    η.app (op (F.obj (unop i)))
      ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (unop (op (F.obj (unop i))))))

Tactic:
simp only [Functor.comp_obj, Functor.op_obj, colimitYonedaHomEquiv, uliftFunctor_obj,
  Iso.instTransIso_trans, Iso.trans_assoc, Iso.toEquiv_comp, Equiv.symm_trans_apply,
  Equiv.symm_symm, Equiv.trans_apply, Iso.toEquiv_fun, Iso.symm_hom, Equiv.ulift_apply]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ limit.π (F.op ⋙ G) i
      ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv
          ((HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom
            ((colimitYonedaHomIsoLimitOp F G).hom η))).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    limit.π (F.op ⋙ G) i ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv a).down =
      (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i a).down
⊢ ((limit.π (F.op ⋙ G ⋙ uliftFunctor.{u, v}) i ≫ (F.op.associator G uliftFunctor.{u, v}).symm.hom.app i)
        ((colimitYonedaHomIsoLimitOp F G).hom η)).down =
    η.app (op (F.obj (unop i))) ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))) (𝟙 (F.obj (unop i))))

Tactic:
simp

Result:
no goals