-- Mathlib/CategoryTheory/Limits/Indization/IndObject.lean
theorem isIndObject_of_isFiltered_of_finallySmall (A : Cᵒᵖ ⥤ Type v)
    [IsFiltered (CostructuredArrow yoneda A)] [FinallySmall.{v} (CostructuredArrow yoneda A)] :
    IsIndObject A

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
⊢ IsIndObject A

Tactic:
let hc : IsColimit c := (Functor.Final.isColimitWhiskerEquiv _ _).symm
  (Presheaf.isColimitTautologicalCocone A)

Result:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
⊢ IsIndObject A

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A

Tactic:
let c := (Presheaf.tautologicalCocone A).whisker
  (inclusion (fromFinalModel (CostructuredArrow yoneda A)))

Result:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
⊢ IsIndObject A

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
⊢ IsIndObject A

Tactic:
have h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
    inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final := Functor.final_of_natIso
  (factoringCompInclusion (fromFinalModel <| CostructuredArrow yoneda A)).symm

Result:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
hq : Nonempty (FinalModel (CostructuredArrow yoneda A))
⊢ IsIndObject A

Tactic:
exact ⟨_, inclusion (fromFinalModel _) ⋙ CostructuredArrow.proj yoneda A, c.ι, hc⟩

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
⊢ IsIndObject A

Tactic:
have hq : Nonempty (FinalModel (CostructuredArrow yoneda A)) := Nonempty.map
  (Functor.Final.lift (fromFinalModel (CostructuredArrow yoneda A))) IsFiltered.nonempty

Result:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
hq : Nonempty (FinalModel (CostructuredArrow yoneda A))
⊢ IsIndObject A

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A

Tactic:
have h₂ : Functor.Final (inclusion (fromFinalModel (CostructuredArrow yoneda A))) :=
  Functor.final_of_comp_full_faithful' (factoring _) (inclusion _)

Result:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A