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
fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }
x : P.obj (op X)
this :
  HasPullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
    (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X)
⊢ Eq (α :=
    P.obj
      (op
        (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
          (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X))))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (P.map
          (Quiver.Hom.op
            (pullback.snd (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X) ≫
              (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X)))))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (P.map (↑(fg.2.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.2.fst ⟶ X).op ≫
          P.map
            (Quiver.Hom.op
              (pullback.snd (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X)))))
      x)

Tactic:
simp
-- 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 : FirstObj P R
rw :
  Presieve.FamilyOfElements.PullbackCompatible (P := P) (R := R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
        x) ↔
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
⊢ Presieve.FamilyOfElements.Compatible (P := P) (R := R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
        x) ↔
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))

Tactic:
rw [Presieve.pullbackCompatible_iff]

Premises used: CategoryTheory.Presieve.pullbackCompatible_iff
-- 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 : FirstObj P R
mp :
  Presieve.FamilyOfElements.PullbackCompatible (P := P) (R := R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
        x) →
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
mpr :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R)) →
    Presieve.FamilyOfElements.PullbackCompatible (P := P) (R := R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
        x)
⊢ Presieve.FamilyOfElements.PullbackCompatible (P := P) (R := R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
        x) ↔
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P R))

Tactic:
constructor
-- 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
rw :
  Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
                (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
                (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            (fun (X : Type (max u v)) ↦ X) (SecondObj P R)) →
        ∃! x : P.obj (op X),
          Eq (α := (fun (X : Type (max u v)) ↦ X) (FirstObj P R))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) :
                  (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) → (fun (X : Type (max u v)) ↦ X) (FirstObj P R))
                x :
              (fun (X : Type (max u v)) ↦ X) (FirstObj P R))
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)
⊢ Presieve.IsSheafFor P R ↔
    Nonempty
      (IsLimit (F := parallelPair (Y := SecondObj P R) (firstMap P R) (secondMap P R)) (Fork.ofι (forkMap P R) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique,
    ← Equiv.forall_congr_right (firstObjEqFamily P R).toEquiv.symm]

Premises used: CategoryTheory.Iso.toEquiv, Equiv.symm, Equiv.forall_congr_right, CategoryTheory.Equalizer.firstObjEqFamily, CategoryTheory.Limits.Types.type_equalizer_iff_unique
-- 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
simp_rw :
  Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Presieve.FamilyOfElements.Compatible (P := P) (R := R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
                (a : FirstObj P R) → Presieve.FamilyOfElements P R)
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            Presieve.FamilyOfElements P R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
                (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
                (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            (fun (X : Type (max u v)) ↦ X) (SecondObj P R)) →
        ∃! x : P.obj (op X),
          Eq (α := (fun (X : Type (max u v)) ↦ X) (FirstObj P R))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) :
                  (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) → (fun (X : Type (max u v)) ↦ X) (FirstObj P R))
                x :
              (fun (X : Type (max u v)) ↦ X) (FirstObj P R))
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)

Tactic:
simp_rw [← compatible_iff]

Premises used: CategoryTheory.Equalizer.Presieve.compatible_iff
-- 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
enter :
  ∀ (a : Presieve.FamilyOfElements P R),
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
          (a : FirstObj P R) → Presieve.FamilyOfElements P R)
        (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
      Presieve.FamilyOfElements P R)
| Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Presieve.FamilyOfElements.Compatible (P := P) (R := R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
                (a : FirstObj P R) → Presieve.FamilyOfElements P R)
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            Presieve.FamilyOfElements P R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)

Tactic:
enter [2, a, 1, 1]
-- 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
a : Presieve.FamilyOfElements P R
rw :
  (((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
      (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
    Presieve.FamilyOfElements P R)
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
        (a : FirstObj P R) → Presieve.FamilyOfElements P R)
      (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
    Presieve.FamilyOfElements P R)

Tactic:
rw [← Iso.toEquiv_apply]

Premises used: CategoryTheory.Iso.toEquiv_apply
-- 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
enter :
  ∀ (a : Presieve.FamilyOfElements P R),
    (((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
        (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
      Presieve.FamilyOfElements P R)
| Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Presieve.FamilyOfElements.Compatible (P := P) (R := R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
                (a : FirstObj P R) → Presieve.FamilyOfElements P R)
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            Presieve.FamilyOfElements P R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)

Tactic:
enter [2, a, 1, 1]; rw [← Iso.toEquiv_apply]

Premises used: CategoryTheory.Iso.toEquiv_apply
-- 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
conv :
  Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Presieve.FamilyOfElements.Compatible (P := P) (R := R)
          (((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            Presieve.FamilyOfElements P R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Presieve.FamilyOfElements.Compatible (P := P) (R := R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
                (a : FirstObj P R) → Presieve.FamilyOfElements P R)
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            Presieve.FamilyOfElements P R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)

Tactic:
conv => enter [2, a, 1, 1]; rw [← Iso.toEquiv_apply]

Premises used: CategoryTheory.Iso.toEquiv_apply
-- 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
simp_rw :
  Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      a.Compatible (R := R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      Presieve.FamilyOfElements.Compatible (P := P) (R := R)
          (((firstObjEqFamily P R).toEquiv : (a : FirstObj P R) → Presieve.FamilyOfElements P R)
              (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a) :
            Presieve.FamilyOfElements P R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)

Tactic:
simp_rw [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- 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
h :
  ∀ (a : Presieve.FamilyOfElements P R) (b : a.Compatible (R := R)),
    (∃! t : P.obj (op X), a.IsAmalgamation (R := R) t) ↔
      ∃! x : P.obj (op X),
        Eq (α := FirstObj P R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
            FirstObj P R)
          (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a : FirstObj P R)
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      a.Compatible (R := R) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P R)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x :
              FirstObj P R)
            (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) a :
              FirstObj P R)

Tactic:
apply forall₂_congr

Premises used: forall₂_congr
-- 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
h :
  x.Compatible (R := R) →
    ((∃! t : P.obj (op X), x.IsAmalgamation (R := R) t) ↔
      ∃! x_1 : P.obj (op X),
        Eq (α := FirstObj P R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x_1 :
            FirstObj P R)
          (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) x : FirstObj P R))
⊢ ∀ (b : x.Compatible (R := R)),
    (∃! t : P.obj (op X), x.IsAmalgamation (R := R) t) ↔
      ∃! x_1 : P.obj (op X),
        Eq (α := FirstObj P R)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x_1 :
            FirstObj P R)
          (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) x : FirstObj P R)

Tactic:
_
-- 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)
h :
  ∀ (a : P.obj (op X)),
    x.IsAmalgamation (R := R) a ↔
      Eq (α := FirstObj P R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) a : FirstObj P R)
        (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) x : FirstObj P R)
⊢ (∃! t : P.obj (op X), x.IsAmalgamation (R := R) t) ↔
    ∃! x_1 : P.obj (op X),
      Eq (α := FirstObj P R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) x_1 :
          FirstObj P R)
        (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) x : FirstObj P R)

Tactic:
apply existsUnique_congr

Premises used: existsUnique_congr
-- 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)
h :
  x.IsAmalgamation (R := R) t ↔
    ((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
⊢ x.IsAmalgamation (R := R) t ↔
    Eq (α := FirstObj P R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P R) : (a : P.obj (op X)) → FirstObj P R) t : FirstObj P R)
      (((firstObjEqFamily P R).toEquiv.symm : (a : Presieve.FamilyOfElements P R) → FirstObj P R) x : FirstObj P R)

Tactic:
rw [Equiv.eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- 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)
h :
  x.IsAmalgamation (R := R) t →
    ((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
h₁ :
  ((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 →
    x.IsAmalgamation (R := R) t
⊢ x.IsAmalgamation (R := R) t ↔
    ((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

Tactic:
constructor
-- 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 : x.IsAmalgamation (R := R) t
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    ((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 =
      x f hf
⊢ ((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

Tactic:
funext Y f hf
-- 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 : x.IsAmalgamation (R := R) t
Y : C
f : Y ⟶ X
hf : R f
⊢ ((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 =
    x f hf

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

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Equalizer.forkMap