Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
⊢ S ∈ J (Opposite.unop X)

Tactic:
apply J.intersection_covering

Goal state after:
case rj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := ⋯
⊢ Presheaf.imageSieve α r ∈ J (Opposite.unop X)

case sj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := ⋯
⊢ Presheaf.imageSieve φ m ∈ J (Opposite.unop X)