-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
this : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hf₁ :
  ∀ (x : A) (hx : x ∈ Set.range f),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hf₂ :
  ∀ (r : ↥(𝒜 0)),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A))
hf₃ :
  ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x)
    (hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
        (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)) →
      Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
          (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)) →
        Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
          (HSub.hSub (β := A) (x + y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x + y) : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
have hf₄ : ∀ (x y : A) (hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x)
  (hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y)
  (hx' :
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)))
  (hy' :
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A))
Tactic: induction this using Algebra.adjoin_induction with
  | mem x hx =>
    obtain ⟨i, rfl⟩ := hx
    obtain ⟨n, hn⟩ := hfn i
    rw [GradedRing.projZeroRingHom_apply]
    by_cases hn' : n = 0
    · rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
      exact zero_mem _
    · rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
      exact Ideal.subset_span ⟨_, rfl⟩
  | algebraMap r =>
    convert! zero_mem (Ideal.span _)
    rw [sub_eq_zero]
    exact (DirectSum.decompose_of_mem_same 𝒜 r.2).symm
  | add x y hx hy _ _ =>
    rw [map_add, add_sub_add_comm]
    exact add_mem ‹_› ‹_›
  | mul x y hx hy hx' hy' =>
    convert!
      add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1
    rw [map_mul]
    ring
Cleared hypotheses: this