-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
intro intro₁ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) z
intro₂ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (∑
        i ∈
          DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z :
                  DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              i) :
          A))
intro₃ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z)
    (c : ℕ)
    (hc :
      Membership.mem (γ := Finset ℕ)
        (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
        c)
    (hc0 : c = 0),
    Membership.mem (γ := Ideal A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            c) :
        A)
h :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z)
    (c : ℕ)
    (hc :
      Membership.mem (γ := Finset ℕ)
        (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
        c)
    (hc0 : c = 0),
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            c) :
        A) =
      0
⊢ LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
have h₁ : ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z)
  (hc :
    Membership.mem (γ := Finset ℕ)
      (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
      0),
  (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          0) :
      A) =
    0
Tactic: classical
  intro z hz
  rw [← DirectSum.sum_support_decompose 𝒜 z]
  refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
  convert! Ideal.zero_mem _
  subst hc0
  exact hz