case zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
⊢ coeff (p ^ Nat.zero) (Nat.zero * natDegree p) = leadingCoeff p ^ Nat.zero

case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
⊢ coeff (p ^ Nat.succ i) (Nat.succ i * natDegree p) = leadingCoeff p ^ Nat.succ i
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
n : ℕ
⊢ coeff (p ^ n) (n * natDegree p) = leadingCoeff p ^ n
induction' n with i hi
no goals
case zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
⊢ coeff (p ^ Nat.zero) (Nat.zero * natDegree p) = leadingCoeff p ^ Nat.zero
simp
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
⊢ coeff (p ^ Nat.succ i) (Nat.succ i * natDegree p) = leadingCoeff p ^ Nat.succ i
rw [pow_succ', pow_succ', Nat.succ_mul]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : ¬leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
by_cases hp1 : p.leadingCoeff ^ i = 0
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
rw [hp1, zero_mul]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
by_cases hp2 : p ^ i = 0
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
rw [hp2, zero_mul, coeff_zero]
case neg.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ natDegree (p ^ i * p) < i * natDegree p + natDegree p
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
apply coeff_eq_zero_of_natDegree_lt
case neg.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h1 : natDegree (p ^ i) < i * natDegree p
⊢ natDegree (p ^ i * p) < i * natDegree p + natDegree p
case neg.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ natDegree (p ^ i * p) < i * natDegree p + natDegree p
have h1 : (p ^ i).natDegree < i * p.natDegree := by
  refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
  rw [← h, hp1] at hi
  exact leadingCoeff_eq_zero.mp hi
no goals
case neg.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h1 : natDegree (p ^ i) < i * natDegree p
⊢ natDegree (p ^ i * p) < i * natDegree p + natDegree p
calc
  (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
  _ < i * p.natDegree + p.natDegree := add_lt_add_right h1 _
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h : natDegree (p ^ i) = i * natDegree p
⊢ p ^ i = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ natDegree (p ^ i) < i * natDegree p
refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (natDegree (p ^ i)) = 0
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h : natDegree (p ^ i) = i * natDegree p
⊢ p ^ i = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h : natDegree (p ^ i) = i * natDegree p
⊢ p ^ i = 0
rw [← h, hp1] at hi
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (natDegree (p ^ i)) = 0
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h : natDegree (p ^ i) = i * natDegree p
⊢ p ^ i = 0
exact leadingCoeff_eq_zero.mp hi
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : ¬leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (natDegree (p ^ i) + natDegree p) = leadingCoeff (p ^ i) * leadingCoeff p
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : ¬leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
no goals
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.697185
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : ¬leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (natDegree (p ^ i) + natDegree p) = leadingCoeff (p ^ i) * leadingCoeff p
exact coeff_mul_degree_add_degree _ _