awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : (i : I) → P.obj (op (X i))
h :
  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) ↔
      ∃! x_1 : 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_1 :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
          (((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))) :
                (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              ((equivShrink ((j : I) → P.obj (op (X j))) :
                    (a : (j : I) → P.obj (op (X j))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                  x :
                Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))))
⊢ ∀ (b : 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) ↔
      ∃! x_1 : 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_1 :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
          (((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))) :
                (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              ((equivShrink ((j : I) → P.obj (op (X j))) :
                    (a : (j : I) → P.obj (op (X j))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                  x :
                Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))

Tactic:
_
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
h :
  ∀ (a : 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))) a = x i) ↔
      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)))
            a :
          ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
        (((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))) :
              (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
            ((equivShrink ((j : I) → P.obj (op (X j))) :
                  (a : (j : I) → P.obj (op (X j))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                x :
              Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
          ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
⊢ (∃! 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) ↔
    ∃! x_1 : 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_1 :
          ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
        (((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))) :
              (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
            ((equivShrink ((j : I) → P.obj (op (X j))) :
                  (a : (j : I) → P.obj (op (X j))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                x :
              Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
          ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))

Tactic:
apply existsUnique_congr

Premises used: existsUnique_congr
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
h :
  (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) ↔
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x
⊢ (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) ↔
    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)))
          t :
        ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
      (((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))) :
            (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
          ((equivShrink ((j : I) → P.obj (op (X j))) :
                (a : (j : I) → P.obj (op (X j))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
              x :
            Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
        ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))

Tactic:
rw [Equiv.eq_symm_apply, ← Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq, Equiv.eq_symm_apply
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
h :
  (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) →
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x
h₁ :
  (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x →
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i
⊢ (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) ↔
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x

Tactic:
constructor
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
q :
  ∀ (i : I), (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i
h :
  ∀ (i : I),
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
        i =
      x i
⊢ (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x

Tactic:
funext i
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
q :
  ∀ (i : I), (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i
i : I
⊢ (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
      i =
    x i

Tactic:
simpa [Iso.toEquiv, forkMap] using q i

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Equalizer.Presieve.Arrows.forkMap
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x
i : I
h :
  Eq (α := P.obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t :
      P.obj (op (X i)))
    ((Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
        i :
      P.obj (op (X i)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i

Tactic:
rw [← q]
-- 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
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x
i : I
⊢ Eq (α := P.obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t :
      P.obj (op (X i)))
    ((Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
        i :
      P.obj (op (X i)))

Tactic:
simp [Iso.toEquiv, forkMap]

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Equalizer.Presieve.Arrows.forkMap
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X_1 : C
R : Presieve.{v, u} X_1
S : Sieve.{v, u} X_1
inst_1 : R.HasPairwisePullbacks
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ F.map f.op ≫ F.map c.fst.op = F.map f.op ≫ F.map c.snd.op

Tactic:
simp [← Functor.map_comp, ← op_comp, c.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
⊢ (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f →
        Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
              x :
            (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
              x :
            (fun (X : Type u_1) ↦ X) (F.obj (op Z)))) ↔
    Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
          x :
        (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
          x :
        (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))

Tactic:
⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.PullbackCone.fst, Iff.intro, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
refine :
  ∀
    (H :
      Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt))))
    (Z : C) (p₁ p₂ : Z ⟶ X) (h : p₁ ≫ f = p₂ ≫ f),
    Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
          x :
        (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
          x :
        (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
⊢ (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f →
        Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
              x :
            (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
              x :
            (fun (X : Type u_1) ↦ X) (F.obj (op Z)))) ↔
    Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
          x :
        (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
          x :
        (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))

Tactic:
refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩