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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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