Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
have hm : m < n := lt_of_le_of_lt le_self_add hkm
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
have hk : k < n := lt_of_le_of_lt le_add_self hkm
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Tactic:
rw [dpow_eq_of_mem _ hx, dpow_eq_of_mem _ hx, dpow_eq_of_mem _ hx,
  mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m),
  ← pow_add, ← mul_assoc, ← mul_assoc]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! * x ^ (m + k) = ↑((m + k).choose m) * 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! * x ^ (m + k) = ↑((m + k).choose m) * 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! = ↑((m + k).choose m) * Ring.inverse ↑(m + k)!

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ Ring.inverse ↑m ! * Ring.inverse ↑k ! = ↑((m + k).choose m) * 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 hm),
    Ring.inverse_mul_eq_iff_eq_mul _ _ _ (factorial_isUnit hn_fac hk)]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ ↑(m + k)! = ↑k ! * (↑m ! * ↑((m + k).choose m))

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ ↑(m + k)! = ↑k ! * (↑m ! * ↑((m + k).choose m))
Tactic:
norm_cast
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ ↑(m + k)! = ↑(k ! * (m ! * (m + k).choose m))

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ ↑(m + k)! = ↑(k ! * (m ! * (m + k).choose m))
Tactic:
apply congr_arg
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)
Tactic:
rw [← Nat.add_choose_mul_factorial_mul_factorial, mul_comm, mul_comm _ (m !), Nat.choose_symm_add]
State after:
no goals