awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i)))
    (x * if k = 0 then 1 else 0)
have pos : k = 0 →
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * 1)
Tactic: split_ifs
-- 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 : ℕ) ↦ dp R k (v i))) x
pos :
  k = 0 →
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * 1)
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (x * if k = 0 then 1 else 0)
have neg : ¬k = 0 →
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * 0)
Tactic: split_ifs
-- 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 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * dp R k y)
have dp : ∀ (i : ι),
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * dp R k (v i))
Tactic: obtain ⟨i, rfl⟩ := hy
Cleared hypotheses: y, hy
-- 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_1 : DividedPowerAlgebra R M
k : ℕ
i : ι
x : DividedPowerAlgebra R M
hx :
  Membership.mem (γ := Set (DividedPowerAlgebra R M))
    (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * dp R k (v i))
have dp : ∀ (n : ι →₀ ℕ),
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (HMul.hMul (α := DividedPowerAlgebra R M)
      ((fun (n : ι →₀ ℕ) ↦ (n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i) : DividedPowerAlgebra R M)) n) (dp R k (v i)))
Tactic: obtain ⟨n, rfl⟩ := hx
Cleared hypotheses: x, hx
-- 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 : ℕ
i : ι
n : ι →₀ ℕ
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (HMul.hMul (α := DividedPowerAlgebra R M) (n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)) (dp R k (v i)))
have dp : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  ((HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)).choose k •
    HMul.hMul (α := DividedPowerAlgebra R M) (dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
      ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
Tactic: 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]
-- 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 : ℕ
i : ι
n : ι →₀ ℕ
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    ((HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)).choose k •
      HMul.hMul (α := DividedPowerAlgebra R M) (dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
        ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
have dp : (fun (n : ι →₀ ℕ) ↦ (n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i) : DividedPowerAlgebra R M)) (Finsupp.single i k + n) =
  HMul.hMul (α := DividedPowerAlgebra R M) (dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
    ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))
Tactic: refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
-- 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 : ℕ
i : ι
n : ι →₀ ℕ
⊢ ((Finsupp.single i k + n).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)) =
    HMul.hMul (α := DividedPowerAlgebra R M) (dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
      ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))
have dp : HMul.hMul (α := DividedPowerAlgebra R M) (dp R ((Finsupp.single i k + n : (a : ι) → ℕ) i) (v i))
    ((Finsupp.erase i (Finsupp.single i k + n)).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)) =
  HMul.hMul (α := DividedPowerAlgebra R M) (dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
    ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))
Tactic: rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]
-- 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_1 : DividedPowerAlgebra R M
k : ℕ
i : ι
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 : ℕ) ↦ 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ dp R k (v i))) (y * dp R k (v i))
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) ((x + y) * dp R k (v i))
have dp : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  (x * dp R k (v i) + y * dp R k (v i))
Tactic: rw [add_mul]
-- 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_1 : DividedPowerAlgebra R M
k : ℕ
i : ι
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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * dp R k (v i))
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (r • x * dp R k (v i))
have dp : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (r • (x * dp R k (v i)))
Tactic: rw [smul_mul_assoc]
-- 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 : ℕ) ↦ dp R k (v i))) x
i : ι
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * dp R k (v i))
have dp : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  (HMul.hMul (α := DividedPowerAlgebra R M) 0 (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
-- 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)))
⊢ 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₁ : ∀ (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))
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
-- 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_1 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * dp R k (m + n))
have dp : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ k, x * HMul.hMul (α := DividedPowerAlgebra R M) (dp R i.1 m) (dp R i.2 n))
Tactic: rw [dp_add, mul_sum]
-- 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_1 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i)))
    (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      x * HMul.hMul (α := DividedPowerAlgebra R M) (dp R i.1 m) (dp R i.2 n))
have apply : ∀ (c : ℕ × ℕ) (hc : c ∈ @antidiagonal _ Nat.instAddMonoid _ k),
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (x * HMul.hMul (α := DividedPowerAlgebra R M) (dp R c.1 m) (dp R c.2 n))
Tactic: apply sum_mem (fun c hc ↦ ?_)
-- 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_1 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * 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 : ℕ) ↦ dp R k (v i))) x
c : ℕ × ℕ
hc : c ∈ @antidiagonal _ Nat.instAddMonoid _ k
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (x * HMul.hMul (α := DividedPowerAlgebra R M) (dp R c.1 m) (dp R c.2 n))
have rw : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  (x * dp R c.1 m * dp R c.2 n)
Tactic: rw [← mul_assoc]
-- 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)) ⊤
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 : ℕ) ↦ dp R k (v i))) x
hm : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * dp R k m)
have 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x * dp R k 0)
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)
Cleared hypotheses: x, k, hx, hm
-- 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)) ⊤
p : DividedPowerAlgebra R M
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) p
have 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 : ℕ) ↦ dp R k (v i)))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) r : DividedPowerAlgebra R M)
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)
Cleared hypotheses: p