-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P Q : Functor.{v, w', u, w} Cᵒᵖ D
R : Sheaf.{v, w', u, w} J D
η : P ⟶ Q
γ : Q ⟶ Functor.obj (sheafToPresheaf J D) R
h :
  Eq (α :=
    (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
      R.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
        ((Equiv.symm
              { toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R) ↦ J.toSheafify P ≫ e.hom,
                invFun := fun (e : P ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                left_inv := ⋯, right_inv := ⋯ } :
            (a : P ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj P ⟶ R)
          (η ≫ γ)) :
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
        R.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
        (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) η ≫
          (Equiv.symm
                {
                  toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) Q ⟶ R) ↦
                    J.toSheafify Q ≫ e.hom,
                  invFun := fun (e : Q ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
              (a : Q ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj Q ⟶ R)
            γ) :
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
        R.obj (P := Presheaf.IsSheaf J))
⊢ Eq (α := Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R)
    ((Equiv.symm
            { toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R) ↦ J.toSheafify P ≫ e.hom,
              invFun := fun (e : P ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
          (a : P ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj P ⟶ R)
        (η ≫ γ) :
      Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R)
    (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) η ≫
        (Equiv.symm
              { toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) Q ⟶ R) ↦ J.toSheafify Q ≫ e.hom,
                invFun := fun (e : Q ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                left_inv := ⋯, right_inv := ⋯ } :
            (a : Q ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj Q ⟶ R)
          γ :
      Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R)

Tactic:
ext1