-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
rw :
  Eq (α := (↑(CommRingCat.of (at x)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
          (stalkToFiberRingHom 𝒜 x) :
        (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
      (Quotient.liftOn' (s₁ :=
        Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl))
        (Quotient.mk'' z)
        (fun (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl) ↦
          ((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 := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
                  (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A))
                      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))ᵒᵖ) ⟶
                      Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) 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))ᵒᵖ)) :
                    Type u_1) →+*
                  (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
              (a :
                  (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))) :
                    Type u_1)) →
                (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
            (sectionInBasicOpen 𝒜 x f))
        ⋯))
    (Quotient.mk'' z)
rw₁ :
  Eq (α := (↑(CommRingCat.of (at x)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
            (stalkToFiberRingHom 𝒜 x) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : 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 𝒜 (↑z.den : A)) :
                    (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
                (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
                (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)) x
                    ⋯ :
                  Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                    Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) :
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                      (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                      (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)) :
                        (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                  Type u_1) →+*
                (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
            (a :
                (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)))) :
                  Type u_1)) →
              (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
          (sectionInBasicOpen 𝒜 x z)) :
      (↑(CommRingCat.of (at x)) : Type u_1))
    (Quotient.mk'' z :
      _root_.Quotient (α := HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)
        (Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)))
rw₂ :
  Eq (α := (↑(CommRingCat.of (at x)) : Type u_1))
    ((↑(sectionInBasicOpen 𝒜 x z) :
          (x_1 : ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A))))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
          Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
            (unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)))) x_1)
          x ⋯) :
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
                  (unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)))) x_1)
                x ⋯ :
              ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A))))) :
          (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    (Quotient.mk'' z :
      _root_.Quotient (α := HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)
        (Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)))
rw₃ rw₄ :
  Eq (α := (↑(CommRingCat.of (at x)) : Type u_1))
    ((↑(Subtype.mk (p :=
            fun
              (f :
                (x_1 : ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A))))) →
                  (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                    (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
            PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
              fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
              (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                  (isLocallyFraction 𝒜) :
                PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  at x)
              f)
            (fun (y : ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A))))) ↦
              HomogeneousLocalization.mk { deg := z.deg, num := z.num, den := z.den, den_mem := ⋯ })
            ⋯) :
        (x_1 : ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A))))) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
        Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
          (unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑z.den : A)))) x_1)
        x ⋯))
    (Quotient.mk'' z)
⊢ Eq (α := (↑(CommRingCat.of (at x)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
            (stalkToFiberRingHom 𝒜 x) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
        (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) :
      (↑(CommRingCat.of (at x)) : Type u_1))
    (Quotient.mk'' z :
      _root_.Quotient (α := HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)
        (Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)))

Tactic:
rw [homogeneousLocalizationToStalk, Quotient.liftOn'_mk'',
    stalkToFiberRingHom_germ, sectionInBasicOpen]

Premises used: Quotient.liftOn'_mk'', AlgebraicGeometry.homogeneousLocalizationToStalk, AlgebraicGeometry.sectionInBasicOpen, AlgebraicGeometry.stalkToFiberRingHom_germ