-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
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
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 := ⋯ },
                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)))
    (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 := ⋯ },
                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))
⊢ 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)

Tactic:
ext