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

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 ⋙ F)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
        (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.hom)

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 ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
            (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.hom)

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

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
  leftKanExtensionUniqueOfIso_hom, 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 ⋙ F)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
        (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.hom)

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 ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
          (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
            (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.hom)

Tactic:
aesop

Result:
no goals