[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ LeftInverse (Polynomial.eval₂ C (X PUnit.unit)) (eval₂ Polynomial.C fun x => Polynomial.X)
[PROOFSTEP]
let f : R[X] →+* MvPolynomial PUnit R := Polynomial.eval₂RingHom MvPolynomial.C (X PUnit.unit)
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
⊢ LeftInverse (Polynomial.eval₂ C (X PUnit.unit)) (eval₂ Polynomial.C fun x => Polynomial.X)
[PROOFSTEP]
let g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ LeftInverse (Polynomial.eval₂ C (X PUnit.unit)) (eval₂ Polynomial.C fun x => Polynomial.X)
[PROOFSTEP]
show ∀ p, f.comp g p = p
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ ∀ (p : MvPolynomial PUnit R), ↑(RingHom.comp f g) p = p
[PROOFSTEP]
apply is_id
[GOAL]
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ RingHom.comp (RingHom.comp f g) C = C
[PROOFSTEP]
ext a
[GOAL]
case hC.a.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
a : R
m✝ : PUnit →₀ ℕ
⊢ coeff m✝ (↑(RingHom.comp (RingHom.comp f g) C) a) = coeff m✝ (↑C a)
[PROOFSTEP]
dsimp
[GOAL]
case hC.a.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
a : R
m✝ : PUnit →₀ ℕ
⊢ coeff m✝ (Polynomial.eval₂ C (X PUnit.unit) (eval₂ Polynomial.C (fun x => Polynomial.X) (↑C a))) = coeff m✝ (↑C a)
[PROOFSTEP]
rw [eval₂_C, Polynomial.eval₂_C]
[GOAL]
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ ∀ (n : PUnit), ↑(RingHom.comp f g) (X n) = X n
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case hX.unit
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ ↑(RingHom.comp f g) (X PUnit.unit) = X PUnit.unit
[PROOFSTEP]
dsimp
[GOAL]
case hX.unit
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ Polynomial.eval₂ C (X PUnit.unit) (eval₂ Polynomial.C (fun x => Polynomial.X) (X PUnit.unit)) = X PUnit.unit
[PROOFSTEP]
rw [eval₂_X, Polynomial.eval₂_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (↑Polynomial.C a)) = ↑Polynomial.C a
[PROOFSTEP]
rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) p) = p
hq : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) q) = q
⊢ eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (p + q)) = p + q
[PROOFSTEP]
rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (↑Polynomial.C n * Polynomial.X ^ p)) =
    ↑Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x => Polynomial.X)
      (Polynomial.eval₂ C (X PUnit.unit) (↑Polynomial.C n * Polynomial.X ^ (p + 1))) =
    ↑Polynomial.C n * Polynomial.X ^ (p + 1)
[PROOFSTEP]
rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C, eval₂_mul, eval₂_C, eval₂_pow,
  eval₂_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : CommSemiring S₂
inst✝ : CommSemiring S₃
e : S₁ ≃+* S₂
f : S₂ ≃+* S₃
p : MvPolynomial σ S₁
⊢ ↑(RingEquiv.trans (mapEquiv σ e) (mapEquiv σ f)) p = ↑(mapEquiv σ (RingEquiv.trans e f)) p
[PROOFSTEP]
simp only [RingEquiv.coe_trans, comp_apply, mapEquiv_apply, RingEquiv.coe_ringHom_trans, map_map]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
⊢ AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f) = mapAlgEquiv σ (AlgEquiv.trans e f)
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f)) a✝) =
    coeff m✝ (↑(mapAlgEquiv σ (AlgEquiv.trans e f)) a✝)
[PROOFSTEP]
simp only [AlgEquiv.trans_apply, mapAlgEquiv_apply, map_map]
[GOAL]
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(map (RingHom.comp ↑f ↑e)) a✝) = coeff m✝ (↑(map ↑(AlgEquiv.trans e f)) a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
⊢ AlgHom.comp (aeval fun a => IsEmpty.elim he a) (Algebra.ofId R (MvPolynomial σ R)) = AlgHom.id R R
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
x✝ : R
⊢ ↑(AlgHom.comp (aeval fun a => IsEmpty.elim he a) (Algebra.ofId R (MvPolynomial σ R))) x✝ = ↑(AlgHom.id R R) x✝
[PROOFSTEP]
simp [Algebra.ofId_apply, algebraMap_eq]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
⊢ AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun a => IsEmpty.elim he a) = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext i m
[GOAL]
case hf.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (↑(AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun a => IsEmpty.elim he a)) (X i)) =
    coeff m (↑(AlgHom.id R (MvPolynomial σ R)) (X i))
[PROOFSTEP]
exact IsEmpty.elim' he i
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
[PROOFSTEP]
apply mvPolynomialEquivMvPolynomial R (Sum S₁ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
[GOAL]
case hfgC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C = C
[PROOFSTEP]
refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)
[GOAL]
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C = RingHom.comp C C
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C = RingHom.comp C C
[PROOFSTEP]
case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C = RingHom.comp C C
[PROOFSTEP]
ext1
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) x✝ = ↑(RingHom.comp C C) x✝
[PROOFSTEP]
simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
[GOAL]
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
intro
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : S₂
⊢ ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n✝) = ↑C (X n✝)
[PROOFSTEP]
simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
[GOAL]
case hfgX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₁), ↑(sumToIter R S₁ S₂) (↑(iterToSum R S₁ S₂) (X n)) = X n
[PROOFSTEP]
simp [iterToSum_X, sumToIter_Xl]
[GOAL]
case hgfC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C = C
[PROOFSTEP]
ext1
[GOAL]
case hgfC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) x✝ = ↑C x✝
[PROOFSTEP]
simp only [RingHom.comp_apply, sumToIter_C, iterToSum_C_C]
[GOAL]
case hgfX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₁ ⊕ S₂), ↑(iterToSum R S₁ S₂) (↑(sumToIter R S₁ S₂) (X n)) = X n
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case hgfX.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₁
⊢ ↑(iterToSum R S₁ S₂) (↑(sumToIter R S₁ S₂) (X (Sum.inl val✝))) = X (Sum.inl val✝)
[PROOFSTEP]
simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]
[GOAL]
case hgfX.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₂
⊢ ↑(iterToSum R S₁ S₂) (↑(sumToIter R S₁ S₂) (X (Sum.inr val✝))) = X (Sum.inr val✝)
[PROOFSTEP]
simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
⊢ ∀ (r : R),
    Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
      ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
intro r
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
    ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) : _) := by rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
⊢ ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
A : ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
    ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
have B : algebraMap R (MvPolynomial (Sum S₁ S₂) R) r = C r := by rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
A : ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
⊢ ↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r = ↑C r
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
A : ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
B : ↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r = ↑C r
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
    ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe_apply, Equiv.coe_fn_mk, B, sumToIter_C, A]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s))
      (Polynomial.aevalTower (rename Option.some) (X none)) =
    AlgHom.id R (MvPolynomial S₁ R)[X]
[PROOFSTEP]
ext : 2
[GOAL]
case h₁.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
⊢ ↑(AlgHom.comp
          (AlgHom.comp (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s))
            (Polynomial.aevalTower (rename Option.some) (X none)))
          (IsScalarTower.toAlgHom R (MvPolynomial S₁ R) (MvPolynomial S₁ R)[X]))
      (X i✝) =
    ↑(AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R)[X])
          (IsScalarTower.toAlgHom R (MvPolynomial S₁ R) (MvPolynomial S₁ R)[X]))
      (X i✝)
[PROOFSTEP]
simp [← Polynomial.C_eq_algebraMap]
[GOAL]
case h₂.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : ℕ
⊢ Polynomial.coeff
      (↑(AlgHom.comp (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s))
            (Polynomial.aevalTower (rename Option.some) (X none)))
        Polynomial.X)
      n✝ =
    Polynomial.coeff (↑(AlgHom.id R (MvPolynomial S₁ R)[X]) Polynomial.X) n✝
[PROOFSTEP]
simp [← Polynomial.C_eq_algebraMap]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
      (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)) =
    AlgHom.id R (MvPolynomial (Option S₁) R)
[PROOFSTEP]
ext i : 2
[GOAL]
case hf.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)))
        (X i)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))
[PROOFSTEP]
cases i
[GOAL]
case hf.a.none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)))
        (X none)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))
[PROOFSTEP]
simp
[GOAL]
case hf.a.some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
val✝ : S₁
⊢ coeff m✝
      (↑(AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)))
        (X (Option.some val✝))) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (aeval fun o => Option.elim o (↑C Polynomial.X) X)
      (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)) =
    AlgHom.id R (MvPolynomial S₁ R[X])
[PROOFSTEP]
ext : 2
[GOAL]
case h₁.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ↑(AlgHom.comp
          (AlgHom.comp (aeval fun o => Option.elim o (↑C Polynomial.X) X)
            (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)))
          (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X =
    ↑(AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R[X])) (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X
[PROOFSTEP]
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp, IsScalarTower.coe_toAlgHom',
  comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X, Option.elim', aevalTower_X, AlgHom.coe_id, id.def,
  eq_self_iff_true, imp_true_iff]
[GOAL]
case h₂.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (aeval fun o => Option.elim o (↑C Polynomial.X) X)
            (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)))
        (X i✝)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial S₁ R[X])) (X i✝))
[PROOFSTEP]
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp, IsScalarTower.coe_toAlgHom',
  comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X, Option.elim', aevalTower_X, AlgHom.coe_id, id.def,
  eq_self_iff_true, imp_true_iff]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
      (aeval fun o => Option.elim o (↑C Polynomial.X) X) =
    AlgHom.id R (MvPolynomial (Option S₁) R)
[PROOFSTEP]
ext ⟨i⟩ : 2
[GOAL]
case hf.none.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
            (aeval fun o => Option.elim o (↑C Polynomial.X) X))
        (X none)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))
[PROOFSTEP]
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C, Polynomial.aeval_X, AlgHom.coe_id, id.def,
  aevalTower_X]
[GOAL]
case hf.some.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
            (aeval fun o => Option.elim o (↑C Polynomial.X) X))
        (X (Option.some val✝))) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))
[PROOFSTEP]
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C, Polynomial.aeval_X, AlgHom.coe_id, id.def,
  aevalTower_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) =
    eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i
[PROOFSTEP]
ext i : 2
[GOAL]
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ↑(RingHom.comp (↑(finSuccEquiv R n)) C) i =
    ↑(RingHom.comp
          (eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) C)
      i
[PROOFSTEP]
simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe, coe_eval₂Hom, comp_apply,
  renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]
[GOAL]
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ↑(algebraMap R (MvPolynomial (Fin n) R)[X]) i = ↑Polynomial.C (↑C i)
[PROOFSTEP]
rfl
[GOAL]
case hX.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ Polynomial.coeff (↑↑(finSuccEquiv R n) (X i)) n✝ =
    Polynomial.coeff
      (↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) (X i))
      n✝
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case hX.a.refine'_1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ Polynomial.coeff (↑↑(finSuccEquiv R n) (X 0)) n✝ =
    Polynomial.coeff
      (↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) (X 0))
      n✝
[PROOFSTEP]
simp [finSuccEquiv]
[GOAL]
case hX.a.refine'_2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ ∀ (i : Fin n),
    Polynomial.coeff (↑↑(finSuccEquiv R n) (X (Fin.succ i))) n✝ =
      Polynomial.coeff
        (↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i)
          (X (Fin.succ i)))
        n✝
[PROOFSTEP]
simp [finSuccEquiv]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
⊢ ↑(finSuccEquiv R n) p =
    ↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) p
[PROOFSTEP]
rw [← finSuccEquiv_eq, RingHom.coe_coe]
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C) = C
[PROOFSTEP]
refine' RingHom.ext fun x => _
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C)) x = ↑C x
[PROOFSTEP]
rw [RingHom.comp_apply]
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑↑(AlgEquiv.symm (finSuccEquiv R n)) (↑(RingHom.comp Polynomial.C C) x) = ↑C x
[PROOFSTEP]
refine' (MvPolynomial.finSuccEquiv R n).injective (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) _)
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp Polynomial.C C) x = ↑(finSuccEquiv R n) (↑C x)
[PROOFSTEP]
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) (X 0) = Polynomial.X
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ ↑(finSuccEquiv R n) (X (Fin.succ j)) = ↑Polynomial.C (X j)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) f) i) = coeff (cons i m) f
[PROOFSTEP]
induction' f using MvPolynomial.induction_on' with j r p q hp hq generalizing i m
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
[PROOFSTEP]
swap
[GOAL]
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
[PROOFSTEP]
simp only [(finSuccEquiv R n).map_add, Polynomial.coeff_add, coeff_add, hp, hq]
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)
[PROOFSTEP]
simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, prod_pow, Polynomial.coeff_C_mul,
  coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero, Fin.cases_succ, ← map_prod, ← RingHom.map_pow,
  Function.comp_apply]
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (Polynomial.coeff (Polynomial.X ^ ↑j 0 * ↑Polynomial.C (∏ x : Fin n, X x ^ ↑j (Fin.succ x))) i) =
    if j = cons i m then r else 0
[PROOFSTEP]
rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = r * if j = cons i m then 1 else 0
[PROOFSTEP]
congr 1
[GOAL]
case h1.e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = if j = cons i m then 1 else 0
[PROOFSTEP]
obtain rfl | hjmi := eq_or_ne j (m.cons i)
[GOAL]
case h1.e_a.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑(cons i m) 0 then ∏ x : Fin n, X x ^ ↑(cons i m) (Fin.succ x) else 0) =
    if cons i m = cons i m then 1 else 0
[PROOFSTEP]
simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul, prod_pow] using coeff_monomial m m (1 : R)
[GOAL]
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = if j = cons i m then 1 else 0
[PROOFSTEP]
simp only [hjmi, if_false]
[GOAL]
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = 0
[PROOFSTEP]
obtain hij | rfl := ne_or_eq i (j 0)
[GOAL]
case h1.e_a.inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
hij : i ≠ ↑j 0
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = 0
[PROOFSTEP]
simp only [hij, if_false, coeff_zero]
[GOAL]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ coeff m (if ↑j 0 = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = 0
[PROOFSTEP]
simp only [eq_self_iff_true, if_true]
[GOAL]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
[PROOFSTEP]
have hmj : m ≠ j.tail := by
  rintro rfl
  rw [cons_tail] at hjmi 
  contradiction
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ m ≠ tail j
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (↑j 0) (tail j)
⊢ False
[PROOFSTEP]
rw [cons_tail] at hjmi 
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
hmj : m ≠ tail j
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
[PROOFSTEP]
simpa only [monomial_eq, C_1, one_mul, prod_pow, Finsupp.tail_apply, if_neg hmj.symm] using
  coeff_monomial m j.tail (1 : R)
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
⊢ ↑(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) (↑(finSuccEquiv R n) f))
[PROOFSTEP]
let φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  { Polynomial.mapRingHom (eval s) with
    commutes' := fun r => by
      convert Polynomial.map_C (eval s)
      exact (eval_C _).symm }
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                  OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
    ↑(algebraMap R R[X]) r
[PROOFSTEP]
convert Polynomial.map_C (eval s)
[GOAL]
case h.e'_3.h.e'_6
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ r = ↑(eval s) (↑(algebraMap R (MvPolynomial (Fin n) R)) r)
[PROOFSTEP]
exact (eval_C _).symm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) (↑(finSuccEquiv R n) f))
[PROOFSTEP]
show aeval (Fin.cons y s : Fin (n + 1) → R) f = (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) f = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) f
[PROOFSTEP]
congr 2
[GOAL]
case e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ aeval (Fin.cons y s) = AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))
[PROOFSTEP]
apply MvPolynomial.algHom_ext
[GOAL]
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ∀ (i : Fin (n + 1)),
    ↑(aeval (Fin.cons y s)) (X i) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X i)
[PROOFSTEP]
rw [Fin.forall_fin_succ]
[GOAL]
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) (X 0) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      ↑(aeval (Fin.cons y s)) (X (Fin.succ i)) =
        ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X (Fin.succ i))
[PROOFSTEP]
simp only [aeval_X, Fin.cons_zero, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
  Polynomial.map_C, AlgHom.coe_mk, RingHom.toFun_eq_coe, Polynomial.coe_mapRingHom, comp_apply, finSuccEquiv_apply,
  eval₂Hom_X', Fin.cases_zero, Polynomial.map_X, Polynomial.eval_X, Fin.cons_succ, Fin.cases_succ, eval_X,
  Polynomial.eval_C, RingHom.coe_mk, MonoidHom.coe_coe, AlgHom.coe_coe, implies_true, and_self,
  RingHom.toMonoidHom_eq_coe]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s' : Fin n → R
f : (MvPolynomial (Fin n) R)[X]
i : ℕ
⊢ Polynomial.coeff (Polynomial.map (eval s') f) i = ↑(eval s') (Polynomial.coeff f i)
[PROOFSTEP]
simp only [Polynomial.coeff_map]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ↔ cons i m ∈ support f
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) → cons i m ∈ support f
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
⊢ cons i m ∈ support f
[PROOFSTEP]
simpa [← finSuccEquiv_coeff_coeff] using h
[GOAL]
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ support f → m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ support f
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
[PROOFSTEP]
simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ Polynomial.support (↑(finSuccEquiv R n) f) = Finset.image (fun m => ↑m 0) (support f)
[PROOFSTEP]
ext i
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ Polynomial.support (↑(finSuccEquiv R n) f) ↔ i ∈ Finset.image (fun m => ↑m 0) (support f)
[PROOFSTEP]
rw [Polynomial.mem_support_iff, Finset.mem_image, nonzero_iff_exists]
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) ↔ ∃ a, a ∈ support f ∧ ↑a 0 = i
[PROOFSTEP]
constructor
[GOAL]
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) → ∃ a, a ∈ support f ∧ ↑a 0 = i
[PROOFSTEP]
rintro ⟨m, hm⟩
[GOAL]
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ ∃ a, a ∈ support f ∧ ↑a 0 = i
[PROOFSTEP]
refine' ⟨cons i m, _, cons_zero _ _⟩
[GOAL]
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ cons i m ∈ support f
[PROOFSTEP]
rw [← support_coeff_finSuccEquiv]
[GOAL]
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
[PROOFSTEP]
simpa using hm
[GOAL]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, a ∈ support f ∧ ↑a 0 = i) → ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0
[PROOFSTEP]
rintro ⟨m, h, rfl⟩
[GOAL]
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) a ≠ 0
[PROOFSTEP]
refine' ⟨tail m, _⟩
[GOAL]
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) (tail m) ≠ 0
[PROOFSTEP]
rwa [← coeff, ← mem_support_iff, support_coeff_finSuccEquiv, cons_tail]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ Finset.image (cons i) (support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)) =
    Finset.filter (fun m => ↑m 0 = i) (support f)
[PROOFSTEP]
ext m
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ m ∈ Finset.image (cons i) (support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)) ↔
    m ∈ Finset.filter (fun m => ↑m 0 = i) (support f)
[PROOFSTEP]
rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m) ↔ coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
conv_lhs =>
  congr
  ext
  rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
  congr
  ext
  rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
  congr
  ext
  rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
congr
[GOAL]
case p
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| fun a => a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
ext
[GOAL]
case p.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| x✝ ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i x✝ = m
[PROOFSTEP]
rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
constructor
[GOAL]
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
rintro ⟨m', ⟨h, hm'⟩⟩
[GOAL]
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
simp only [← hm']
[GOAL]
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff (cons i m') f ≠ 0 ∧ ↑(cons i m') 0 = i
[PROOFSTEP]
exact ⟨h, by rw [cons_zero]⟩
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ ↑(cons i m') 0 = i
[PROOFSTEP]
rw [cons_zero]
[GOAL]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
[PROOFSTEP]
intro h
[GOAL]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
[PROOFSTEP]
use tail m
[GOAL]
case h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff (cons i (tail m)) f = 0 ∧ cons i (tail m) = m
[PROOFSTEP]
rw [← h.2, cons_tail]
[GOAL]
case h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff m f = 0 ∧ m = m
[PROOFSTEP]
simp [h.1]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ Finset.Nonempty (Polynomial.support (↑(finSuccEquiv R n) f))
[PROOFSTEP]
simp only [Finset.nonempty_iff_ne_empty, Ne, Polynomial.support_eq_empty]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ¬↑(finSuccEquiv R n) f = 0
[PROOFSTEP]
refine fun c => h ?_
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
⊢ f = 0
[PROOFSTEP]
let ii := (finSuccEquiv R n).symm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = 0
[PROOFSTEP]
calc
  f = ii (finSuccEquiv R n f) := by simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
  _ = ii 0 := by rw [c]
  _ = 0 := by simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = ↑ii (↑(finSuccEquiv R n) f)
[PROOFSTEP]
simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ ↑ii (↑(finSuccEquiv R n) f) = ↑ii 0
[PROOFSTEP]
rw [c]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ ↑ii 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h₂ : WithBot.some = Nat.cast := rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
h₂ : WithBot.some = Nat.cast
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
  rw [degreeOf_eq_sup, finSuccEquiv_support f, Finset.sup_image, h₀]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
h₂ : WithBot.some = Nat.cast
⊢ (Finset.sup (Polynomial.support (↑(finSuccEquiv R n) f)) fun x => x) = degreeOf 0 f
[PROOFSTEP]
rw [degreeOf_eq_sup, finSuccEquiv_support f, Finset.sup_image, h₀]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
h₂ : WithBot.some = Nat.cast
h' : (Finset.sup (Polynomial.support (↑(finSuccEquiv R n) f)) fun x => x) = degreeOf 0 f
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
rw [Polynomial.degree, ← h', ← h₂, Finset.coe_sup_of_nonempty (support_finSuccEquiv_nonempty h), Finset.max_eq_sup_coe,
  h₁]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
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
[PROOFSTEP]
by_cases c : f = 0
[GOAL]
case pos
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
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
[PROOFSTEP]
rw [c, (finSuccEquiv R n).map_zero, Polynomial.natDegree_zero, degreeOf_zero]
[GOAL]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
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
[PROOFSTEP]
rw [Polynomial.natDegree, degree_finSuccEquiv (by simpa only [Ne.def])]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ f ≠ 0
[PROOFSTEP]
simpa only [Ne.def]
[GOAL]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
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
[PROOFSTEP]
erw [WithBot.unbot'_coe]
[GOAL]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
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
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf j (Polynomial.coeff (↑(finSuccEquiv R n) p) i) ≤ degreeOf (Fin.succ j) p
[PROOFSTEP]
rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ (b : Fin n →₀ ℕ),
    b ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i) → ↑b j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑m j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
[PROOFSTEP]
rw [← Finsupp.cons_succ j i m]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑(cons i m) (Fin.succ j) ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
[PROOFSTEP]
exact Finset.le_sup (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j)) (support_coeff_finSuccEquiv.1 hm)
