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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)
overS : SheafOfModules S ⥤ SheafOfModules (S.over i.fst) := SheafOfModules.pushforward (𝟙 (S.over i.fst))
G' : Over i.fst ⥤ Over (P.X i.snd.fst) := Over.post G ⋙ Over.map i.snd.snd
ψ : S.over i.fst ⟶
  (G'.sheafPushforwardContinuous RingCat (K.over i.fst) (J.over (P.X i.snd.fst))).obj (R.over (P.X i.snd.fst)) :=
  ((Over.forget i.fst).sheafPushforwardContinuous RingCat (K.over i.fst) K).map φ
e : (SheafOfModules.pushforward ψ).obj (unit (R.over (P.X i.snd.fst))) ≅ unit (S.over i.fst) := overS.mapIso η
⊢ (((SheafOfModules.pushforward φ).obj M).over i.fst).Presentation

Tactic:
haveI : PreservesColimitsOfSize.{u, u, _} (SheafOfModules.pushforward ψ) := h _ _ _

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)
overS : SheafOfModules S ⥤ SheafOfModules (S.over i.fst) := SheafOfModules.pushforward (𝟙 (S.over i.fst))
G' : Over i.fst ⥤ Over (P.X i.snd.fst) := Over.post G ⋙ Over.map i.snd.snd
ψ : S.over i.fst ⟶
  (G'.sheafPushforwardContinuous RingCat (K.over i.fst) (J.over (P.X i.snd.fst))).obj (R.over (P.X i.snd.fst)) :=
  ((Over.forget i.fst).sheafPushforwardContinuous RingCat (K.over i.fst) K).map φ
e : (SheafOfModules.pushforward ψ).obj (unit (R.over (P.X i.snd.fst))) ≅ unit (S.over i.fst) := overS.mapIso η
this :
  PreservesColimitsOfSize.{u, u, max (max u₁ v₁) u, max (max u₂ v₂) u, max (max (max u u₁ v₁) v₁) (u + 1),
      max (max (max u u₂ v₂) v₂) (u + 1)}
    (SheafOfModules.pushforward ψ)
⊢ (((SheafOfModules.pushforward φ).obj M).over i.fst).Presentation