-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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₀ : C₀
i : PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀))) (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
rw :
  presheafObjObjIso.hom data G₀ X₀ ≫
      CategoryStruct.comp (Y := presheafObj data G₀ (unop (op (F.obj X₀))))
        (presheafObjObjIso.inv data G₀ X₀ :
          G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
        (presheafObjπ data G₀ (unop (op (F.obj X₀))) i) =
    𝟙 ((presheaf data G₀).obj (op (F.obj X₀))) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i
rw₁ :
  presheafObjObjIso.hom data G₀ X₀ ≫
      IsDenseSubsite.mapPreimage J F G₀
        (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i) =
    𝟙 ((presheaf data G₀).obj (op (F.obj X₀))) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i
rw₂ :
  Eq (α :=
    (presheaf data G₀).obj (op (F.obj X₀)) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i)))
    (presheafObjObjIso.hom data G₀ X₀ ≫
      IsDenseSubsite.mapPreimage J F G₀ (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i))
    (presheafObjπ data G₀ (unop (op (F.obj X₀))) i)
rw₃ :
  Eq (α :=
    (presheaf data G₀).obj (op (F.obj X₀)) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i)))
    (presheafObjπ data G₀ (F.obj X₀) i ≫
        IsDenseSubsite.mapPreimage J F G₀
          (𝟙 (F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i))) :
      presheafObj data G₀ (F.obj X₀) ⟶
        G₀.obj (P := Presheaf.IsSheaf J₀).obj
          (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)))
    (presheafObjπ data G₀ (unop (op (F.obj X₀))) i)
rw₄ :
  Eq (α :=
    (presheaf data G₀).obj (op (F.obj X₀)) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i)))
    (presheafObjπ data G₀ (F.obj X₀) i ≫
        𝟙
          (G₀.obj (P := Presheaf.IsSheaf J₀).obj
            (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i))) :
      presheafObj data G₀ (F.obj X₀) ⟶
        G₀.obj (P := Presheaf.IsSheaf J₀).obj
          (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)))
    (presheafObjπ data G₀ (unop (op (F.obj X₀))) i)
⊢ CategoryStruct.comp (Y := presheafObj data G₀ (unop (op (F.obj X₀))))
      (presheafObjObjIso.hom data G₀ X₀ ≫ presheafObjObjIso.inv data G₀ X₀ :
        (presheaf data G₀).obj (op (F.obj X₀)) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
      (presheafObjπ data G₀ (unop (op (F.obj X₀))) i) =
    𝟙 ((presheaf data G₀).obj (op (F.obj X₀))) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i
have rw₅ : Eq (α :=
  (presheaf data G₀).obj (op (F.obj X₀)) ⟶
    G₀.obj (P := Presheaf.IsSheaf J₀).obj
      (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i)))
  (presheafObjπ data G₀ (F.obj X₀) i :
    presheafObj data G₀ (F.obj X₀) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)))
  (presheafObjπ data G₀ (unop (op (F.obj X₀))) i)
Tactic: rw [assoc, presheafObjObjIso.inv_π, id_comp,
      presheafObjObjIso.hom_mapPreimage data G₀ _ (𝟙 _) (fac := by simp),
      IsDenseSubsite.mapPreimage_id, comp_id]