-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx :
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i))) x
i : ι
dp :
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
    (HMul.hMul (α := DividedPowerAlgebra R M) 0 (DividedPowerAlgebra.dp R k (v i)))
dp₁ :
  ∀ (x : DividedPowerAlgebra R M)
    (hx :
      Membership.mem (γ := Set (DividedPowerAlgebra R M))
        (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)) x),
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
      (x * DividedPowerAlgebra.dp R k (v i))
dp₂ :
  ∀ (x y : DividedPowerAlgebra R M)
    (hxmem :
      Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
        (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
        x)
    (hymem :
      Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
        (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
        y)
    (hx :
      Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
        (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
        (x * DividedPowerAlgebra.dp R k (v i)))
    (hy :
      Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
        (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
        (y * DividedPowerAlgebra.dp R k (v i))),
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
      ((x + y) * DividedPowerAlgebra.dp R k (v i))
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
    (x * DividedPowerAlgebra.dp R k (v i))
have dp₃ : ∀ (r : R) (x : DividedPowerAlgebra R M)
  (hxmem :
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i))) x)
  (hx :
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
      (x * DividedPowerAlgebra.dp R k (v i))),
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
    (r • x * DividedPowerAlgebra.dp R k (v i))
Tactic: induction hx using span_induction with
      | zero => simp
      | mem x hx =>
        obtain ⟨n, rfl⟩ := hx
        simp only
        rw [← n.mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i)), mul_comm,
          ← mul_assoc, dp_mul, nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul]
        refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
        simp only
        rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]
        simp
      | add x y hxmem hymem hx hy =>
        rw [add_mul]
        exact Submodule.add_mem _ hx hy
      | smul r x hxmem hx =>
        rw [smul_mul_assoc]
        exact smul_mem _ _ hx
Cleared hypotheses: hx