-- 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₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
this :
  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₁ ≫ h₁).op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj X₁)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (x f₁ hf₁) :
      (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₂ ≫ h₂).op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj X₂)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (x f₂ hf₂) :
      (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)))
        (FunctorPushforwardStructure.casesOn (S := T) (motive :=
            fun (x : FunctorPushforwardStructure G T (h₁ ≫ G.map f₁)) ↦ ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z₁))
            (FunctorPushforwardStructure.mk (S := T) X₁ f₁ h₁ hf₁ ⋯)
            fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : Z₁ ⟶ G.obj Z_1) (h₁_1 : T g) (fac : h₁ ≫ G.map 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₁_1) :
          ℱ.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 (h₂ ≫ G.map f₂)) ↦ ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z₂))
            (FunctorPushforwardStructure.mk (S := T) X₂ f₂ h₂ hf₂ ⋯)
            fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : Z₂ ⟶ G.obj Z_1) (h₁ : T g) (fac : h₂ ≫ G.map 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)))

Tactic:
simpa using this