Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: 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.ofArrows T g ∈ (J.over X) Z
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)))
⊢ ∃! t_1, t.IsAmalgamation t_1

Tactic:
rw [J.mem_over_iff, Sieve.ofArrows, Sieve.overEquiv_generate,
    ← Sieve.arrows_generate_map_eq_functorPushforward, Sieve.generate_sieve,
    Presieve.map_ofArrows] at hR

Goal state after:
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)))
⊢ ∃! t_1, t.IsAmalgamation t_1