-- 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₂'
rcases :
  ∀ (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₂ ≫ f₂'),
    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 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)))
        (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)))

Tactic:
rcases getFunctorPushforwardStructure H₁ with ⟨X₁, f₁, h₁, hf₁, rfl⟩

Premises used: CategoryTheory.Presieve.getFunctorPushforwardStructure, rfl