Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: case zero
C✝ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
    (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app WalkingParallelPair.zero

pp: case one
C✝ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
    (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
C✝ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
    (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app WalkingParallelPair.zero

case one
C✝ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
    (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app WalkingParallelPair.one