-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
d : F.obj T₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac₂ : d ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map (c ≫ b)
rw :
  CategoryStruct.comp (Y := presheafObj data G₀ (F.obj X₀))
      (inv data G₀ X₀ : G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
      (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ d) =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op
rw₁ :
  IsDenseSubsite.mapPreimage J F G₀ (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i) ≫
      IsDenseSubsite.mapPreimage J F G₀ d =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op
rw₂ :
  IsDenseSubsite.mapPreimage J F G₀
      (d ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i) =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op
rw₃ :
  IsDenseSubsite.mapPreimage J F G₀ (F.map (c ≫ b)) =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op
rw₄ : IsDenseSubsite.mapPreimage J F G₀ (F.map (c ≫ b)) = IsDenseSubsite.mapPreimage J F G₀ (F.map (c ≫ a) ≫ f)
rw₅ : IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map b) = IsDenseSubsite.mapPreimage J F G₀ (F.map (c ≫ a) ≫ f)
rw₆ : IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map b) = IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ f)
rw₇ rw₈ :
  IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ f) = IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ f)
⊢ CategoryStruct.comp (Y := presheafObj data G₀ (F.obj X₀))
      (inv data G₀ X₀ : G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
      (restriction data G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op) =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op

Tactic:
rw [restriction_map data G₀ f (c ≫ a) d
    (by rw [fac₂, map_comp, map_comp_assoc, fac₁]), inv_π_assoc,
    ← IsDenseSubsite.mapPreimage_comp, fac₂,
    IsDenseSubsite.mapPreimage_comp_map J F G₀, map_comp,
      map_comp_assoc, fac₁]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π_assoc, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map