case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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

case hX.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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✝
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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
ext i : 2
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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)
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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
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]
no goals
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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)
rfl
no goals
case hX.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.833445
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✝
refine' Fin.cases _ _ i <;> simp [finSuccEquiv]