Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: 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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)

pp: 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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
V : C
iUV : V ⟶ r.Z
hiUV : iUV ≫ r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯ = iUV ≫ r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₁.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₂.op)

Tactic:
· rw [map_comp, hl, map_comp, hl, ← map_comp_assoc, r.w, map_comp_assoc]

Goal state after:
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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
V : C
iUV : V ⟶ r.Z
hiUV : iUV ≫ r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯ = iUV ≫ r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₁.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₂.op)