internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! = ↑m ! * Ring.inverse ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! * ↑k.1! = ↑m !

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! * ↑k.1! = ↑m !
Tactic:
rw [← hk, ← Nat.cast_mul, ← Nat.cast_mul, add_comm, Nat.add_choose_mul_factorial_mul_factorial]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.1!
Tactic:
apply factorial_isUnit' hm
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ m
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ m
Tactic:
rw [← hk]
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ k.1 + k.2
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ k.1 + k.2
Tactic:
exact Nat.le_add_right k.1 k.2
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!
Tactic:
apply factorial_isUnit' hm
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ m
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ m
Tactic:
rw [← hk]
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ k.1 + k.2
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ k.1 + k.2
Tactic:
exact Nat.le_add_left k.2 k.1
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
rw [dpow_eq_of_mem m (Ideal.add_mem I hx hy)]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ Ring.inverse ↑m ! * (x + y) ^ m = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ Ring.inverse ↑m ! * (x + y) ^ m = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
simp only [dpow]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ Ring.inverse ↑m ! * (x + y) ^ m =
    ∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ Ring.inverse ↑m ! * (x + y) ^ m =
    ∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0
Tactic:
rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (factorial_isUnit hn_fac hmn), Finset.mul_sum, Commute.add_pow' (Commute.all _ _)]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ ∑ m_1 ∈ Finset.antidiagonal m, m.choose m_1.1 • (x ^ m_1.1 * y ^ m_1.2) =
    ∑ i ∈ Finset.antidiagonal m,
      ↑m ! * ((if x ∈ I then Ring.inverse ↑i.1! * x ^ i.1 else 0) * if y ∈ I then Ring.inverse ↑i.2! * y ^ i.2 else 0)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ ∑ m_1 ∈ Finset.antidiagonal m, m.choose m_1.1 • (x ^ m_1.1 * y ^ m_1.2) =
    ∑ i ∈ Finset.antidiagonal m,
      ↑m ! * ((if x ∈ I then Ring.inverse ↑i.1! * x ^ i.1 else 0) * if y ∈ I then Ring.inverse ↑i.2! * y ^ i.2 else 0)
Tactic:
apply Finset.sum_congr rfl
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ ∀ x_1 ∈ Finset.antidiagonal m,
    m.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) =
      ↑m ! *
        ((if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) *
          if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ ∀ x_1 ∈ Finset.antidiagonal m,
    m.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) =
      ↑m ! *
        ((if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) *
          if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0)
Tactic:
intro k hk
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) =
    ↑m ! * ((if x ∈ I then Ring.inverse ↑k.1! * x ^ k.1 else 0) * if y ∈ I then Ring.inverse ↑k.2! * y ^ k.2 else 0)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) =
    ↑m ! * ((if x ∈ I then Ring.inverse ↑k.1! * x ^ k.1 else 0) * if y ∈ I then Ring.inverse ↑k.2! * y ^ k.2 else 0)
Tactic:
rw [if_pos hx, if_pos hy]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) = ↑m ! * (Ring.inverse ↑k.1! * x ^ k.1 * (Ring.inverse ↑k.2! * y ^ k.2))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) = ↑m ! * (Ring.inverse ↑k.1! * x ^ k.1 * (Ring.inverse ↑k.2! * y ^ k.2))
Tactic:
ring_nf
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ x ^ k.1 * y ^ k.2 * ↑(m.choose k.1) = x ^ k.1 * y ^ k.2 * ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ x ^ k.1 * y ^ k.2 * ↑(m.choose k.1) = x ^ k.1 * y ^ k.2 * ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Tactic:
simp only [mul_assoc]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ x ^ k.1 * (y ^ k.2 * ↑(m.choose k.1)) = x ^ k.1 * (y ^ k.2 * (↑m ! * (Ring.inverse ↑k.1! * Ring.inverse ↑k.2!)))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ x ^ k.1 * (y ^ k.2 * ↑(m.choose k.1)) = x ^ k.1 * (y ^ k.2 * (↑m ! * (Ring.inverse ↑k.1! * Ring.inverse ↑k.2!)))
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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * ↑(m.choose k.1) = y ^ k.2 * (↑m ! * (Ring.inverse ↑k.1! * Ring.inverse ↑k.2!))
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * ↑(m.choose k.1) = y ^ k.2 * (↑m ! * (Ring.inverse ↑k.1! * Ring.inverse ↑k.2!))
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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * (Ring.inverse ↑k.1! * Ring.inverse ↑k.2!)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * (Ring.inverse ↑k.1! * Ring.inverse ↑k.2!)
Tactic:
rw [← mul_assoc]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add_dif_pos
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Tactic:
exact foo (factorial_isUnit' hn_fac (le_sub_one_of_lt hmn)) hk
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
by_cases hmn : m < 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : m < n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : m < n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
exact dpow_add_dif_pos hn_fac hmn hx hy
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
have h_sub : I ^ m ≤ I ^ n := Ideal.pow_le_pow_right (not_lt.mp hmn)
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
rw [dpow_eq_of_mem m (Ideal.add_mem I hx hy)]
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ Ring.inverse ↑m ! * (x + y) ^ m = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ Ring.inverse ↑m ! * (x + y) ^ m = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Tactic:
simp only [dpow]
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ Ring.inverse ↑m ! * (x + y) ^ m =
    ∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ Ring.inverse ↑m ! * (x + y) ^ m =
    ∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0
Tactic:
have hxy : (x + y) ^ m = 0 :=
  by
  rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
  apply Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ Ring.inverse ↑m ! * (x + y) ^ m =
    ∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ Ring.inverse ↑m ! * (x + y) ^ m =
    ∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0
Tactic:
rw [hxy, MulZeroClass.mul_zero, eq_comm]
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ (∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0) =
    0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ (∑ x_1 ∈ Finset.antidiagonal m,
      (if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0) =
    0
Tactic:
apply Finset.sum_eq_zero
Proof state after:
case neg.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ ∀ x_1 ∈ Finset.antidiagonal m,
    ((if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0) =
      0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ ∀ x_1 ∈ Finset.antidiagonal m,
    ((if x ∈ I then Ring.inverse ↑x_1.1! * x ^ x_1.1 else 0) * if y ∈ I then Ring.inverse ↑x_1.2! * y ^ x_1.2 else 0) =
      0
Tactic:
intro k hk
Proof state after:
case neg.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ((if x ∈ I then Ring.inverse ↑k.1! * x ^ k.1 else 0) * if y ∈ I then Ring.inverse ↑k.2! * y ^ k.2 else 0) = 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ((if x ∈ I then Ring.inverse ↑k.1! * x ^ k.1 else 0) * if y ∈ I then Ring.inverse ↑k.2! * y ^ k.2 else 0) = 0
Tactic:
rw [if_pos hx, if_pos hy, mul_assoc, mul_comm (x ^ k.1), mul_assoc, ← mul_assoc]
Proof state after:
case neg.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ Ring.inverse ↑k.1! * Ring.inverse ↑k.2! * (y ^ k.2 * x ^ k.1) = 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ Ring.inverse ↑k.1! * Ring.inverse ↑k.2! * (y ^ k.2 * x ^ k.1) = 0
Tactic:
apply mul_eq_zero_of_right
Proof state after:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 = 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 = 0
Tactic:
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
Proof state after:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ I ^ n
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ I ^ n
Tactic:
apply Set.mem_of_subset_of_mem h_sub
Proof state after:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ m)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ m)
Tactic:
rw [Finset.mem_antidiagonal] at hk
Proof state after:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k.1 + k.2 = m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ m)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k.1 + k.2 = m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ m)
Tactic:
rw [← hk, add_comm, pow_add]
Proof state after:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k.1 + k.2 = m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ k.2 * I ^ k.1)
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
case neg.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k.1 + k.2 = m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ k.2 * I ^ k.1)
Tactic:
exact Ideal.mul_mem_mul (Ideal.pow_mem_pow hy _) (Ideal.pow_mem_pow hx _)
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m = 0
Tactic:
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m ∈ I ^ n
Theorem: DividedPowers.OfInvertibleFactorial.dpow_add
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : ¬m < n
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m ∈ I ^ n
Tactic:
apply Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_smul
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
a x : A
hx : x ∈ I
⊢ dpow I m (a * x) = a ^ m * dpow I m x
Tactic:
rw [dpow_eq_of_mem m (Ideal.mul_mem_left I _ hx), dpow_eq_of_mem m hx,
  mul_pow, ← mul_assoc, mul_comm _ (a ^ m), mul_assoc]
Proof state after:
no goals