-- 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:
case a.intro.intro.intro
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 (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))

Tactic:
rw [← ConcreteCategory.comp_apply, ← Functor.map_comp,
  map_smul_eq α φ r m (π ≫ f.op) r₀ (by rw [hr₀, Functor.map_comp, RingCat.comp_apply]) m₀
    (by rw [hm₀, Functor.map_comp, ConcreteCategory.comp_apply]),
  map_smul_eq α φ (R.val.map π r) (A.val.map π m) f.op r₀ hr₀ m₀ hm₀]

Result:
no goals

Proof state:
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)

Tactic:
all_goals apply Presheaf.imageSieve_mem

Result:
no goals

Proof state:
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))

Tactic:
rintro Y f ⟨⟨r₀,
  (hr₀ : (α.app (Opposite.op Y)).hom r₀ = (R.val.map f.op).hom ((R.val.map π).hom r))⟩,
  ⟨m₀, (hm₀ : (φ.app _) _ = _)⟩⟩

Result:
case a.intro.intro.intro
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 (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:
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)

Tactic:
have hS : S ∈ J Y.unop := by
  apply J.intersection_covering
  all_goals apply Presheaf.imageSieve_mem

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)
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)