Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : unop (G.op.obj (op W₁)) ⟶ unop (op (G.obj U))
W₂ : C
g₂ : unop (G.op.obj (op W₂)) ⟶ unop (op (G.obj U))
i : unop (StructuredArrow.mk (op g₂)).right ⟶ unop (StructuredArrow.mk (op g₁)).right
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op g₂)).hom
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map (StructuredArrow.homMk (op i) hi) ≫
      ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₂)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₂)).2) U I.f (StructuredArrow.mk (op g₂)).hom.unop ⋯).op)
        ⋯ =
    ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₁)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₁)).2) U I.f (StructuredArrow.mk (op g₁)).hom.unop ⋯).op)
        ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map (StructuredArrow.homMk (op i) hi)

Tactic:
replace hi := Quiver.Hom.op_inj hi

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : unop (G.op.obj (op W₁)) ⟶ unop (op (G.obj U))
W₂ : C
g₂ : unop (G.op.obj (op W₂)) ⟶ unop (op (G.obj U))
i : unop (StructuredArrow.mk (op g₂)).right ⟶ unop (StructuredArrow.mk (op g₁)).right
hi✝ : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op g₂)).hom
hi : (G.op.map (op i)).unop ≫ (StructuredArrow.mk (op g₁)).hom.unop = g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map (StructuredArrow.homMk (op i) hi✝) ≫
      ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₂)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₂)).2) U I.f (StructuredArrow.mk (op g₂)).hom.unop ⋯).op)
        ⋯ =
    ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₁)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₁)).2) U I.f (StructuredArrow.mk (op g₁)).hom.unop ⋯).op)
        ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map (StructuredArrow.homMk (op i) hi✝)