no goals
p : ℕ
R : Type ?u.1881167
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ↑constantCoeff (wittStructureRat p Φ 0) = ↑constantCoeff Φ
simp only [wittStructureRat, bind₁, map_aeval, xInTermsOfW_zero, constantCoeff_rename,
  constantCoeff_wittPolynomial, aeval_X, constantCoeff_comp_algebraMap, eval₂Hom_zero'_apply,
  RingHom.id_apply]