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 : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
⊢ 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)
have 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)
Tactic: apply forall₂_congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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), 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)
have 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)
Tactic: apply existsUnique_congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)
⊢ 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)
have 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
Tactic: rw [Equiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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 ↔
    ((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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ ((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
have 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
Tactic: ext Y f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ (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
have 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))
Tactic: rw [← q]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (hypothesis)
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)
⊢ 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)
have 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)
Tactic: haveI := Presieve.HasPairwisePullbacks.has_pullbacks fg.1.2.2 fg.2.2.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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 (↑(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)
have 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)
Tactic: rw [← P.map_comp, ← op_comp, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ 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))
have 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))
Tactic: rw [Presieve.pullbackCompatible_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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))
⊢ 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))
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ Presieve.IsSheafFor P R ↔
    Nonempty
      (IsLimit (F := parallelPair (Y := SecondObj P R) (firstMap P R) (secondMap P R)) (Fork.ofι (forkMap P R) ⋯))
have 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)
Tactic: rw [Types.type_equalizer_iff_unique,
    ← Equiv.forall_congr_right (firstObjEqFamily P R).toEquiv.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [← compatible_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
| 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)
have 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)
Tactic: enter [2, a, 1, 1]