-- 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)) ⊤
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
hm : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m
dp :
  ∀ (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),
    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 0)
dp₁ :
  ∀ (r : R) (m : M) (hm : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m)
    (h :
      ∀ (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),
        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))
    (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),
    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 (r • m))
dp₂ :
  ∀ (y : M) (hy : y ∈ Set.range v) (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),
    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 y)
dp₃ :
  ∀ (m n : M) (hm_mem : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m)
    (hn_mem : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) n)
    (hm :
      ∀ (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),
        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))
    (hn :
      ∀ (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),
        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 n))
    (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),
    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 + n))
⊢ 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)

Tactic:
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, mul_comm, nsmul_eq_mul, Submodule.zero, Submodule.add, DividedPowerAlgebra.dp_smul, DividedPowerAlgebra.dp_add, sum_mem, rfl, Submodule.smul_mem, DividedPowerAlgebra.dp_null