-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
lemma map_smul :
    A.val.map π (smul α φ r m) = smul α φ (R.val.map π r) (A.val.map π m)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
hS : S ∈ J (Opposite.unop Y)
⊢ (ConcreteCategory.hom (A.val.map π)) (smul α φ r m) =
    smul α φ ((ConcreteCategory.hom (R.val.map π)) r) ((ConcreteCategory.hom (A.val.map π)) m)

Tactic:
apply A.isSeparated _ _ hS

Result:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
hS : S ∈ J (Opposite.unop Y)
⊢ ∀ (Y_1 : C) (f : Y_1 ⟶ Opposite.unop Y),
    S.arrows f →
      (ConcreteCategory.hom (A.val.map f.op)) ((ConcreteCategory.hom (A.val.map π)) (smul α φ r m)) =
        (ConcreteCategory.hom (A.val.map f.op))
          (smul α φ ((ConcreteCategory.hom (R.val.map π)) r) ((ConcreteCategory.hom (A.val.map π)) m))

Proof state:
case sj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
⊢ Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m) ∈ J (Opposite.unop Y)

Tactic:
apply Presheaf.imageSieve_mem

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
⊢ (ConcreteCategory.hom (A.val.map π)) (smul α φ r m) =
    smul α φ ((ConcreteCategory.hom (R.val.map π)) r) ((ConcreteCategory.hom (A.val.map π)) m)

Tactic:
let S := Presheaf.imageSieve α (R.val.map π r) ⊓ Presheaf.imageSieve φ (A.val.map π m)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
⊢ (ConcreteCategory.hom (A.val.map π)) (smul α φ r m) =
    smul α φ ((ConcreteCategory.hom (R.val.map π)) r) ((ConcreteCategory.hom (A.val.map π)) m)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
⊢ S ∈ J (Opposite.unop Y)

Tactic:
apply J.intersection_covering

Result:
case rj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
⊢ Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ∈ J (Opposite.unop Y)

case sj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
⊢ Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m) ∈ J (Opposite.unop Y)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrp
φ : M₀.presheaf ⟶ A.val
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r : ↑(R.val.obj X)
m : ↑(A.val.obj X)
S : Sieve (Opposite.unop Y✝) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.val.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.val.map π)) m)
hS : S ∈ J (Opposite.unop Y✝)
Y : C
f : Y ⟶ Opposite.unop Y✝
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ :
  (RingCat.Hom.hom (α.app (Opposite.op Y))) r₀ = (RingCat.Hom.hom (R.val.map f.op)) ((RingCat.Hom.hom (R.val.map π)) r)
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ :
  (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
    (ConcreteCategory.hom (A.val.map f.op)) ((ConcreteCategory.hom (A.val.map π)) m)
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map (π ≫ f.op))) r

Tactic:
rw [hr₀, Functor.map_comp, RingCat.comp_apply]

Result:
no goals