-- 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))
t : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
ht' : t ∈ (↑(ProjectiveSpectrum.basicOpen 𝒜 c) : Set (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
htf : t ∈ (↑(ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) : Set (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
htg : t ∈ (↑(ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)) : Set (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
⊢ Eq (α :=
    Localization (M := A)
      (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
                    (unop
                      (op
                        (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                          ProjectiveSpectrum.basicOpen 𝒜 c)))
                    x_1)
                  t ⋯) :
              (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(sectionInBasicOpen 𝒜 x f) :
          (x_1 : ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A))))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
            (a :
                ↥(unop
                    (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c)))) →
              ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))))
          (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
            Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
              (unop
                (op
                  (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c)))
              x_1)
            t ⋯))))
    (val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(sectionInBasicOpen 𝒜 x g) :
          (x_1 : ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A))))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯ ≫ homOfLE ⋯)) :
            (a :
                ↥(unop
                    (op
                      (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                        ProjectiveSpectrum.basicOpen 𝒜 c)))) →
              ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A)))))
          (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
            Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
              (unop
                (op
                  (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A) ⊓ ProjectiveSpectrum.basicOpen 𝒜 (↑g.den : A) ⊓
                    ProjectiveSpectrum.basicOpen 𝒜 c)))
              x_1)
            t ⋯))))
have a : Eq (α := Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl)
  ((algebraMap A (Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl) :
        (a : A) → Localization t.asHomogeneousIdeal.toIdeal.primeCompl)
      ((↑g.den : A) * (↑f.num : A)) :
    Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl)
  ((algebraMap A (Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl) :
        (a : A) → Localization t.asHomogeneousIdeal.toIdeal.primeCompl)
      ((↑f.den : A) * (↑g.num : A)) :
    Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl)
Tactic: simp only [sectionInBasicOpen, HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
      IsLocalization.mk'_eq_iff_eq]