p : ℕ
R : Type u_2
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i =>
    ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)

p : ℕ
R : Type u_2
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(rename (Prod.mk i)) (W_ R n)) = fun i => ↑(map (Int.castRingHom R)) (↑(rename (Prod.mk i)) (W_ ℤ n))
p : ℕ
R : Type u_2
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ
convert congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1 <;>
    rw [hom_bind₁] <;>
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
no goals
p : ℕ
R : Type u_2
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i =>
    ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)
rfl
no goals
p : ℕ
R : Type u_2
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(rename (Prod.mk i)) (W_ R n)) = fun i => ↑(map (Int.castRingHom R)) (↑(rename (Prod.mk i)) (W_ ℤ n))
simp only [map_rename, map_wittPolynomial]