awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
s : Finset ι
n : ι → ℕ
m : M
empty :
  ∏ i ∈ ∅, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)
insert :
  ∀ (a : ι) (s : Finset ι) (hi : a ∉ s)
    (hrec :
      ∏ i ∈ s, dp R (n i) m =
        HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)),
    ∏ i ∈ Insert.insert a s, dp R (n i) m =
      HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)
        (dp R ((Insert.insert a s).sum n) m)
⊢ ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)

Tactic:
induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (dp R (n _) m),
      mul_assoc, dp_mul, ← sum_insert hi, nsmul_eq_mul, ← mul_assoc]
    congr 1
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Premises used: Finset.prod_empty, mul_assoc, DividedPowerAlgebra.dp_mul, Insert.insert, DividedPowerAlgebra.dp_zero, Nat.cast_mul, DividedPowerAlgebra.dp, mul_comm, nsmul_eq_mul, Finset.sum_empty, Nat.multinomial_empty, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
s : Finset ι
n : ι → ℕ
m : M
empty :
  ∏ i ∈ ∅, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)
insert :
  ∀ (a : ι) (s : Finset ι) (hi : a ∉ s)
    (hrec :
      ∏ i ∈ s, dp R (n i) m =
        HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)),
    ∏ i ∈ Insert.insert a s, dp R (n i) m =
      HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)
        (dp R ((Insert.insert a s).sum n) m)
⊢ ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (dp R (n _) m),
      mul_assoc, dp_mul, ← sum_insert hi, nsmul_eq_mul, ← mul_assoc]
    congr 1
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Premises used: Finset.prod_empty, mul_assoc, DividedPowerAlgebra.dp_mul, Insert.insert, DividedPowerAlgebra.dp_zero, Nat.cast_mul, DividedPowerAlgebra.dp, mul_comm, nsmul_eq_mul, Finset.sum_empty, Nat.multinomial_empty, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑0! : DividedPowerAlgebra R M) (dp R 0 x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (β := ℕ) (dp R 1 x) 0

Tactic:
simp [dp_zero]

Premises used: DividedPowerAlgebra.dp_zero
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
n : ℕ
h :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n
succ :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(n ! * (n + 1).choose n) : DividedPowerAlgebra R M) (dp R (n + 1) x)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) (n + 1)

Tactic:
rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]

Premises used: pow_succ, mul_assoc, DividedPowerAlgebra.dp_mul, Nat.cast_mul, nsmul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
n : ℕ
h :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(n ! * (n + 1).choose n) : DividedPowerAlgebra R M) (dp R (n + 1) x)

Tactic:
simp [mul_comm _ (n + 1), Nat.factorial_succ]

Premises used: Nat.factorial_succ, HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : M
zero :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑0! : DividedPowerAlgebra R M) (dp R 0 x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (β := ℕ) (dp R 1 x) 0
succ :
  ∀ (n : ℕ)
    (h :
      HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
        HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n),
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
      HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) (n + 1)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n

Tactic:
induction n with
  | zero => simp [dp_zero]
  | succ n h =>
    rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]
    simp [mul_comm _ (n + 1), Nat.factorial_succ]

Premises used: Nat.factorial_succ, pow_succ, mul_assoc, DividedPowerAlgebra.dp_mul, DividedPowerAlgebra.dp_zero, Nat.cast_mul, HAdd.hAdd, mul_comm, nsmul_eq_mul, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 : M
⊢ dp R 1 (x + x_1) = HAdd.hAdd (α := DividedPowerAlgebra R M) (dp R 1 x) (dp R 1 x_1)

Tactic:
simp [dp_add, Nat.antidiagonal_succ, dp_zero, add_comm]

Premises used: Finset.Nat.antidiagonal_succ, DividedPowerAlgebra.dp_zero, add_comm, DividedPowerAlgebra.dp_add
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
x_1 : M
⊢ dp R 1 (x • x_1) =
    HSMul.hSMul (α := R) (β := DividedPowerAlgebra R M) ((RingHom.id R : (a : R) → R) x : R) (dp R 1 x_1)

Tactic:
simp [dp_smul, pow_one, RingHom.id_apply]

Premises used: RingHom.id_apply, pow_one, DividedPowerAlgebra.dp_smul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := DividedPowerAlgebra R M) ((embed R M : (a : M) → DividedPowerAlgebra R M) m : DividedPowerAlgebra R M)
    (dp R 1 m : DividedPowerAlgebra R M)

Tactic:
rfl

Premises used: DividedPowerAlgebra.dp, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
x : ℕ
x_1 : M
rw rw₁ :
  Eq.{u_3 + 1} (α := A) ((g : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
    ((g : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
    ((g : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
refine :
  ∀
    (h :
      ∀ (n : ℕ) (m : M),
        Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
          ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)),
    f = g
⊢ f = g ↔
    ∀ (n : ℕ) (m : M),
      Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
        ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)

Tactic:
refine ⟨fun h _ _ ↦ by rw [h], fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h :
  ∀ (n : ℕ) (m : M),
    Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
      ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
rw :
  Eq (α := (a : DividedPowerAlgebra R M) → A) (⇑f : (a : DividedPowerAlgebra R M) → A)
    (⇑g : (a : DividedPowerAlgebra R M) → A)
⊢ f = g

Tactic:
rw [DFunLike.ext'_iff]

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h :
  ∀ (n : ℕ) (m : M),
    Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
      ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
a :
  Eq (α := MvPolynomial.{u_2, u_1} (ℕ × M) R → A)
    ((fun (g : RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) → A) ↦
        (g ∘ (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) :
          MvPolynomial.{u_2, u_1} (ℕ × M) R → A))
      (⇑f : (a : DividedPowerAlgebra R M) → A))
    ((fun (g : RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) → A) ↦
        (g ∘ (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) :
          MvPolynomial.{u_2, u_1} (ℕ × M) R → A))
      (⇑g : (a : DividedPowerAlgebra R M) → A))
⊢ Eq (α := (a : DividedPowerAlgebra R M) → A) (⇑f : (a : DividedPowerAlgebra R M) → A)
    (⇑g : (a : DividedPowerAlgebra R M) → A)

Tactic:
apply Function.Surjective.injective_comp_right mkAlgHom_surjective

Premises used: Function.Surjective.injective_comp_right, DividedPowerAlgebra.mkAlgHom_surjective
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h :
  ∀ (n : ℕ) (m : M),
    Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
      ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
⊢ Eq (α := MvPolynomial.{u_2, u_1} (ℕ × M) R → A)
    ((fun (g : RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) → A) ↦
        (g ∘ (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) :
          MvPolynomial.{u_2, u_1} (ℕ × M) R → A))
      (⇑f : (a : DividedPowerAlgebra R M) → A))
    ((fun (g : RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) → A) ↦
        (g ∘ (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) :
          MvPolynomial.{u_2, u_1} (ℕ × M) R → A))
      (⇑g : (a : DividedPowerAlgebra R M) → A))

Tactic:
simpa [← AlgHom.coe_comp] using MvPolynomial.algHom_ext fun ⟨n, m⟩ ↦ h n m

Premises used: AlgHom.coe_comp, MvPolynomial.algHom_ext
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h :
  ∀ (n : ℕ) (m : M),
    Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
      ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
⊢ f = g

Tactic:
algHom_ext_iff.mpr h

Premises used: Iff.mpr, DividedPowerAlgebra.algHom_ext_iff
-- 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)) ⊤
rw :
  LE.le (α := Submodule R (DividedPowerAlgebra R M)) ⊤
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
⊢ Eq (α := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- 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)) ⊤
r : R
C :
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (HSMul.hSMul (β := DividedPowerAlgebra R M) r 1)
⊢ 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:
simp only [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- 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)) ⊤
r : R
⊢ Eq (α := DividedPowerAlgebra R M)
    ((fun (n : ι →₀ ℕ) ↦ (n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i) : DividedPowerAlgebra R M)) 0) 1

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)) ⊤
r : R
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    (HSMul.hSMul (β := DividedPowerAlgebra R M) r 1)

Tactic:
exact smul_mem _ _ (subset_span ⟨0, by 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)) ⊤
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 : ℕ) ↦ 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x + y)

Tactic:
Submodule.add_mem _ hx hy

Premises used: Set.Mem, 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)) ⊤
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 : ℕ) ↦ 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 : ℕ) ↦ 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 : ℕ) ↦ dp R k (v i))) (x + y)

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)) ⊤
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
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m

Tactic:
simp [hv, mem_top]

Premises used: Submodule.mem_top
-- 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 : ℕ) ↦ dp R k (v i))) x
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m

Tactic:
have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
-- 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 : ℕ
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)))
    (x * if k = 0 then 1 else 0)
⊢ 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)

Tactic:
rw [dp_null]

Premises used: DividedPowerAlgebra.dp_null
-- 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 : ℕ
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)
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)
⊢ 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)

Tactic:
split_ifs
-- 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 : ℕ
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
h : 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:
simp [hx]
-- 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 : ℕ
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
h : ¬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:
simp [hx]
-- 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
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 : ℕ) ↦ 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)
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 (r • m))

Tactic:
simp [dp_smul, smul_mem _ _ (h x k hx)]

Premises used: DividedPowerAlgebra.dp_smul, 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 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
dp :
  ∀ (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))
⊢ 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)

Tactic:
obtain ⟨i, rfl⟩ := hy

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 : ι
⊢ 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:
simp