case pos
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f

case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
by_cases c : f = 0
no goals
case pos
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
rw [c, (finSuccEquiv R n).map_zero, Polynomial.natDegree_zero, degreeOf_zero]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ WithBot.unbot' 0 ↑(degreeOf 0 f) = degreeOf 0 f
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
rw [Polynomial.natDegree, degree_finSuccEquiv (by simpa only [Ne.def] )]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ↑(degreeOf 0 f) = degreeOf 0 f
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ WithBot.unbot' 0 ↑(degreeOf 0 f) = degreeOf 0 f
erw [WithBot.unbot'_coe]
no goals
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ↑(degreeOf 0 f) = degreeOf 0 f
simp
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1366622
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ f ≠ 0
simpa only [Ne.def]