-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
i : ι
b : B
hb : Membership.mem (γ := Submodule B B) (Ideal.span ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) b
zero :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑(((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) 0 : (a : ι) → ↥(ℬ a)) i) : B)
add :
  ∀ (x y : B),
    Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) x →
      Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) y →
        (∀ (i : ι),
            Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
              (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) x :
                        DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                      (a : ι) → ↥(ℬ a))
                    i) :
                B)) →
          (∀ (i : ι),
              Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
                (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) y :
                          DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                        (a : ι) → ↥(ℬ a))
                      i) :
                  B)) →
            ∀ (i : ι),
              Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
                (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) (x + y) :
                          DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                        (a : ι) → ↥(ℬ a))
                      i) :
                  B)
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) b :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
have mem : ∀ (a : B) (ha : Membership.mem (γ := Set B) ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A)) a) (i : ι),
  Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
Tactic: induction hb using Submodule.span_induction generalizing i with
    | zero => simp
    | add => simp [*, Ideal.add_mem]
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      rw [← f.map_directSumDecompose]
      exact Ideal.mem_map_of_mem _ (I.2 _ ha)
    | smul a₁ a₂ ha₂ ih =>
      classical rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]
      exact sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _
Cleared hypotheses: i, hb