-- 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 : ℕ
g : ℕ → A⁰_ f :=
  fun (j : ℕ) ↦
    HSMul.hSMul (β := A⁰_ f) ((m + m).choose j)
      (if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
                      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j))
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
        else
          HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
                      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j))
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }))
j : ℕ
hj : j ∈ range (m + m + 1)
pos :
  ∀ (h2 : m + m < j),
    Localization.mk
        ((m + m).choose j •
          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
            HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j)))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i + i)) ⋯) =
      HSMul.hSMul (β := Localization (Submonoid.powers f)) ((m + m).choose j)
        (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 0)
pos₁ :
  ∀ (h2 : ¬m + m < j) (h1 : j ≤ m),
    Localization.mk
        ((m + m).choose j •
          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
            HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j)))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i + i)) ⋯) =
      (m + m).choose j •
        (HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
                      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j))
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) })
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) })).val
⊢ Localization.mk
      ((m + m).choose j •
        (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
          HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j)))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i + i)) ⋯) =
    HSMul.hSMul (β := Localization (Submonoid.powers f)) ((m + m).choose j)
      (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        (if h2 : m + m < j then 0
        else
          if h1 : j ≤ m then
            HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
              (HomogeneousLocalization.mk
                { deg := m * i,
                  num :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                      (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
                        HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j))
                      ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) })
              (HomogeneousLocalization.mk
                { deg := m * i,
                  num :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                      (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m) ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) })
          else
            HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
              (HomogeneousLocalization.mk
                { deg := m * i,
                  num :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                      (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) })
              (HomogeneousLocalization.mk
                { deg := m * i,
                  num :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                      (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
                        HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j))
                      ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) })))
have neg : ∀ (h2 : ¬m + m < j) (h1 : ¬j ≤ m),
  Localization.mk
      ((m + m).choose j •
        (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
          HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j)))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i + i)) sorry) =
    (m + m).choose j •
      (HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
          (HomogeneousLocalization.mk
            { deg := m * i,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
              NumDenSameDeg 𝒜 (Submonoid.powers f) })
          (HomogeneousLocalization.mk
            { deg := m * i,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                  (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
                    HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j))
                  sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
              NumDenSameDeg 𝒜 (Submonoid.powers f) })).val
Tactic: split_ifs with h2 h1