-- Mathlib/Condensed/Discrete/Colimit.lean
lemma isoFinYonedaComponents_inv_comp {X Y : LightProfinite.{u}} [Finite X] [Finite Y]
    (f : Y → F.obj ⟨LightProfinite.of PUnit⟩) (g : X ⟶ Y) :
    (isoFinYonedaComponents F X).inv (f ∘ g) = F.map g.op ((isoFinYonedaComponents F Y).inv f)

Proof state:
case a.h
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (isoFinYonedaComponents F X).hom (F.map g.op ((isoFinYonedaComponents F Y).inv f)) x

Tactic:
rw [isoFinYonedaComponents_hom_apply]

Result:
case a.h
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op (F.map g.op ((isoFinYonedaComponents F Y).inv f))

Proof state:
case a
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ f ∘ ⇑(ConcreteCategory.hom g) = (isoFinYonedaComponents F X).hom (F.map g.op ((isoFinYonedaComponents F Y).inv f))

Tactic:
ext x

Result:
case a.h
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (isoFinYonedaComponents F X).hom (F.map g.op ((isoFinYonedaComponents F Y).inv f)) x

Proof state:
case a.h
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op (F.map g.op ((isoFinYonedaComponents F Y).inv f))

Tactic:
simp only [← FunctorToTypes.map_comp_apply, ← op_comp, CompHausLike.const_comp,
  ← isoFinYonedaComponents_hom_apply, CategoryTheory.inv_hom_id_apply, Function.comp_apply]

Result:
no goals

Proof state:
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (isoFinYonedaComponents F X).inv (f ∘ ⇑(ConcreteCategory.hom g)) = F.map g.op ((isoFinYonedaComponents F Y).inv f)

Tactic:
apply injective_of_mono (isoFinYonedaComponents F X).hom

Result:
case a
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (isoFinYonedaComponents F X).hom ((isoFinYonedaComponents F X).inv (f ∘ ⇑(ConcreteCategory.hom g))) =
    (isoFinYonedaComponents F X).hom (F.map g.op ((isoFinYonedaComponents F Y).inv f))

Proof state:
case a
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (isoFinYonedaComponents F X).hom ((isoFinYonedaComponents F X).inv (f ∘ ⇑(ConcreteCategory.hom g))) =
    (isoFinYonedaComponents F X).hom (F.map g.op ((isoFinYonedaComponents F Y).inv f))

Tactic:
simp only [CategoryTheory.inv_hom_id_apply]

Result:
case a
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ f ∘ ⇑(ConcreteCategory.hom g) = (isoFinYonedaComponents F X).hom (F.map g.op ((isoFinYonedaComponents F Y).inv f))