-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ Eq (α :=
    Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ⟶
      Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) d)
    (CategoryTheory.Functor.map (coneEquivInverse F U ⋙ coneEquivFunctor F U) f ≫
      Iso.hom
        ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
            {
              hom :=
                {
                  hom :=
                    𝟙
                      (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                        (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                  w := ⋯ },
              inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := ⋯ },
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
          d))
    (Iso.hom
        ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
            {
              hom :=
                {
                  hom :=
                    𝟙
                      (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                        (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                  w := ⋯ },
              inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := ⋯ },
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
          c) ≫
      CategoryTheory.Functor.map (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) f)
have w : Eq (α :=
  Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
      (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c) ⟶
    (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) d).pt)
  (ConeMorphism.hom
    (CategoryTheory.Functor.map (coneEquivInverse F U ⋙ coneEquivFunctor F U) f ≫
      Iso.hom
        ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
            {
              hom :=
                {
                  hom :=
                    𝟙
                      (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                        (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                  w := sorry },
              inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := sorry },
              hom_inv_id := sorry, inv_hom_id := sorry :
              Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
          d)))
  (ConeMorphism.hom
    (Iso.hom
        ((fun (c : Cone (SheafConditionEqualizerProducts.diagram F U)) ↦
            {
              hom :=
                {
                  hom :=
                    𝟙
                      (Cone.pt (F := SheafConditionEqualizerProducts.diagram F U)
                        (Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c)),
                  w := sorry },
              inv := { hom := 𝟙 (Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c).pt, w := sorry },
              hom_inv_id := sorry, inv_hom_id := sorry :
              Functor.obj (coneEquivInverse F U ⋙ coneEquivFunctor F U) c ≅
                Functor.obj (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) c })
          c) ≫
      CategoryTheory.Functor.map (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))) f))
Tactic: ext