-- 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))
rw :
  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)
            (R₀.map g₁.op ≫ α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Y₁)) : 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))
⊢ 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))
have rw₁ : 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)
          (α.app (Opposite.op Y₁) ≫ R.map g₁.op) :
        (a : (↑(R₀.obj (Opposite.op Y₁)) : 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))
Tactic: rw [← RingCat.comp_apply, NatTrans.naturality, RingCat.comp_apply, ha₁, Functor.map_comp,
      RingCat.comp_apply]