Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp (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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x
Tactic:
by_cases hmk : 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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : m * k < n
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * 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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : ¬m * k < n
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * 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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : m * k < n
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x
Tactic:
exact dpow_comp_dif_pos hn_fac hk hmk 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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : ¬m * k < n
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x
Tactic:
have hxmk : x ^ (m * k) = 0 := Ideal.mem_pow_eq_zero n (m * k) hnI (not_lt.mp hmk) 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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : ¬m * k < n
hxmk : x ^ (m * k) = 0
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * 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 : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : ¬m * k < n
hxmk : x ^ (m * k) = 0
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x
Tactic:
rw [dpow_eq_of_mem _ (dpow_mem hk hx), dpow_eq_of_mem _ hx, dpow_eq_of_mem _ hx,
  mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk,
  MulZeroClass.mul_zero, MulZeroClass.mul_zero, MulZeroClass.mul_zero]
State after:
no goals