Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
by_cases hkm : m + k < n
State after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : m + k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : ¬m + k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

State before:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : m + k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
exact dpow_mul_dif_pos hn_fac hkm hx
State after:
no goals

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : ¬m + k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
have hxmk : x ^ (m + k) = 0 := Ideal.mem_pow_eq_zero n (m + k) hnI (not_lt.mp hkm) hx
State after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : ¬m + k < n
hxmk : x ^ (m + k) = 0
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : ¬m + k < n
hxmk : x ^ (m + k) = 0
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
rw [dpow_eq_of_mem m hx, dpow_eq_of_mem k hx, dpow_eq_of_mem (m + k) hx,
  mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
  MulZeroClass.mul_zero, MulZeroClass.mul_zero, MulZeroClass.mul_zero, MulZeroClass.mul_zero]
State after:
no goals