R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
⊢ (∀ (n : ℕ), coeff p n = coeff q n) ↔ ∀ (i : ℕ), i ≤ n → coeff p i = coeff q i
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
⊢ p = q ↔ ∀ (i : ℕ), i ≤ n → coeff p i = coeff q i
refine' Iff.trans Polynomial.ext_iff _
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
i : ℕ
h : i ≤ n → coeff p i = coeff q i
⊢ coeff p i = coeff q i
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
⊢ (∀ (n : ℕ), coeff p n = coeff q n) ↔ ∀ (i : ℕ), i ≤ n → coeff p i = coeff q i
refine' forall_congr' fun i => ⟨fun h _ => h, fun h => _⟩
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
i : ℕ
h : i ≤ n → coeff p i = coeff q i
k : n < i
⊢ coeff p i = coeff q i
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
i : ℕ
h : i ≤ n → coeff p i = coeff q i
⊢ coeff p i = coeff q i
refine' (le_or_lt i n).elim h fun k => _
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
i : ℕ
h : i ≤ n → coeff p i = coeff q i
k : n < i
⊢ coeff p i = coeff q i
refine'
  (coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans
    (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm