-- Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean
theorem isIndObject_limit_comp_yoneda_comp_colim
    (hF : ∀ i, IsIndObject (limit (F.flip.obj i ⋙ yoneda))) :
    IsIndObject (limit (F ⋙ (whiskeringRight _ _ _).obj yoneda ⋙ colim))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (limit (F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda ⋙ colim))

Tactic:
apply IsIndObject.map (HasLimit.isoOfNatIso (colimitFlipIsoCompColim G)).hom

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (limit (colimit G.flip))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
⊢ IsIndObject (limit (F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda ⋙ colim))

Tactic:
let G : J ⥤ I ⥤ (Cᵒᵖ ⥤ Type v) := F ⋙ (whiskeringRight _ _ _).obj yoneda

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (limit (F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda ⋙ colim))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (limit (colimit G.flip))

Tactic:
apply IsIndObject.map (colimitLimitIso G).hom

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (colimit (limit G))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (colimit (limit G))

Tactic:
apply isIndObject_colimit

Result:
case hF
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ ∀ (i : I), IsIndObject ((limit G).obj i)

Proof state:
case hF
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ ∀ (i : I), IsIndObject ((limit G).obj i)

Tactic:
exact fun i => IsIndObject.map (limitObjIsoLimitCompEvaluation _ _).inv (hF i)

Result:
no goals