Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z
hR : Sieve.generate (Presieve.ofArrows (fun i ↦ (Over.forget X).obj (T i)) fun i ↦ (Over.forget X).map (g i)) ∈ J Z.left
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
hg : Presieve.Arrows.Compatible (CategoryTheory.yoneda.obj E.left) (fun i ↦ Over.Hom.left (g i)) fun i ↦
  Over.Hom.left (t (g i) ⋯) :=
  fun i j Z_1 gi gj hgij ↦
    id
      (congrArg Over.Hom.left
        (ht (Over.homMk gi rfl)
          (Over.homMk gj
            (id
              (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ (T j).hom = gi ≫ _a) (Eq.symm (Over.w (g i)))))
                (Eq.mpr
                  (id
                    (congrArg (fun _a ↦ gj ≫ (T j).hom = _a)
                      (id
                        (Eq.mp
                          (forall_congr fun {Z_2} ↦
                            forall_congr fun h ↦
                              congr (congrArg Eq (Category.assoc gi (Over.Hom.left (g i)) h))
                                (Category.assoc gj (Over.Hom.left (g j)) h))
                          (@Mathlib.Tactic.Reassoc.eq_whisker' C inst✝¹ Z_1 Z.left
                            (gi ≫ (fun i ↦ Over.Hom.left (g i)) i) (gj ≫ (fun i ↦ Over.Hom.left (g i)) j) hgij))
                        Z.hom)))
                  (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ _a = gj ≫ Over.Hom.left (g j) ≫ Z.hom) (Eq.symm (Over.w (g j)))))
                    (Eq.refl (gj ≫ Over.Hom.left (g j) ≫ Z.hom)))))))
          (Sieve.ofArrows_mk T g i) (Sieve.ofArrows_mk T g j) (Over.OverMorphism.ext hgij)))
a : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)
ha : hg.familyOfElements.sieveExtend.IsAmalgamation a
huniq :
  ∀ (y : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)),
    (fun t_1 ↦ hg.familyOfElements.sieveExtend.IsAmalgamation t_1) y → y = a
⊢ a ≫ E.hom = (Opposite.unop (Opposite.op Z)).hom

Tactic:
refine (Subcanonical.isSheaf_of_isRepresentable <| CategoryTheory.yoneda.obj X)
      (.ofArrows _ <| fun i ↦ (g i).left) hR |>.isSeparatedFor.ext ?_

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z
hR : Sieve.generate (Presieve.ofArrows (fun i ↦ (Over.forget X).obj (T i)) fun i ↦ (Over.forget X).map (g i)) ∈ J Z.left
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
hg : Presieve.Arrows.Compatible (CategoryTheory.yoneda.obj E.left) (fun i ↦ Over.Hom.left (g i)) fun i ↦
  Over.Hom.left (t (g i) ⋯) :=
  fun i j Z_1 gi gj hgij ↦
    id
      (congrArg Over.Hom.left
        (ht (Over.homMk gi rfl)
          (Over.homMk gj
            (id
              (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ (T j).hom = gi ≫ _a) (Eq.symm (Over.w (g i)))))
                (Eq.mpr
                  (id
                    (congrArg (fun _a ↦ gj ≫ (T j).hom = _a)
                      (id
                        (Eq.mp
                          (forall_congr fun {Z_2} ↦
                            forall_congr fun h ↦
                              congr (congrArg Eq (Category.assoc gi (Over.Hom.left (g i)) h))
                                (Category.assoc gj (Over.Hom.left (g j)) h))
                          (@Mathlib.Tactic.Reassoc.eq_whisker' C inst✝¹ Z_1 Z.left
                            (gi ≫ (fun i ↦ Over.Hom.left (g i)) i) (gj ≫ (fun i ↦ Over.Hom.left (g i)) j) hgij))
                        Z.hom)))
                  (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ _a = gj ≫ Over.Hom.left (g j) ≫ Z.hom) (Eq.symm (Over.w (g j)))))
                    (Eq.refl (gj ≫ Over.Hom.left (g j) ≫ Z.hom)))))))
          (Sieve.ofArrows_mk T g i) (Sieve.ofArrows_mk T g j) (Over.OverMorphism.ext hgij)))
a : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)
ha : hg.familyOfElements.sieveExtend.IsAmalgamation a
huniq :
  ∀ (y : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)),
    (fun t_1 ↦ hg.familyOfElements.sieveExtend.IsAmalgamation t_1) y → y = a
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z.left⦄,
    (Sieve.ofArrows (fun i ↦ (T i).left) fun i ↦ Over.Hom.left (g i)).arrows f →
      (ConcreteCategory.hom ((CategoryTheory.yoneda.obj X).map f.op)) (a ≫ E.hom) =
        (ConcreteCategory.hom ((CategoryTheory.yoneda.obj X).map f.op)) (Opposite.unop (Opposite.op Z)).hom