internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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]
Proof 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)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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
Proof 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)!
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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)]
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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
Proof 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)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul_dif_pos
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mul
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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)]
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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]
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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]
Proof 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)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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
Proof 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)!
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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)]
Proof 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)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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)]
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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]
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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]
Proof 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))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp_dif_pos
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp
Proof 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
Proof 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
Theorem: DividedPowers.OfInvertibleFactorial.dpow_comp
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.OfSquareZero.dpow_of_two_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ (dividedPowers hI2).dpow n a = 0
Tactic:
simp only [dividedPowers, OfInvertibleFactorial.dpow_def, ite_eq_right_iff]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ a ∈ I → Ring.inverse ↑n ! * a ^ n = 0
Theorem: DividedPowers.OfSquareZero.dpow_of_two_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ a ∈ I → Ring.inverse ↑n ! * a ^ n = 0
Tactic:
intro ha
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ Ring.inverse ↑n ! * a ^ n = 0
Theorem: DividedPowers.OfSquareZero.dpow_of_two_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ Ring.inverse ↑n ! * a ^ n = 0
Tactic:
suffices h : a ^ n = 0 by
  rw [h, mul_zero]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ a ^ n = 0
Theorem: DividedPowers.OfSquareZero.dpow_of_two_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ a ^ n = 0
Tactic:
exact Ideal.mem_pow_eq_zero 2 n hI2 hn ha
Proof state after:
no goals
Theorem: DividedPowers.OfSquareZero.dpow_of_two_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
h : a ^ n = 0
⊢ Ring.inverse ↑n ! * a ^ n = 0
Tactic:
rw [h, mul_zero]
Proof state after:
no goals
Theorem: DividedPowers.RatAlgebra.dpow_eq_of_mem
Proof state before:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
n : ℕ
x : R
hx : x ∈ I
⊢ dpow I n x = Ring.inverse ↑n ! * x ^ n
Tactic:
rw [dpow, OfInvertibleFactorial.dpow_eq_of_mem _ hx]
Proof state after:
no goals
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = Ring.inverse ↑n ! • x ^ n
Tactic:
simp only [Ring.inverse_eq_inv']
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • x ^ n
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • x ^ n
Tactic:
rw [← factorial_mul_dpow_eq_pow hI n x hx]
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • (↑n ! * hI.dpow n x)
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • (↑n ! * hI.dpow n x)
Tactic:
rw [← smul_eq_mul]
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • ↑n ! • hI.dpow n x
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • ↑n ! • hI.dpow n x
Tactic:
rw [← smul_assoc]
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Tactic:
nth_rewrite 1 [← one_smul R (hI.dpow n x)]
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 • hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 • hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Tactic:
congr
Proof state after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 = (↑n !)⁻¹ • ↑n !
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 = (↑n !)⁻¹ • ↑n !
Tactic:
have this_rat : ((n !) : R) = (n ! : ℚ) • (1 : R) := by
  rw [← nsmul_eq_smul_cast, nsmul_eq_mul, mul_one]
Proof state after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = (↑n !)⁻¹ • ↑n !
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = (↑n !)⁻¹ • ↑n !
Tactic:
rw [this_rat, ← mul_smul]
Proof state after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1
Tactic:
suffices (n ! : ℚ)⁻¹ * (n !) = 1 by
  rw [this, one_smul]
Proof state after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ (↑n !)⁻¹ * ↑n ! = 1
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ (↑n !)⁻¹ * ↑n ! = 1
Tactic:
apply Rat.inv_mul_cancel
Proof state after:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ↑n ! ≠ 0