-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
h : x.Compatible (R := T)
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁' : Z₁ ⟶ G.obj Z
f₂' : Z₂ ⟶ G.obj Z
H₁ : Presieve.functorPushforward G T f₁'
H₂ : Presieve.functorPushforward G T f₂'
eq : g₁ ≫ f₁' = g₂ ≫ f₂'
unfold :
  Eq (α := (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op Z₁))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (FunctorPushforwardStructure.casesOn (S := T) (motive := fun (x : FunctorPushforwardStructure G T f₁') ↦
            ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z₁)) (getFunctorPushforwardStructure (S := T) H₁)
            fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : Z₁ ⟶ G.obj Z_1) (h₁ : T g) (fac : f₁' = h ≫ G.map g) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map h.op) :
                (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Z_1)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op Z₁)))
              (x g h₁) :
          ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z₁)) :
      (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op Z₂))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (FunctorPushforwardStructure.casesOn (S := T) (motive := fun (x : FunctorPushforwardStructure G T f₂') ↦
            ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z₂)) (getFunctorPushforwardStructure (S := T) H₂)
            fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : Z₂ ⟶ G.obj Z_1) (h₁ : T g) (fac : f₂' = h ≫ G.map g) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map h.op) :
                (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Z_1)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op Z₂)))
              (x g h₁) :
          ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z₂)) :
      (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op Z₁))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (FamilyOfElements.functorPushforward G (T := T) x f₁' H₁) :
      (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op Z₂))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (FamilyOfElements.functorPushforward G (T := T) x f₂' H₂) :
      (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))

Tactic:
unfold FamilyOfElements.functorPushforward

Premises used: CategoryTheory.Presieve.FamilyOfElements.functorPushforward