-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafExt_inv  {F G : LightProfinite.{u}ᵒᵖ ⥤ Type u} (S : LightProfinite.{u}ᵒᵖ)
    (i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G) : (lanPresheafExt i).inv.app S =
      colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.inv)

Proof state:
case w
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
            (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.inv)

Tactic:
aesop

Result:
no goals

Proof state:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ (lanPresheafExt i).inv.app S = colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.inv)

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
  leftKanExtensionUniqueOfIso_inv, pointwiseLeftKanExtension_desc_app]

Result:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
        (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.inv)

Proof state:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
        (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.inv)

Tactic:
apply colimit.hom_ext

Result:
case w
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
            (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.inv)