-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
rw :
  (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : P.obj (op B),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t =
              x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      Eq (α := SecondObj P X π)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
                (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
              (((Equiv.trans (β := Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                        (equivShrink ((j : I) → P.obj (op (X j))) :
                          ((j : I) → P.obj (op (X j))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                        (Equiv.symm (Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                          Shrink.{w, max w t} ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                      ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                    (a : (j : I) → P.obj (op (X j))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                  a :
                ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
            SecondObj P X π)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
                (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
              (((Equiv.trans (β := Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                        (equivShrink ((j : I) → P.obj (op (X j))) :
                          ((j : I) → P.obj (op (X j))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                        (Equiv.symm (Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                          Shrink.{w, max w t} ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                      ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                    (a : (j : I) → P.obj (op (X j))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                  a :
                ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
            SecondObj P X π) →
        ∃! x : P.obj (op B),
          Eq (α := ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                x :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
            (((Equiv.trans (β := Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                      (equivShrink ((j : I) → P.obj (op (X j))) :
                        ((j : I) → P.obj (op (X j))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                      (Equiv.symm (Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                        Shrink.{w, max w t} ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                    ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                  (a : (j : I) → P.obj (op (X j))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                a :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : P.obj (op B),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t =
              x i) ↔
    ∀ (y : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))),
      Eq (α := SecondObj P X π)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
                (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
              y :
            SecondObj P X π)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
                (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
              y :
            SecondObj P X π) →
        ∃! x : P.obj (op B),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              x =
            y

Tactic:
rw [← Equiv.forall_congr_right ((equivShrink _).trans (Types.Small.productIso _).toEquiv.symm)]

Premises used: CategoryTheory.Iso.toEquiv, Equiv.trans, Equiv.symm, Equiv.forall_congr_right, equivShrink, CategoryTheory.Limits.Types.Small.productIso