Theorem: DividedPowers.factorial_mul_dpow_eq_pow (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
x : A
hx : x ∈ I
⊢ ↑n.factorial * hI.dpow n x = x ^ n
Tactic:
induction n with
| zero => rw [Nat.factorial_zero, Nat.cast_one, one_mul, pow_zero, hI.dpow_zero hx]
| add_one n ih =>
  rw [Nat.factorial_succ, mul_comm (n + 1)]
  nth_rewrite 1 [← (n + 1).choose_one_right]
  rw [← Nat.choose_symm_add, Nat.cast_mul, mul_assoc,
    ← hI.dpow_mul n 1 hx, ← mul_assoc, ih, hI.dpow_one hx, pow_succ', mul_comm]
State after:
no goals

State before:
case zero
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
⊢ ↑(Nat.factorial 0) * hI.dpow 0 x = x ^ 0
Tactic:
rw [Nat.factorial_zero, Nat.cast_one, one_mul, pow_zero, hI.dpow_zero hx]
State after:
no goals

State before:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n + 1).factorial * hI.dpow (n + 1) x = x ^ (n + 1)
Tactic:
rw [Nat.factorial_succ, mul_comm (n + 1)]
State after:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1)) * hI.dpow (n + 1) x = x ^ (n + 1)

State before:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1)) * hI.dpow (n + 1) x = x ^ (n + 1)
Tactic:
nth_rewrite 1 [← (n + 1).choose_one_right]
State after:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1).choose 1) * hI.dpow (n + 1) x = x ^ (n + 1)

State before:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1).choose 1) * hI.dpow (n + 1) x = x ^ (n + 1)
Tactic:
rw [← Nat.choose_symm_add, Nat.cast_mul, mul_assoc,
  ← hI.dpow_mul n 1 hx, ← mul_assoc, ih, hI.dpow_one hx, pow_succ', mul_comm]
State after:
no goals