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
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
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)
have 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)
Tactic: rw [← Iso.toEquiv_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
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),
  (((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)
Tactic: enter [2, a, 1, 1]; rw [← Iso.toEquiv_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
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 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)
Tactic: conv => enter [2, a, 1, 1]; rw [← Iso.toEquiv_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
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)
          (((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)
have 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)
Tactic: simp_rw [Equiv.apply_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
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
⊢ 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)
have 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)
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
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements 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)
have 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)
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
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b : x.Compatible (R := R)
t : P.obj (op 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)
have 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
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
R : Presieve.{v, u} X
inst_1 : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b : x.Compatible (R := R)
t : P.obj (op X)
⊢ 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
have 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
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 : 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 ↔
    ((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
have 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
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 : Presieve.FamilyOfElements P R
b : x.Compatible (R := R)
t : P.obj (op X)
q : 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
have 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
Tactic: funext 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
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 :
  ((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
Y : C
f : Y ⟶ X
hf : R 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 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 :
    P.obj (op Y))
Tactic: rw [← q]
-- 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)
I : Type t
inst_1 : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₁ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : I) ↦ P.obj (op (X i))) i) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          z₂ :
        (fun (X : Type w) ↦ X) (P.obj (op (X i))))
⊢ z₁ = z₂
have w : ∀ (j : Discrete I),
  Eq (α := (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j) :
          (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
            (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj j))
        z₁ :
      (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j) :
          (a : (fun (X : Type w) ↦ X) (limit (Discrete.functor fun (i : I) ↦ P.obj (op (X i))))) →
            (fun (X : Type w) ↦ X) ((Discrete.functor fun (i : I) ↦ P.obj (op (X i))).obj j))
        z₂ :
      (fun (X : Type w) ↦ X) (Functor.obj (Discrete.functor fun (i : I) ↦ P.obj (op (X i))) j))
Tactic: apply Limits.Types.limit_ext
-- 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
⊢ Eq (α := P.obj (op B) ⟶ SecondObj P X π) (forkMap P X π ≫ firstMap P X π) (forkMap P X π ≫ secondMap P X π)
have h : ∀ (x : I × I) (ij : P.obj (op B)),
  Eq (α := P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
            (forkMap P X π ≫ firstMap P X π : P.obj (op B) ⟶ SecondObj P X π)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x)))
        ij :
      P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
            (forkMap P X π ≫ secondMap P X π : P.obj (op B) ⟶ SecondObj P X π)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x)))
        ij :
      P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
Tactic: ext x 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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.Compatible 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 rw : 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 π))
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 w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ 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 : 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 π))
Tactic: constructor
-- 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
mp :
  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 π))
⊢ 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 mpr : Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
          (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
        x :
      (fun (X : Type w) ↦ X) (SecondObj P X π))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
          (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
        x :
      (fun (X : Type w) ↦ X) (SecondObj P X π)) →
  Arrows.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)
Tactic: constructor