awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ⊤
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 : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)) x
dp :
  ∀ (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)))
      (HMul.hMul (α := DividedPowerAlgebra R M)
        ((fun (n : ι →₀ ℕ) ↦ (n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i) : DividedPowerAlgebra R M))
          n)
        (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))

Tactic:
obtain ⟨n, rfl⟩ := hx

Premises used: rfl
-- 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)) ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
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)))
    ((HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)).choose k •
      HMul.hMul (α := DividedPowerAlgebra R M)
        (DividedPowerAlgebra.dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
        ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ 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)))
    (HMul.hMul (α := DividedPowerAlgebra R M) (n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i))
      (DividedPowerAlgebra.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]

Premises used: mul_assoc, DividedPowerAlgebra.dp_mul, mul_comm, nsmul_eq_mul, Finsupp.mul_prod_erase'
-- 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)) ⊤
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)))

Tactic:
smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)

Premises used: HAdd.hAdd, Submodule.mem_span_of_mem, Exists.intro, Submodule.smul_of_tower_mem, Finsupp.single
-- 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)) ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
dp :
  (fun (n : ι →₀ ℕ) ↦ (n.prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i) : DividedPowerAlgebra R M))
      (Finsupp.single i k + n) =
    HMul.hMul (α := DividedPowerAlgebra R M)
      (DividedPowerAlgebra.dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
      ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ 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)))
    ((HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)).choose k •
      HMul.hMul (α := DividedPowerAlgebra R M)
        (DividedPowerAlgebra.dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
        ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)))

Tactic:
refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
-- 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)) ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
dp :
  HMul.hMul (α := DividedPowerAlgebra R M) (DividedPowerAlgebra.dp R ((Finsupp.single i k + n : (a : ι) → ℕ) i) (v i))
      ((Finsupp.erase i (Finsupp.single i k + n)).prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)) =
    HMul.hMul (α := DividedPowerAlgebra R M)
      (DividedPowerAlgebra.dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
      ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i))
⊢ ((Finsupp.single i k + n).prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i)) =
    HMul.hMul (α := DividedPowerAlgebra R M)
      (DividedPowerAlgebra.dp R (HAdd.hAdd (β := ℕ) k ((n : (a : ι) → ℕ) i : ℕ)) (v i))
      ((Finsupp.erase i n).prod fun (i : ι) (k : ℕ) ↦ DividedPowerAlgebra.dp R k (v i))

Tactic:
rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]

Premises used: HAdd.hAdd, Finsupp.mul_prod_erase', Finsupp.single
-- 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)) ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ 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:
simp
-- 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)) ⊤
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 : ℕ) ↦ 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))
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)))
    (x * 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))

Tactic:
rw [add_mul]

Premises used: add_mul
-- 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)) ⊤
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 * dp R k (v i) + y * dp R k (v i))

Tactic:
Submodule.add_mem _ hx hy

Premises used: Submodule.add_mem
-- 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)) ⊤
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 * dp R k (v i) + y * dp R k (v i))

Tactic:
exact Submodule.add_mem _ hx hy

Premises used: Submodule.add_mem
-- 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)) ⊤
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 : ℕ) ↦ 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))
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)))
    (r • (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:
rw [smul_mul_assoc]

Premises used: smul_mul_assoc
-- 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)) ⊤
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)))

Tactic:
smul_mem _ _ hx

Premises used: Submodule.smul_mem
-- 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)) ⊤
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)))

Tactic:
exact smul_mem _ _ hx

Premises used: Submodule.smul_mem
-- 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)) ⊤
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 : ℕ) ↦ 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
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)))
    (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      x * HMul.hMul (α := DividedPowerAlgebra R M) (DividedPowerAlgebra.dp R i.1 m) (DividedPowerAlgebra.dp R i.2 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 + n))

Tactic:
rw [dp_add, mul_sum]

Premises used: Finset.mul_sum, DividedPowerAlgebra.dp_add
-- 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)) ⊤
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
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))
⊢ 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:
apply sum_mem (fun c hc ↦ ?_)

Premises used: sum_mem
-- 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)) ⊤
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
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)
⊢ 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:
rw [← mul_assoc]

Premises used: mul_assoc
-- 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)) ⊤
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 * dp R c.1 m * dp R c.2 n)

Tactic:
hn (x * dp R c.1 m) c.2 (hm x c.1 hx)

Premises used: HMul.hMul, Set.Mem, Prod.fst, DividedPowerAlgebra.dp, Prod.snd
-- 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)) ⊤
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 * dp R c.1 m * dp R c.2 n)

Tactic:
exact hn (x * dp R c.1 m) c.2 (hm x c.1 hx)

Premises used: HMul.hMul, Prod.fst, DividedPowerAlgebra.dp, Prod.snd