case a
p : ℕ
R : Type ?u.1846181
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_1
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p (↑(rename f) Φ) n) =
    ↑(map (Int.castRingHom ℚ)) (↑(rename (Prod.map f id)) (wittStructureInt p Φ n))
p : ℕ
R : Type ?u.1846181
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_1
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ wittStructureInt p (↑(rename f) Φ) n = ↑(rename (Prod.map f id)) (wittStructureInt p Φ n)
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
case a
p : ℕ
R : Type ?u.1846181
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_1
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ ((fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    ↑(bind₁ fun i =>
          ↑(bind₁ fun i_1 => ↑(rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)
case a
p : ℕ
R : Type ?u.1846181
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_1
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p (↑(rename f) Φ) n) =
    ↑(map (Int.castRingHom ℚ)) (↑(rename (Prod.map f id)) (wittStructureInt p Φ n))
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename,
  bind₁_rename]
no goals
case a
p : ℕ
R : Type ?u.1846181
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_1
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ ((fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    ↑(bind₁ fun i =>
          ↑(bind₁ fun i_1 => ↑(rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)
rfl