awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b : x.Compatible (R := R)
t : P.obj (op X)
q :
  ((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) t) =
    x
Y : C
f : Y ⟶ X
hf : R f
h :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) → (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
        t :
      (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
    (((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) t) f hf :
      P.obj (op Y))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
        (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) → (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
      t =
    x f hf

Tactic:
rw [← q]
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b : x.Compatible (R := R)
t : P.obj (op X)
q :
  ((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) t) =
    x
Y : C
f : Y ⟶ X
hf : R f
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) → (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
        t :
      (fun (X : Type (max u v)) ↦ X) (P.obj (op Y)))
    (((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) t) f hf :
      P.obj (op Y))

Tactic:
simp [Iso.toEquiv, forkMap]

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Equalizer.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)
I : Type t
inst_1 : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₁ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₂ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
w :
  ∀ (j : Discrete I),
    Eq (α := (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j) :
            (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
              (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj j))
          z₁ :
        (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j) :
            (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
              (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj j))
          z₂ :
        (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j))
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Premises used: CategoryTheory.Limits.Types.limit_ext
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type t
inst_1 : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₁ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₂ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
i : I
⊢ Eq (α :=
    (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }) :
          (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
            (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj { as := i }))
        z₁ :
      (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }) :
          (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
            (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj { as := i }))
        z₂ :
      (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }))

Tactic:
h 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)
I : Type t
inst_1 : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₁ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₂ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
i : I
⊢ Eq (α :=
    (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }) :
          (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
            (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj { as := i }))
        z₁ :
      (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }) :
          (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
            (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj { as := i }))
        z₂ :
      (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) { as := i : Discrete I }))

Tactic:
exact h 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
h :
  ∀ (x : I × I) (ij : P.obj (op B)),
    Eq (α := P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
              (forkMap P X π ≫ firstMap P X π : P.obj (op B) ⟶ SecondObj P X π)
              (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x)))
          ij :
        P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
              (forkMap P X π ≫ secondMap P X π : P.obj (op B) ⟶ SecondObj P X π)
              (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x)))
          ij :
        P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
⊢ Eq (α := P.obj (op B) ⟶ SecondObj P X π) (forkMap P X π ≫ firstMap P X π) (forkMap P X π ≫ secondMap P X π)

Tactic:
ext x ij
-- 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
ij : P.obj (op B)
⊢ Eq (α := P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x) :
          (a : ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) →
            P.obj (op (Limits.pullback (π x.1) (π x.2))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Pi.lift (f := fun (ij : I × I) ↦
                  P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) fun (x : I × I) ↦
                  Pi.π (fun (i : I) ↦ P.obj (op (X i))) x.1 ≫ P.map (Quiver.Hom.op (pullback.fst (π x.1) (π x.2)))) :
              (a : FirstObj P X) → ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Pi.lift (f := fun (i : I) ↦ P.obj (op (X i))) fun (i : I) ↦ P.map (π i).op) :
                  (a : P.obj (op B)) → FirstObj P X)
                ij :
              FirstObj P X) :
          ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) :
      P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x) :
          (a : ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) →
            P.obj (op (Limits.pullback (π x.1) (π x.2))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Pi.lift (f := fun (ij : I × I) ↦
                  P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) fun (x : I × I) ↦
                  Pi.π (fun (i : I) ↦ P.obj (op (X i))) x.2 ≫ P.map (Quiver.Hom.op (pullback.snd (π x.1) (π x.2)))) :
              (a : FirstObj P X) → ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Pi.lift (f := fun (i : I) ↦ P.obj (op (X i))) fun (i : I) ↦ P.map (π i).op) :
                  (a : P.obj (op B)) → FirstObj P X)
                ij :
              FirstObj P X) :
          ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) :
      P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))

Tactic:
simp [← comp_apply, -types_comp_apply, ← Functor.map_comp, ← op_comp, pullback.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition, CategoryTheory.types_comp_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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
rw :
  Arrows.PullbackCompatible P π
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
        x) ↔
    Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
⊢ Arrows.Compatible P π
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
        x) ↔
    Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))

Tactic:
rw [Arrows.pullbackCompatible_iff]

Premises used: CategoryTheory.Presieve.Arrows.pullbackCompatible_iff
-- 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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
mp :
  Arrows.PullbackCompatible P π
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
        x) →
    Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
mpr :
  Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π)) →
    Arrows.PullbackCompatible P π
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
        x)
⊢ Arrows.PullbackCompatible P π
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
        x) ↔
    Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P 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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
        (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
          (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
      x)
mp :
  ∀ (ij : I × I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
                ij) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
                (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
              x :
            (fun (X : Type w) ↦ X) (SecondObj P X π)) :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
                ij) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
                (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
              x :
            (fun (X : Type w) ↦ X) (SecondObj P X π)) :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
⊢ Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
          (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
        x :
      (fun (X : Type w) ↦ X) (SecondObj P X π))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
          (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
        x :
      (fun (X : Type w) ↦ X) (SecondObj P X π))

Tactic:
ext ij
-- 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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
        (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
          (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
      x)
ij : I × I
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) ij) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
              (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
            x :
          (fun (X : Type w) ↦ X) (SecondObj P X π)) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) ij) :
          (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
              (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
            x :
          (fun (X : Type w) ↦ X) (SecondObj P X π)) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))

Tactic:
simpa [firstMap, secondMap] using t ij.1 ij.2

Premises used: Prod.fst, CategoryTheory.Equalizer.Presieve.Arrows.firstMap, CategoryTheory.Equalizer.Presieve.Arrows.secondMap, Prod.snd