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

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

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

Tactic:
simp_rw [← compatible_iff]

Premises used: CategoryTheory.Equalizer.Sieve.compatible_iff
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
enter :
  ∀ (a : Presieve.FamilyOfElements P S.arrows),
    (((firstObjEqFamily P S.arrows).toEquiv.symm : (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows) a :
      FirstObj P S.arrows)
| Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
                (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
              (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a) :
            Presieve.FamilyOfElements P S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)

Tactic:
enter [2, a, 1, 1, 2]
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
enter :
  ∀ (a : Presieve.FamilyOfElements P S.arrows),
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).inv :
          (a : (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
        a :
      (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
| Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
                (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
              (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a) :
            Presieve.FamilyOfElements P S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)

Tactic:
enter [2, a, 1, 1, 2]; rw [(firstObjEqFamily P S.arrows).toEquiv_symm_apply]

Premises used: CategoryTheory.Sieve.arrows, CategoryTheory.Iso.toEquiv_symm_apply, CategoryTheory.Equalizer.firstObjEqFamily
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
simp :
  Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      a.Compatible (R := S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
                (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).inv :
                  (a : (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows)) →
                    (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
                a) :
            Presieve.FamilyOfElements P S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)

Tactic:
simp only [Iso.inv_hom_id_apply]

Premises used: CategoryTheory.Iso.inv_hom_id_apply
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
h :
  ∀ (a : Presieve.FamilyOfElements P S.arrows) (b : a.Compatible (R := S.arrows)),
    (∃! t : P.obj (op X), a.IsAmalgamation (R := S.arrows) t) ↔
      ∃! x : P.obj (op X),
        Eq (α := FirstObj P S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
              x :
            FirstObj P S.arrows)
          (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a :
            FirstObj P S.arrows)
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      a.Compatible (R := S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)

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

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
h :
  ∀ (a : P.obj (op X)),
    x.IsAmalgamation (R := S.arrows) a ↔
      Eq (α := FirstObj P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) a :
          FirstObj P S.arrows)
        (((firstObjEqFamily P S.arrows).toEquiv.symm : (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
            x :
          FirstObj P S.arrows)
⊢ (∃! t : P.obj (op X), x.IsAmalgamation (R := S.arrows) t) ↔
    ∃! x_1 : P.obj (op X),
      Eq (α := FirstObj P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
            x_1 :
          FirstObj P S.arrows)
        (((firstObjEqFamily P S.arrows).toEquiv.symm : (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
            x :
          FirstObj P S.arrows)

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
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
t : P.obj (op X)
h :
  x.IsAmalgamation (R := S.arrows) t ↔
    ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) =
      x
⊢ x.IsAmalgamation (R := S.arrows) t ↔
    Eq (α := FirstObj P S.arrows)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t :
        FirstObj P S.arrows)
      (((firstObjEqFamily P S.arrows).toEquiv.symm : (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
          x :
        FirstObj P S.arrows)

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
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
t : P.obj (op X)
h :
  x.IsAmalgamation (R := S.arrows) t →
    ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) =
      x
h₁ :
  ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) =
      x →
    x.IsAmalgamation (R := S.arrows) t
⊢ x.IsAmalgamation (R := S.arrows) t ↔
    ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) 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
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
t : P.obj (op X)
q : x.IsAmalgamation (R := S.arrows) t
h :
  ∀ {Y : C} (f : Y ⟶ X) (hf : S.arrows f),
    ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) f
        hf =
      x f hf
⊢ ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) =
    x

Tactic:
ext 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
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
t : P.obj (op X)
q : x.IsAmalgamation (R := S.arrows) t
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) f
      hf =
    x f hf

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

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Equalizer.forkMap
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
t : P.obj (op X)
q :
  ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) =
    x
Y : C
f : Y ⟶ X
hf : S.arrows 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 S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) 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
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements P S.arrows
b : x.Compatible (R := S.arrows)
t : P.obj (op X)
q :
  ((firstObjEqFamily P S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) t) =
    x
Y : C
f : Y ⟶ X
hf : S.arrows 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 S.arrows).toEquiv : (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows) 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 : 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)
⊢ 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)

Tactic:
haveI := Presieve.HasPairwisePullbacks.has_pullbacks fg.1.2.2 fg.2.2.2
-- 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)
h :
  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)
⊢ 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 (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X).op ≫
          P.map
            (Quiver.Hom.op
              (pullback.fst (↑(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)
    (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:
rw [← P.map_comp, ← op_comp, pullback.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition