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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x
Tactic:
have hmn : m < n := lt_of_le_of_lt (Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero hk)) hkm
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ dpow I m (dpow I k x) = ↑(mchoose m k) * dpow I (m * k) x
Tactic:
rw [dpow_eq_of_mem (m * k) hx, dpow_eq_of_mem _ (dpow_mem hk hx)]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ Ring.inverse ↑m ! * dpow I k x ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))

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

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
⊢ Ring.inverse ↑m ! * dpow I k x ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))

State before:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : m = 0
⊢ Ring.inverse ↑m ! * dpow I k x ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))
Tactic:
simp only [hm0, MulZeroClass.zero_mul, _root_.pow_zero, mul_one, mchoose_zero, Nat.cast_one, one_mul]
State after:
no goals

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
⊢ Ring.inverse ↑m ! * dpow I k x ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))
Tactic:
have hkn : k < n := lt_of_le_of_lt (Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero hm0)) hkm
State after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * dpow I k x ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * dpow I k x ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))
Tactic:
rw [dpow_eq_of_mem _ hx]
State after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * (Ring.inverse ↑k ! * x ^ k) ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * (Ring.inverse ↑k ! * x ^ k) ^ m = ↑(mchoose m k) * (Ring.inverse ↑(m * k)! * x ^ (m * k))
Tactic:
rw [mul_pow, ← pow_mul, mul_comm k, ← mul_assoc, ← mul_assoc]
State after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! ^ m * x ^ (m * k) = ↑(mchoose m k) * Ring.inverse ↑(m * k)! * x ^ (m * k)

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! ^ m * x ^ (m * k) = ↑(mchoose m k) * Ring.inverse ↑(m * k)! * x ^ (m * k)
Tactic:
apply congr_arg₂ _ _ rfl
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! ^ m = ↑(mchoose m k) * Ring.inverse ↑(m * k)!

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! ^ m = ↑(mchoose m k) * Ring.inverse ↑(m * k)!
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ (factorial_isUnit hn_fac hkm),
  mul_assoc, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (factorial_isUnit hn_fac hmn)]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑k ! ^ m * ↑(m * k)! = ↑m ! * ↑(mchoose m k)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ Ring.inverse ↑k ! ^ m * ↑(m * k)! = ↑m ! * ↑(mchoose m k)
Tactic:
rw [Ring.inverse_pow_mul_eq_iff_eq_mul _ _ (factorial_isUnit hn_fac hkn)]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m * k)! = ↑k ! ^ m * (↑m ! * ↑(mchoose m k))

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m * k)! = ↑k ! ^ m * (↑m ! * ↑(mchoose m k))
Tactic:
rw [← mchoose_lemma _ hk]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m ! * k ! ^ m * mchoose m k) = ↑k ! ^ m * (↑m ! * ↑(mchoose m k))

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m ! * k ! ^ m * mchoose m k) = ↑k ! ^ m * (↑m ! * ↑(mchoose m k))
Tactic:
simp only [Nat.cast_mul, Nat.cast_pow]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑m ! * ↑k ! ^ m * ↑(mchoose m k) = ↑k ! ^ m * (↑m ! * ↑(mchoose m k))

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑m ! * ↑k ! ^ m * ↑(mchoose m k) = ↑k ! ^ m * (↑m ! * ↑(mchoose m k))
Tactic:
rw [mul_comm (m ! : A), mul_assoc]
State after:
no goals