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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  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 π))
i j : I
⊢ Eq (α :=
    (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).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))))
              (i, j)) :
          (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 (π (i, j).1) (π (i, j).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 (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).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))))
              (i, j)) :
          (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 (π (i, j).1) (π (i, j).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 (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).2)))))

Tactic:
apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.Pi.π, Prod.mk, Prod.fst, Opposite.op, Prod.snd, CategoryTheory.Functor.obj
-- 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 : FirstObj P X
rw :
  Arrows.PullbackCompatible P π
      ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
          (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
              (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
            x :
          (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))) ↔
    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 π
      ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
          (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
              (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
            x :
          (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))) ↔
    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 t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π
      ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
          (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
              (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
            x :
          (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))) ↔
    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:
⟨fun t ↦ ?_, fun t i j ↦ ?_⟩

Premises used: Iff.intro
-- 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 : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
        (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
      (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
              TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
          x :
        (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))))
refine_1 :
  ∀ (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 t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
        (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
      (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
              TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
          x :
        (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))))
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
-- 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 : FirstObj P X
t :
  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 π))
i j : I
⊢ Eq (α :=
    (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).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))))
              (i, j)) :
          (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 (π (i, j).1) (π (i, j).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 (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).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))))
              (i, j)) :
          (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 (π (i, j).1) (π (i, j).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 (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).2)))))

Tactic:
apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.Pi.π, Prod.mk, Prod.fst, Opposite.op, Prod.snd, CategoryTheory.Functor.obj
-- 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 : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    ∀ (y : FirstObj P 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 π))
              y :
            (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 π))
              y :
            (fun (X : Type w) ↦ X) (SecondObj P X π)) →
        ∃! x : P.obj (op B),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (FirstObj P X))
              x =
            y
⊢ IsSheafFor P (Presieve.ofArrows X π) ↔
    Nonempty
      (IsLimit (F := parallelPair (X := FirstObj P X) (Y := SecondObj P X π) (firstMap P X π) (secondMap P X π))
        (Fork.ofι (forkMap P X π) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique, isSheafFor_arrows_iff]

Premises used: CategoryTheory.Presieve.isSheafFor_arrows_iff, CategoryTheory.Limits.Types.type_equalizer_iff_unique
-- 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
simp :
  (∀ (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
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    ∀ (y : FirstObj P 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 π))
              y :
            (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 π))
              y :
            (fun (X : Type w) ↦ X) (SecondObj P X π)) →
        ∃! x : P.obj (op B),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (FirstObj P X))
              x =
            y

Tactic:
simp only [FirstObj]

Premises used: CategoryTheory.Equalizer.Presieve.Arrows.FirstObj
-- 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 :
  ∀ (a : (i : I) → P.obj (op (X i))) (b : Arrows.Compatible P π a),
    (∃! 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 = a i) ↔
      ∃! 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.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))))
                  a :
                Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            ∏ᶜ 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) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      Arrows.Compatible P π a →
        ∃! 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.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))))
                    a :
                  Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))

Tactic:
apply forall₂_congr

Premises used: forall₂_congr