p : ℕ
R : Type ?u.65060
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)
p : ℕ
R : Type ?u.65060
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (↑(bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))
rw [bind₁_bind₁]
no goals
p : ℕ
R : Type ?u.65060
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)
exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl
no goals
p : ℕ
R : Type ?u.65060
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (↑(bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n)) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]