-- 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 : FirstObj P S.arrows
t :
  Presieve.FamilyOfElements.SieveCompatible (C := C) (P := P) (X := X) (S := S)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
        (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
          (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
      x)
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ Eq (α :=
    (fun (X : Type (max u v)) ↦ X)
      (P.obj
        (op
          (Sigma.fst (β := fun (Z_1 : C) ↦
            (_ :
              Z_1 ⟶
                Sigma.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                  (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                    (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                      (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                        (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf))))) ×
              { f' :
                Sigma.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                    (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                      (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                        (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                          (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf)))) ⟶
                  X //
                S.arrows f' })
            (Sigma.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
              (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                  (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                    (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf)))))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Pi.π
              (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ↦
                P.obj
                  (op
                    (f.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }).fst (β :=
                      fun (Z : C) ↦
                      (_ : Z ⟶ f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })) ×
                        { f' : f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ⟶ X //
                          S.arrows f' }))))
              (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                  (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                    (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf))))) :
          (a :
              (fun (X : Type (max u v)) ↦ X)
                (∏ᶜ fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ↦ P.obj (op f.snd.fst))) →
            (fun (X : Type (max u v)) ↦ X) (P.obj (op ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩.snd.fst)))
        ((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))
          x) :
      (fun (X : Type (max u v)) ↦ X)
        (P.obj
          (op
            (Sigma.fst (β := fun (Z_1 : C) ↦
              (_ :
                Z_1 ⟶
                  Sigma.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                    (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                      (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                        (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                          (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf))))) ×
                { f' :
                  Sigma.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                      (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                        (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                          (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                            (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf)))) ⟶
                    X //
                  S.arrows f' })
              (Sigma.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                  (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                    (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                      (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf)))))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Pi.π
              (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ↦
                P.obj
                  (op
                    (f.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }).fst (β :=
                      fun (Z : C) ↦
                      (_ : Z ⟶ f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })) ×
                        { f' : f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ⟶ X //
                          S.arrows f' }))))
              (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                  (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                    (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf))))) :
          (a :
              (fun (X : Type (max u v)) ↦ X)
                (∏ᶜ fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ↦ P.obj (op f.snd.fst))) →
            (fun (X : Type (max u v)) ↦ X) (P.obj (op ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩.snd.fst)))
        ((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))
          x) :
      (fun (X : Type (max u v)) ↦ X)
        (P.obj
          (op
            (Sigma.fst (β := fun (Z_1 : C) ↦
              (_ :
                Z_1 ⟶
                  Sigma.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                    (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                      (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                        (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                          (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf))))) ×
                { f' :
                  Sigma.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                      (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                        (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                          (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                            (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf)))) ⟶
                    X //
                  S.arrows f' })
              (Sigma.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })
                (Sigma.mk (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Y
                  (Sigma.mk (β := fun (Z : C) ↦ (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) Z
                    (Sigma.mk (β := fun (x : Z ⟶ Y) ↦ { f' : Y ⟶ X // S.arrows f' }) g
                      (Subtype.mk (p := fun (f' : Y ⟶ X) ↦ S.arrows f') f hf)))))))))

Tactic:
simpa [firstMap, secondMap] using t _ g hf

Premises used: CategoryTheory.Equalizer.Sieve.secondMap, CategoryTheory.Equalizer.Sieve.firstMap