-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
i j : ↥U
this :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen (g i))))
    (const (f i) (g i) (basicOpen (g i)) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            ⋯.hom.op) :
        (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
          (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g i)))))
      s)
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g i * g j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              (homOfLE ⋯).op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g i * g j)))))
        s :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen (g i * g j)))))
    (const (g j • f i) (g i * g j) (basicOpen (g i * g j)) ⋯ :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g i * g j))))

Tactic:
congr((structureSheafInType R M).obj.map (homOfLE ((PrimeSpectrum.basicOpen_mul (g i)
        (g j)).trans_le inf_le_left)).op $(H i)).symm.trans (Subtype.ext <| funext fun a ↦ ?_)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, Set.Mem, Quiver.Hom.op, PrimeSpectrum.basicOpen_mul, id, CategoryTheory.ObjectProperty.FullSubcategory.obj, Eq.trans_le, CategoryTheory.Functor.map, funext, CategoryTheory.homOfLE, inf_le_left, AlgebraicGeometry.structureSheafInType, Eq.symm, DFunLike.coe, Eq.trans, Subtype.ext