-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : G.obj X) ↦
            {
              arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                ∃ (a : F.obj (Opposite.op Y)),
                  Eq (α := G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                      G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                        a :
                      G.obj (Opposite.op Y)),
              downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }) :
        (a : G.obj X) → (Functor.sieves C).obj X)
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (hg :
          (Sieve.pullback f
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
                    (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) →
                      (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
                  x)).arrows
            g) →
        (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y)
    (hg :
      (Sieve.pullback f
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) →
                  (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
              x)).arrows
        g),
    Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
            (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
          x :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
            (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
          (a Z g hg) :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
Z : C
f' : Z ⟶ Y
hf' :
  (Sieve.pullback f
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : G.obj X) ↦
                {
                  arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                    ∃ (a : F.obj (Opposite.op Y)),
                      Eq (α := G.obj (Opposite.op Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y))
                            x :
                          G.obj (Opposite.op Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                              (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                            a :
                          G.obj (Opposite.op Y)),
                  downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }) :
            (a : G.obj X) → (Functor.sieves C).obj X)
          x)).arrows
    f'
refine_2 :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
          (a : F.obj (Opposite.op Z)) → G.obj (Opposite.op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f'.op) : (a : F.obj (Opposite.op Y)) → F.obj (Opposite.op Z))
          (⋯.amalgamate (R :=
            (Sieve.pullback f
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (↾fun (x : G.obj X) ↦
                        {
                          arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                            ∃ (a : F.obj (Opposite.op Y)),
                              Eq (α := G.obj (Opposite.op Y))
                                ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
                                      (a : G.obj X) → G.obj (Opposite.op Y))
                                    x :
                                  G.obj (Opposite.op Y))
                                ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                                      (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                                    a :
                                  G.obj (Opposite.op Y)),
                          downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }) :
                    (a : G.obj X) → (Functor.sieves C).obj X)
                  x)).arrows)
            a ⋯)) :
      G.obj (Opposite.op Z))
refine_2₁ :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
          (a : F.obj (Opposite.op Z)) → G.obj (Opposite.op Z))
        (a Z f' hf') :
      G.obj (Opposite.op Z))
refine_2₂ :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (f' ≫ f).op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
refine_2₃ :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (f.op ≫ f'.op)) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
refine_2₄ refine_2₅ :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) : (a : G.obj (Opposite.op Y)) → G.obj (Opposite.op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
            (a : G.obj (Opposite.op (Opposite.unop X))) → G.obj (Opposite.op Y))
          x) :
      G.obj (Opposite.op Z))
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f'.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
            (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
          (⋯.amalgamate (R :=
            (Sieve.pullback f
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (↾fun (x : G.obj X) ↦
                        {
                          arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                            ∃ (a : F.obj (Opposite.op Y)),
                              Eq (α := G.obj (Opposite.op Y))
                                ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
                                      (a : G.obj X) → G.obj (Opposite.op Y))
                                    x :
                                  G.obj (Opposite.op Y))
                                ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                                      (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                                    a :
                                  G.obj (Opposite.op Y)),
                          downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }) :
                    (a : G.obj X) → (Functor.sieves C).obj X)
                  x)).arrows)
            a ⋯)) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))

Tactic:
rw [← NatTrans.naturality_apply, (hF _ hf).valid_glue _ _ hf', ← (ha _ _ _),
      op_comp, Functor.map_comp_apply]

Premises used: CategoryTheory.op_comp, CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Functor.map_comp_apply, CategoryTheory.Presieve.IsSheafFor.valid_glue