-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
⊢ HomogeneousLocalization.mk
      {
        deg :=
          NumDenSameDeg.deg (x := Submonoid.powers f)
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) } +
            NumDenSameDeg.deg (x := Submonoid.powers f)
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) },
        num :=
          Subtype.mk (p := fun (x : A) ↦
            x ∈
              𝒜
                (NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) } +
                  NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }))
            ((↑(NumDenSameDeg.num
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A) *
              (↑(NumDenSameDeg.num
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A))
            ⋯,
        den :=
          Subtype.mk (p := fun (x : A) ↦
            x ∈
              𝒜
                (NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) } +
                  NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }))
            ((↑(NumDenSameDeg.den
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A) *
              (↑(NumDenSameDeg.den
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A))
            ⋯,
        den_mem := ⋯ } ∈
    q.asIdeal
have dsimp : HomogeneousLocalization.mk
    { deg := m * i + m * i,
      num :=
        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i))
          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m *
            HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m)
          sorry,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i)) (f ^ i * f ^ i) sorry, den_mem := sorry } ∈
  q.asIdeal
Tactic: dsimp only [Subtype.coe_mk]