-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve.{v_1, u_2} Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
refine_2 :
  Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (ii ht ≫ i ⋯).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W ⋯)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
        (x (e ⋯) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map t.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
        (x g hg) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map t.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
            z :
          (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map t.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
        (x g hg) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))

Tactic:
rw [← types_comp_apply (P.map g.op) (P.map t.op), ← P.map_comp, ← op_comp, ← hh2 ht,
    op_comp, P.map_comp, types_comp_apply, hz _ (hh1 _),
    ← types_comp_apply _ (P.map (ii ht).op), ← P.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.op, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.types_comp_apply