awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)
⊢ 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 π))
have 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)))))
Tactic: ext ij
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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.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 π))
have 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 π))
Tactic: rw [Arrows.pullbackCompatible_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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 π))
have refine_1 : ∀
  (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))))))),
  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: refine ⟨fun t ↦ ?_, fun t i j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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))))))
⊢ 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 π))
have 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)))))
Tactic: ext ij
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ 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 π) ⋯))
have 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
Tactic: rw [Types.type_equalizer_iff_unique, isSheafFor_arrows_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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))),
      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
have 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
Tactic: simp only [FirstObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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))),
      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)))
have 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)))
Tactic: apply forall₂_congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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),
      ∀ (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)))
have 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)))
Tactic: apply existsUnique_congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)
⊢ (∀ (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)))
have 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
Tactic: rw [Equiv.eq_symm_apply, ← Equiv.symm_apply_eq]