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