Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ (a + b) ^ (m + n).pred = 0
Tactic:
rw [add_pow]
State after:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∑ m_1 ∈ Finset.range ((m + n).pred + 1), a ^ m_1 * b ^ ((m + n).pred - m_1) * ↑((m + n).pred.choose m_1) = 0

State before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∑ m_1 ∈ Finset.range ((m + n).pred + 1), a ^ m_1 * b ^ ((m + n).pred - m_1) * ↑((m + n).pred.choose m_1) = 0
Tactic:
apply Finset.sum_eq_zero
State after:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∀ x ∈ Finset.range ((m + n).pred + 1), a ^ x * b ^ ((m + n).pred - x) * ↑((m + n).pred.choose x) = 0

State before:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∀ x ∈ Finset.range ((m + n).pred + 1), a ^ x * b ^ ((m + n).pred - x) * ↑((m + n).pred.choose x) = 0
Tactic:
intro k hk
State after:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k ∈ Finset.range ((m + n).pred + 1)
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

State before:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k ∈ Finset.range ((m + n).pred + 1)
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
simp only [Finset.mem_range] at hk
State after:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

State before:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
by_cases h : k < m
State after:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : ¬k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

State before:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
have : n ≤ (m + n).pred - k  := by
  rw [Nat.le_sub_iff_add_le (Nat.le_of_lt_succ hk), add_comm]
  rw [Nat.le_pred_iff_lt (lt_of_le_of_lt (zero_le k) (Nat.lt_add_right n h))]
  exact Nat.add_lt_add_right h n
State after:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

State before:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
rw [← Nat.add_sub_of_le this, pow_add, hb]
State after:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * (0 * b ^ ((m + n).pred - k - n)) * ↑((m + n).pred.choose k) = 0

State before:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * (0 * b ^ ((m + n).pred - k - n)) * ↑((m + n).pred.choose k) = 0
Tactic:
simp only [zero_mul, mul_zero]
State after:
no goals

State before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ n ≤ (m + n).pred - k
Tactic:
rw [Nat.le_sub_iff_add_le (Nat.le_of_lt_succ hk), add_comm]
State after:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n ≤ (m + n).pred

State before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n ≤ (m + n).pred
Tactic:
rw [Nat.le_pred_iff_lt (lt_of_le_of_lt (zero_le k) (Nat.lt_add_right n h))]
State after:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n < m + n

State before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n < m + n
Tactic:
exact Nat.add_lt_add_right h n
State after:
no goals

State before:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : ¬k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
simp only [not_lt] at h
State after:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

State before:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
rw [← Nat.add_sub_of_le h, pow_add, ha]
State after:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ 0 * a ^ (k - m) * b ^ ((m + n).pred - (m + (k - m))) * ↑((m + n).pred.choose (m + (k - m))) = 0

State before:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ 0 * a ^ (k - m) * b ^ ((m + n).pred - (m + (k - m))) * ↑((m + n).pred.choose (m + (k - m))) = 0
Tactic:
simp only [zero_mul]
State after:
no goals