-- 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))
a :
  (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) *
        ((↑g.den : A) * (↑f.num : 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)
          ((↑f.den : A) * (↑g.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)
          ((↑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)
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)
      ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t.asHomogeneousIdeal.toIdeal.primeCompl) c ht') : A) *
        ((↑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)
      ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t.asHomogeneousIdeal.toIdeal.primeCompl) c ht') : A) *
        ((↑f.den : A) * (↑g.num : A))) :
    Localization (M := A) t.asHomogeneousIdeal.toIdeal.primeCompl)
Tactic: rw [← map_mul, ← map_mul, hc']