-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
protected lemma smul_add : smul α φ r (m + m') = smul α φ r m + smul α φ r m'

Proof state:
case a.intro.intro.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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.val.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.val.map f.op)) m'
⊢ (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r (m + m')) =
    (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r m + smul α φ r m')

Tactic:
rw [(A.val.map f.op).hom.map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
  map_smul_eq α φ r m' f.op r₀ hr₀ m₀' hm₀',
  map_smul_eq α φ r (m + m') f.op r₀ hr₀ (m₀ + m₀')
    (by rw [map_add, map_add, hm₀, hm₀']),
  smul_add, map_add]

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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
⊢ smul α φ r (m + m') = smul α φ r m + smul α φ r m'

Tactic:
let S := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ 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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
⊢ smul α φ r (m + m') = smul α φ r m + smul α φ r 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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.val.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.val.map f.op)) m'
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) (m₀ + m₀') = (ConcreteCategory.hom (A.val.map f.op)) (m + m')

Tactic:
rw [map_add, map_add, hm₀, hm₀']

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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f →
      (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r (m + m')) =
        (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r m + smul α φ r m')

Tactic:
rintro Y f ⟨⟨⟨r₀, hr₀⟩, ⟨m₀ : M₀.obj _, hm₀ : (φ.app _) _ = _⟩⟩,
  ⟨m₀' : M₀.obj _, hm₀' : (φ.app _) _ = _⟩⟩

Result:
case a.intro.intro.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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.val.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.val.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.val.map f.op)) m'
⊢ (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r (m + m')) =
    (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r m + smul α φ r 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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
⊢ smul α φ r (m + m') = smul α φ r m + smul α φ r 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 : Cᵒᵖ
r : ↑(R.val.obj X)
m m' : ↑(A.val.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f →
      (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r (m + m')) =
        (ConcreteCategory.hom (A.val.map f.op)) (smul α φ r m + smul α φ r m')