-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R₀ R : Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
α : R₀ ⟶ R
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst_2 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
hA :
  Presheaf.IsSeparated J A (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier)
X : C
r : (↑(R.obj (Opposite.op X)) : Type u)
m : (↑(A.obj (Opposite.op X)) : Type v)
P : Presieve.{v₁, u₁} X
r₀ :
  FamilyOfElements
    (R₀ ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)) P
m₀ :
  FamilyOfElements
    (M₀.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
    P
hr₀ :
  (r₀.map (R := P)
        (whiskerRight α
          (forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            RingCat.carrier)))).IsAmalgamation
    (R := P) r
hm₀ :
  (m₀.map (R := P)
        (whiskerRight φ
          (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier)))).IsAmalgamation
    (R := P) m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)).obj
  (Opposite.op Y₁) :=
  r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier)).obj
  (Opposite.op Y₁) :=
  m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)).obj
  (Opposite.op Y₂) :=
  r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier)).obj
  (Opposite.op Y₂) :=
  m₀ f₂ h₂
a₀ : (↑(R₀.obj (Opposite.op Z)) : Type u) :=
  (ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        (R₀.map g₁.op) :
      (a : (↑(R₀.obj (Opposite.op Y₁)) : Type u)) → (↑(R₀.obj (Opposite.op Z)) : Type u))
    a₁
b₀ : (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) : Type v) :=
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R₀.obj (Opposite.op Y₁)) : Type u)) ↦
        LinearMap.{u, u, v, v} (R := (↑(R₀.obj (Opposite.op Y₁)) : Type u))
          (RingHom.id (↑(R₀.obj (Opposite.op Y₁)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
        (CC := ModuleCat.carrier) (M₀.map g₁.op) :
      (a : (↑(M₀.obj (Opposite.op Y₁)) : Type v)) →
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) : Type v))
    b₁
ha₁ :
  Eq (α := (↑(R.obj (Opposite.op Y₁)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Y₁)) (α.app (Opposite.op Y₁)) :
          (a : (↑(R₀.obj (Opposite.op Y₁)) : Type u)) → (↑(R.obj (Opposite.op Y₁)) : Type u))
        a₁ :
      (↑(R.obj (Opposite.op Y₁)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.map f₁.op) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Y₁)) : Type u))
        r :
      (↑(R.obj (Opposite.op Y₁)) : Type u))
ha₂ :
  Eq (α := (↑(R.obj (Opposite.op Y₂)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Y₂)) (α.app (Opposite.op Y₂)) :
          (a : (↑(R₀.obj (Opposite.op Y₂)) : Type u)) → (↑(R.obj (Opposite.op Y₂)) : Type u))
        a₂ :
      (↑(R.obj (Opposite.op Y₂)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.map f₂.op) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Y₂)) : Type u))
        r :
      (↑(R.obj (Opposite.op Y₂)) : Type u))
hb₁ :
  Eq (α := (↑(A.obj (Opposite.op Y₁)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y₁)) (φ.app (Opposite.op Y₁)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Y₁)) : Type v)) → (↑(A.obj (Opposite.op Y₁)) : Type v))
        b₁ :
      (↑(A.obj (Opposite.op Y₁)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.map f₁.op) :
          (a : (↑(A.obj (Opposite.op X)) : Type v)) → (↑(A.obj (Opposite.op Y₁)) : Type v))
        m :
      (↑(A.obj (Opposite.op Y₁)) : Type v))
hb₂ :
  Eq (α := (↑(A.obj (Opposite.op Y₂)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y₂)) (φ.app (Opposite.op Y₂)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Y₂)) : Type v)) → (↑(A.obj (Opposite.op Y₂)) : Type v))
        b₂ :
      (↑(A.obj (Opposite.op Y₂)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.map f₂.op) :
          (a : (↑(A.obj (Opposite.op X)) : Type v)) → (↑(A.obj (Opposite.op Y₂)) : Type v))
        m :
      (↑(A.obj (Opposite.op Y₂)) : Type v))
ha₀ :
  Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        a₀ :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R.obj (Opposite.op X)) (Y := R.obj (Opposite.op Z)) (R.map (f₁.op ≫ g₁.op)) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r :
      (↑(R.obj (Opposite.op Z)) : Type u))
hb₀ :
  Eq (α := (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        b₀ :
      (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := A.obj (Opposite.op X)) (Y := A.obj (Opposite.op Z)) (A.map (f₁.op ≫ g₁.op)) :
          (a : (↑(A.obj (Opposite.op X)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        m :
      (↑(A.obj (Opposite.op Z)) : Type v))
ha₀' :
  Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        a₀ :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R.obj (Opposite.op X)) (Y := R.obj (Opposite.op Z)) (R.map (f₂.op ≫ g₂.op)) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r :
      (↑(R.obj (Opposite.op Z)) : Type u))
hb₀' :
  Eq (α := (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        b₀ :
      (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := A.obj (Opposite.op X)) (Y := A.obj (Opposite.op Z)) (A.map (f₂.op ≫ g₂.op)) :
          (a : (↑(A.obj (Opposite.op X)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        m :
      (↑(A.obj (Opposite.op Z)) : Type v))
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier)
      (A.obj (Opposite.op Z)))
    (({
            toFun :=
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                    AddCommGrpCat.carrier) (A.map g₁.op)) :
                (a : (↑(A.obj (Opposite.op Y₁)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v)) } :
          (a : ToType (A.obj (Opposite.op Y₁))) → ToType (A.obj (Opposite.op Z)))
        (({
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                        (CC := AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y₁))
                        (φ.app (Opposite.op Y₁))) :
                    (a : (↑(M₀.obj (Opposite.op Y₁)) : Type v)) → (↑(A.obj (Opposite.op Y₁)) : Type v)) } :
              (a : (↑(M₀.obj (Opposite.op Y₁)) : Type v)) → ToType (A.obj (Opposite.op Y₁)))
            (r₀.smul (P := P) m₀ f₁ h₁) :
          ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.obj (Opposite.op Y₁))) :
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier)
        (A.obj (Opposite.op Z)))
    (({
            toFun :=
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                    AddCommGrpCat.carrier) (A.map g₂.op)) :
                (a : (↑(A.obj (Opposite.op Y₂)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v)) } :
          (a : ToType (A.obj (Opposite.op Y₂))) → ToType (A.obj (Opposite.op Z)))
        (({
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                        (CC := AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y₂))
                        (φ.app (Opposite.op Y₂))) :
                    (a : (↑(M₀.obj (Opposite.op Y₂)) : Type v)) → (↑(A.obj (Opposite.op Y₂)) : Type v)) } :
              (a : (↑(M₀.obj (Opposite.op Y₂)) : Type v)) → ToType (A.obj (Opposite.op Y₂)))
            (r₀.smul (P := P) m₀ f₂ h₂) :
          ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.obj (Opposite.op Y₂))) :
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier)
        (A.obj (Opposite.op Z)))
have erw : Eq (α :=
  ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier)
    (A.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
        (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (M₀.presheaf.map g₁.op) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y₁)) : Type v)) → (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
          (r₀.smul (P := P) m₀ f₁ h₁) :
        (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) :
    (↑(A.obj (Opposite.op Z)) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Z)) (φ.app (Opposite.op Z)) :
        (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (M₀.presheaf.map g₂.op) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y₂)) : Type v)) → (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
          (r₀.smul (P := P) m₀ f₂ h₂) :
        (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) :
    (↑(A.obj (Opposite.op Z)) : Type v))
Tactic: erw [← NatTrans.naturality_apply φ, ← NatTrans.naturality_apply φ]