case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ ↑(WittVector.map g) (f x) = f (↑(WittVector.map g) x)
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hf : IsPoly p f
g : R →+* S
x : 𝕎 R
⊢ ↑(WittVector.map g) (f x) = f (↑(WittVector.map g) x)
obtain ⟨φ, hf⟩ := hf
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n : ℕ
⊢ coeff (↑(WittVector.map g) (f x)) n = coeff (f (↑(WittVector.map g) x)) n
case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ ↑(WittVector.map g) (f x) = f (↑(WittVector.map g) x)
ext n
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n : ℕ
⊢ ↑(eval₂Hom (RingHom.comp g (algebraMap ℤ R)) fun i => ↑g (coeff x i)) (φ n) =
    ↑(aeval (↑(WittVector.map g) x).coeff) (φ n)
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n : ℕ
⊢ coeff (↑(WittVector.map g) (f x)) n = coeff (f (↑(WittVector.map g) x)) n
simp only [map_coeff, hf, map_aeval]
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n : ℕ
⊢ (fun i => ↑g (coeff x i)) = (↑(WittVector.map g) x).coeff
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n : ℕ
⊢ ↑(eval₂Hom (RingHom.comp g (algebraMap ℤ R)) fun i => ↑g (coeff x i)) (φ n) =
    ↑(aeval (↑(WittVector.map g) x).coeff) (φ n)
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
case h
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n x✝ : ℕ
⊢ ↑g (coeff x x✝) = coeff (↑(WittVector.map g) x) x✝
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n : ℕ
⊢ (fun i => ↑g (coeff x i)) = (↑(WittVector.map g) x).coeff
ext
no goals
case h
p : ℕ
R S : Type u
σ : Type ?u.696707
idx : Type ?u.696710
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
n x✝ : ℕ
⊢ ↑g (coeff x x✝) = coeff (↑(WittVector.map g) x) x✝
simp only [map_coeff]