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

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)]
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

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]
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

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 _ _)]
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)

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
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)

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
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)

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]
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))

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
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!

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]
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!)))

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
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!))

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
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!)

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]
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!

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
State after:
no goals