-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
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)) ⊤
p : DividedPowerAlgebra R M
C :
  ∀ (r : R),
    Membership.mem (α := DividedPowerAlgebra R M) (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))
      ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) r : DividedPowerAlgebra R M)
add :
  ∀ (x y : DividedPowerAlgebra R M)
    (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)
    (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),
    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)
dp :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ) (m : M)
    (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),
    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 m)
⊢ 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))) p

Tactic:
induction p using DividedPowerAlgebra.induction_on with
  | C r =>
    simp only [Algebra.algebraMap_eq_smul_one]
    exact smul_mem _ _ (subset_span ⟨0, by simp⟩)
  | add x y hx hy => exact Submodule.add_mem _ hx hy
  | dp x k m hx =>
    have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
    induction hm using span_induction generalizing x k with
    | zero => rw [dp_null]; split_ifs <;> simp [hx]
    | smul r m hm h => simp [dp_smul, smul_mem _ _ (h x k hx)]
    | mem y hy =>
      obtain ⟨i, rfl⟩ := hy
      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
    | add m n hm_mem hn_mem hm hn =>
      rw [dp_add, mul_sum]
      apply sum_mem (fun c hc ↦ ?_)
      rw [← mul_assoc]
      exact hn (x * dp R c.1 m) c.2 (hm x c.1 hx)

Premises used: add_mul, Finset.mul_sum, mul_assoc, DividedPowerAlgebra.dp_mul, smul_mul_assoc, Algebra.algebraMap_eq_smul_one, DividedPowerAlgebra.dp, mul_comm, nsmul_eq_mul, Submodule.zero, Submodule.add, DividedPowerAlgebra.dp_smul, MvPolynomial.C, DividedPowerAlgebra.dp_add, sum_mem, rfl, DividedPowerAlgebra.dp_null