-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
y : at x
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x.asHomogeneousIdeal.toIdeal.primeCompl) c hc) : A) *
      ((↑g.den : A) * (↑f.num : A)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x.asHomogeneousIdeal.toIdeal.primeCompl) c hc) : A) *
      ((↑f.den : A) * (↑g.num : A))
⊢ Eq (α :=
    (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
          (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
          (op
              (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                ProjectiveSpectrum.basicOpen 𝒜 c) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
      Type u_1))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (Y :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                  (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
            (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1) →+*
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1)) :
          (a :
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.obj
                  (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c))) :
              Type u_1))
        (sectionInBasicOpen 𝒜 x f) :
      (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
            (op
                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                  ProjectiveSpectrum.basicOpen 𝒜 c) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
        Type u_1))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (Y :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                  (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
            (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1) →+*
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1)) :
          (a :
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)))) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.obj
                  (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c))) :
              Type u_1))
        (sectionInBasicOpen 𝒜 x g) :
      (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
            (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
            (op
                (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                  ProjectiveSpectrum.basicOpen 𝒜 c) :
              (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
        Type u_1))
have a : Eq.{u_1 + 1} (α :=
  (x_1 :
      ↥(unop
          (op
            (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
              ProjectiveSpectrum.basicOpen 𝒜 c)))) →
    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
  (↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (Y :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                  (Quiver.Hom.op (homOfLE sorry ≫ homOfLE sorry)) :
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
            (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1) →+*
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1)) :
          (a :
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.obj
                  (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c))) :
              Type u_1))
        (sectionInBasicOpen 𝒜 x f)) :
    (x_1 :
        ↥(unop
            (op
              (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                ProjectiveSpectrum.basicOpen 𝒜 c)))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
  (↑(((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (Y :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c) :
                  (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (CategoryTheory.Functor.map (Sheaf.presheaf (Proj.structureSheaf 𝒜))
                  (Quiver.Hom.op (homOfLE sorry ≫ homOfLE sorry)) :
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
            (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1) →+*
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1)) :
          (a :
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)))) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.obj
                  (op
                    (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                      ProjectiveSpectrum.basicOpen 𝒜 c))) :
              Type u_1))
        (sectionInBasicOpen 𝒜 x g)) :
    (x_1 :
        ↥(unop
            (op
              (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                ProjectiveSpectrum.basicOpen 𝒜 c)))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
Tactic: apply Subtype.ext