-- 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)
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))
a :
  HMul.hMul (α := Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl) (β :=
      Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl)
      ((algebraMap A (Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl) :
            (a : A) → Localization t.asHomogeneousIdeal.toIdeal.primeCompl)
          (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t.asHomogeneousIdeal.toIdeal.primeCompl) c ht') : A) :
        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) =
    HMul.hMul (α := Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl) (β :=
      Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl)
      ((algebraMap A (Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl) :
            (a : A) → Localization t.asHomogeneousIdeal.toIdeal.primeCompl)
          (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t.asHomogeneousIdeal.toIdeal.primeCompl) c ht') : 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)
⊢ 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:
apply (IsLocalization.map_units (M := t.asHomogeneousIdeal.toIdeal.primeCompl)
      (Localization t.asHomogeneousIdeal.toIdeal.primeCompl) ⟨c, ht'⟩).mul_left_cancel

Premises used: Localization, Subtype.mk, IsUnit.mul_left_cancel, IsLocalization.map_units, Ideal.primeCompl, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.asHomogeneousIdeal