-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X_1 : C
R : Presieve.{v₁, u₁} X_1
h : IsSheafFor P₂ R
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
refine :
  Eq.{w' + 1} (α := P₂.obj (op X))
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
        ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
              Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
            (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y : P₂.obj (op Y)))) :
      P₂.obj (op X))
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                  Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
                (a : P₂.obj (op Y)) → P₁.obj (op Y))
              ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y) :
            P₁.obj (op Y))) :
      P₂.obj (op X))
⊢ Eq.{w + 1} (α := P₁.obj (op X))
    ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
            Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
          (a : P₂.obj (op X)) → P₁.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y : P₂.obj (op Y))) :
      P₁.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
        ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
              (a : P₂.obj (op Y)) → P₁.obj (op Y))
            ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y) :
          P₁.obj (op Y)) :
      (fun (X : Type w) ↦ X) (P₁.obj (op X)))

Tactic:
refine e.injective ?_

Premises used: Equiv.injective