awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
hb : b ∈ I
rw :
  Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 a * hI.dpow k.2 b)
    (∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := A) (∑ k ∈ range n.succ, hI.dpow (k, n - k).1 a * hI.dpow (k, n - k).2 b)
    (∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b)
⊢ hI.dpow n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b

Tactic:
rw [hI.dpow_add ha hb, sum_antidiagonal_eq_sum_range_succ_mk]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, DividedPowers.dpow_add
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, dp k.1 a * dp k.2 b
h :
  ∀ (n : ℕ),
    Eq (α := A) ((PowerSeries.coeff n : (a : PowerSeries A) → A) (PowerSeries.mk fun (n : ℕ) ↦ dp n (a + b)) : A)
      ((PowerSeries.coeff n : (a : PowerSeries A) → A)
          (HMul.hMul (α := PowerSeries A) (PowerSeries.mk fun (n : ℕ) ↦ dp n a) (PowerSeries.mk fun (n : ℕ) ↦ dp n b)) :
        A)
⊢ (PowerSeries.mk fun (n : ℕ) ↦ dp n (a + b)) =
    HMul.hMul (α := PowerSeries A) (PowerSeries.mk fun (n : ℕ) ↦ dp n a) (PowerSeries.mk fun (n : ℕ) ↦ dp n b)

Tactic:
ext n
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, dp k.1 a * dp k.2 b
n : ℕ
⊢ Eq (α := A) ((PowerSeries.coeff n : (a : PowerSeries A) → A) (PowerSeries.mk fun (n : ℕ) ↦ dp n (a + b)) : A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        (HMul.hMul (α := PowerSeries A) (PowerSeries.mk fun (n : ℕ) ↦ dp n a) (PowerSeries.mk fun (n : ℕ) ↦ dp n b)) :
      A)

Tactic:
simp only [PowerSeries.coeff_mk, PowerSeries.coeff_mul, dp_add n,
    sum_antidiagonal_eq_sum_range_succ_mk]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, PowerSeries.coeff_mk, PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
ha : a ∈ I
hb : b ∈ I
⊢ hI.exp (a + b) = hI.exp a * hI.exp b

Tactic:
exp_add' _ (fun _ ↦ hI.dpow_add ha hb)

Premises used: DividedPowers.dpow_add, DividedPowers.exp, DividedPowers.exp_add'
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (b • a) = b ^ n • hI.dpow n a

Tactic:
simp only [smul_eq_mul, hI.dpow_mul, ha]

Premises used: DividedPowers.dpow_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
rw : hI.dpow n (b * a) = hI.dpow n a * b ^ n
rw₁ : b ^ n * hI.dpow n a = hI.dpow n a * b ^ n
rw₂ rw₃ : hI.dpow n a * b ^ n = hI.dpow n a * b ^ n
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n

Tactic:
rw [mul_comm, hI.dpow_mul ha, mul_comm]

Premises used: DividedPowers.dpow_mul, mul_comm
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
rw : hI.dpow n (a * b) = hI.dpow n a • b ^ n
rw₁ : hI.dpow n a * b ^ n = hI.dpow n a • b ^ n
rw₂ rw₃ : hI.dpow n a * b ^ n = hI.dpow n a * b ^ n
⊢ hI.dpow n (a • b) = hI.dpow n a • b ^ n

Tactic:
rw [smul_eq_mul, hI.dpow_mul_right ha, smul_eq_mul]

Premises used: DividedPowers.dpow_mul_right, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
zero : (↑1 : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₁ : 1 * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₂ : hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₃ : hI.dpow 0 a = 1
zero₄ zero₅ : Eq.{u_1 + 1} (α := A) 1 1
⊢ (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0

Tactic:
rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]

Premises used: pow_zero, DividedPowers.dpow_zero, Nat.factorial_zero, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1)) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
⊢ (↑(n + 1)! : A) * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
rw [factorial_succ, mul_comm (n + 1)]

Premises used: Nat.factorial_succ, HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
⊢ (↑(n ! * (n + 1)) : A) * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
nth_rewrite 1 [← (n + 1).choose_one_right]

Premises used: Nat.choose_one_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
succ₄ : (↑n ! : A) * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)
succ₅ : a ^ n * hI.dpow 1 a = a ^ (n + 1)
succ₆ : a ^ n * a = a ^ (n + 1)
succ₇ : a ^ n * a = a ^ n * a
succ₈ succ₉ : a * a ^ n = a * a ^ n
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]

Premises used: pow_succ, mul_assoc, DividedPowers.mul_dpow, Nat.choose_symm_add, Nat.cast_mul, mul_comm, DividedPowers.dpow_one
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
zero : (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
succ : ∀ (n : ℕ) (ih : (↑n ! : A) * hI.dpow n a = a ^ n), (↑(n + 1)! : A) * hI.dpow (n + 1) a = a ^ (n + 1)
⊢ (↑n ! : A) * hI.dpow n a = a ^ n

Tactic:
induction n with
  | zero => rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
  | succ n ih =>
    rw [factorial_succ, mul_comm (n + 1)]
    nth_rewrite 1 [← (n + 1).choose_one_right]
    rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]

Premises used: Nat.factorial_succ, pow_succ, mul_assoc, Nat.choose_one_right, DividedPowers.mul_dpow, pow_zero, Nat.choose_symm_add, DividedPowers.dpow_zero, Nat.cast_mul, HAdd.hAdd, mul_comm, Nat.zero, DividedPowers.dpow_one, Nat.factorial_zero, OfNat.ofNat, Nat.succ, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
rw : hI.dpow n (HMul.hMul (α := A) 0 0) = HMul.hMul (α := A) 0 0
rw₁ : HPow.hPow (α := A) 0 n * hI.dpow n 0 = HMul.hMul (α := A) 0 0
rw₂ : 0 * hI.dpow n 0 = HMul.hMul (α := A) 0 0
rw₃ : 0 = HMul.hMul (α := A) 0 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := A) 0 0
⊢ hI.dpow n 0 = 0

Tactic:
rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
    zero_pow hn, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, DividedPowers.dpow_mul, Ideal.zero_mem, OfNat.ofNat, zero_pow
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
rw : (↑n ! : A) * hI.dpow n a = HMul.hMul (α := A) (↑n : A) (↑(n - 1)! : A) * hI.dpow n a
rw₁ : (↑n ! : A) * hI.dpow n a = (↑(n * (n - 1)!) : A) * hI.dpow n a
rw₂ rw₃ : (↑n ! : A) * hI.dpow n a = (↑n ! : A) * hI.dpow n a
⊢ (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a

Tactic:
rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]

Premises used: Nat.cast_mul, nsmul_eq_mul, Nat.mul_factorial_pred
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a

Tactic:
have h_fac : (n ! : A) * hI.dpow n a = n • ((n - 1)! : A) * hI.dpow n a := by
    rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
rw : n • ((↑(n - 1)! : A) * hI.dpow n a) = 0
⊢ a ^ n = 0

Tactic:
rw [← hI.factorial_mul_dpow_eq_pow ha, h_fac, smul_mul_assoc]

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, smul_mul_assoc
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
⊢ n • ((↑(n - 1)! : A) * hI.dpow n a) = 0

Tactic:
hnI (I.mul_mem_left ((n - 1)! : A) (hI.dpow_mem hn ha))

Premises used: DividedPowers.dpow_mem, HSub.hSub, Nat.cast, Nat.factorial, Ideal.mul_mem_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
⊢ n • ((↑(n - 1)! : A) * hI.dpow n a) = 0

Tactic:
exact hnI (I.mul_mem_left ((n - 1)! : A) (hI.dpow_mem hn ha))

Premises used: DividedPowers.dpow_mem, HSub.hSub, Nat.cast, Nat.factorial, Ideal.mul_mem_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a_1 : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
smul : (↑n ! : A) * hJ.dpow n b * hI.dpow n a = (↑n ! : A) * hI.dpow n a * hJ.dpow n b
⊢ hI.dpow n (a • b) = hJ.dpow n (a • b)

Tactic:
rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, DividedPowers.dpow_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a_1 : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ (↑n ! : A) * hJ.dpow n b * hI.dpow n a = (↑n ! : A) * hI.dpow n a * hJ.dpow n b

Tactic:
ring
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
add :
  Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 x * hI.dpow k.2 y)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hJ.dpow k.1 x * hJ.dpow k.2 y)
⊢ hI.dpow n (x + y) = hJ.dpow n (x + y)

Tactic:
rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy),
      hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]

Premises used: Ideal.mul_le_right, DividedPowers.dpow_add, Ideal.mul_le_left
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
add : ∀ x_1 ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y
⊢ Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 x * hI.dpow k.2 y)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hJ.dpow k.1 x * hJ.dpow k.2 y)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
add : k ∈ @antidiagonal _ instAddMonoid _ n → hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
⊢ k ∈ @antidiagonal _ instAddMonoid _ n → hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y

Tactic:
_
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
h : k ∈ @antidiagonal _ instAddMonoid _ n
add : hJ.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
add₁ add₂ : hJ.dpow k.1 x * hJ.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y

Tactic:
rw [hx', hy']
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
ha : a ∈ I • J
smul : ∀ (a : A) (ha : a ∈ I) (b : A) (hb : b ∈ J) {n : ℕ}, hI.dpow n (a • b) = hJ.dpow n (a • b)
add :
  ∀ (x : A) (hx : x ∈ I • J) (y : A) (hy : y ∈ I • J) (hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x)
    (hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y) {n : ℕ}, hI.dpow n (x + y) = hJ.dpow n (x + y)
⊢ hI.dpow n a = hJ.dpow n a

Tactic:
induction ha using Submodule.smul_induction_on' generalizing n with
  | smul a ha b hb =>
    rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]
    ring
  | add x hx y hy hx' hy' =>
    rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy),
      hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]
    apply sum_congr rfl
    intro k _
    rw [hx', hy']

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, DividedPowers.dpow_mul, smul_eq_mul, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
empty : 1 = hI.dpow 0 a
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a

Tactic:
simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]

Premises used: Finset.prod_empty, Finset.sum_empty, Nat.multinomial_empty, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
empty empty₁ : Eq.{u_1 + 1} (α := A) 1 1
⊢ 1 = hI.dpow 0 a

Tactic:
rw [hI.dpow_zero ha]

Premises used: DividedPowers.dpow_zero
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
insert :
  HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ Insert.insert a_1 s, n x) (n a_1)) : A) *
      hI.dpow (∑ x ∈ Insert.insert a_1 s, n x) a =
    (↑(multinomial (Insert.insert a_1 s) n) : A) * hI.dpow ((Insert.insert a_1 s).sum n) a
⊢ ∏ i ∈ Insert.insert a_1 s, hI.dpow (n i) a =
    (↑(multinomial (Insert.insert a_1 s) n) : A) * hI.dpow ((Insert.insert a_1 s).sum n) a

Tactic:
rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]

Premises used: Finset.prod_insert, mul_assoc, DividedPowers.mul_dpow, DividedPowers.dpow, mul_comm, Finset.sum_insert
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
apply :
  HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑(multinomial (insert a_1 s) n) : A)
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) *
      hI.dpow (∑ x ∈ insert a_1 s, n x) a =
    (↑(multinomial (insert a_1 s) n) : A) * hI.dpow ((insert a_1 s).sum n) a

Tactic:
apply congr_arg₂ _ _ rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
rw :
  HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
rw₁ :
  HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
rw₂ :
  HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
    HMul.hMul (α := A) (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1)) : A) (↑(multinomial s n) : A)
rw₃ rw₄ :
  HMul.hMul (α := A) (↑((n a_1 + ∑ x ∈ s, n x).choose (n a_1)) : A) (↑(multinomial s n) : A) =
    HMul.hMul (α := A) (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1)) : A) (↑(multinomial s n) : A)
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑(multinomial (insert a_1 s) n) : A)

Tactic:
rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Premises used: Nat.cast_mul, Nat.multinomial_insert, mul_comm, Finset.sum_insert
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
empty : ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
insert :
  ∀ (a_1 : ι) (s : Finset ι) (hi : a_1 ∉ s)
    (hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a),
    ∏ i ∈ Insert.insert a_1 s, hI.dpow (n i) a =
      (↑(multinomial (Insert.insert a_1 s) n) : A) * hI.dpow ((Insert.insert a_1 s).sum n) a
⊢ ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a

Tactic:
induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Premises used: Finset.prod_empty, mul_assoc, Insert.insert, DividedPowers.mul_dpow, DividedPowers.dpow_zero, Nat.cast_mul, DividedPowers.dpow, mul_comm, Finset.sum_empty, Nat.multinomial_empty, Nat.cast_one, one_mul, rfl, congr_arg₂
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
empty : ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
insert :
  ∀ (a_1 : ι) (s : Finset ι) (hi : a_1 ∉ s)
    (hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a),
    ∏ i ∈ Insert.insert a_1 s, hI.dpow (n i) a =
      (↑(multinomial (Insert.insert a_1 s) n) : A) * hI.dpow ((Insert.insert a_1 s).sum n) a
⊢ ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Premises used: Finset.prod_empty, mul_assoc, Insert.insert, DividedPowers.mul_dpow, DividedPowers.dpow_zero, Nat.cast_mul, DividedPowers.dpow, mul_comm, Finset.sum_empty, Nat.multinomial_empty, Nat.cast_one, one_mul, rfl, congr_arg₂
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_add :
  ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, dpow k.1 x * dpow k.2 y
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
s : Finset ι
x : ι → M
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
⊢ ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y

Tactic:
simp only [sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
empty : dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
⊢ dpow n (Finset.sum ∅ x) = ∑ k ∈ Finset.sym ∅ n, ∏ i ∈ ∅, dpow (Multiset.count i (↑k : Multiset ι)) (x i)

Tactic:
simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]

Premises used: Finset.prod_empty, nsmul_eq_mul, Finset.sum_empty, mul_one, Finset.sum_const
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
pos : ∀ (hn : n = 0), dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
neg : ∀ (hn : ¬n = 0), dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : n = 0
pos : dpow 0 0 = (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)

Tactic:
rw [hn]