-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
compatible :
  ∀ ⦃Z_1 : C⦄ (j : Z_1 ⟶ V₂),
    j ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = j ≫ iV₂Y₂ ≫ g₂ →
      Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z_1))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₂)))) →
                (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Z_1))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iV₂V₁).op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁)))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₂))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iVW).op) :
                      (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W)))) →
                        (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁))))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
                          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) →
                            (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) →
                                (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                            (x g₁ hg₁) :
                          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
                      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W)))) :
                  (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁)))) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₂)))) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z_1))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₂)))) →
                (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Z_1))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iV₂V₁).op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁)))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₂))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iVW).op) :
                      (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W)))) →
                        (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁))))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
                          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) →
                            (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) →
                                (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                            (x g₂ hg₂) :
                          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
                      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W)))) :
                  (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁)))) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₂)))) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z_1))))
⊢ Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₂))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iV₂V₁).op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁)))) →
            (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₂))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iVW).op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W)))) →
                (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                      (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) →
                        (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                    (x g₁ hg₁) :
                  (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W)))) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁)))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₂))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iV₂V₁).op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁)))) →
            (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₂))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iVW).op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W)))) →
                (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                      (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) →
                        (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                    (x g₂ hg₂) :
                  (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W)))) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁)))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₂))))

Tactic:
refine IsLocallyFaithful.ext G _ (iV₂V₁ ≫ iV₁Y₁ ≫ g₁) (iV₂Y₂ ≫ g₂) (by simp [e₁, e₂, eq]) ?_

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.IsLocallyFaithful.ext