-- Mathlib/RingTheory/WittVector/IsPoly.lean
theorem IsPoly.map [Fact p.Prime] {f} (hf : IsPoly p f) (g : R →+* S) (x : 𝕎 R) :
    map g (f x) = f (map g x)

Proof state:
case mk'.intro.h
p : ℕ
R S : Type u
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 : ℕ
⊢ ((WittVector.map g) (f x)).coeff n = (f ((WittVector.map g) x)).coeff n

Tactic:
simp only [map_coeff, hf, map_aeval]

Result:
case mk'.intro.h
p : ℕ
R S : Type u
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 (g.comp (algebraMap ℤ R)) fun i => g (x.coeff i)) (φ n) = (aeval ((WittVector.map g) x).coeff) (φ n)

Proof state:
case mk'.intro
p : ℕ
R S : Type u
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)

Tactic:
ext n

Result:
case mk'.intro.h
p : ℕ
R S : Type u
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 : ℕ
⊢ ((WittVector.map g) (f x)).coeff n = (f ((WittVector.map g) x)).coeff n

Proof state:
p : ℕ
R S : Type u
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)

Tactic:
obtain ⟨φ, hf⟩ := hf

Result:
case mk'.intro
p : ℕ
R S : Type u
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)

Proof state:
p : ℕ
R S : Type u
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 (x.coeff i)) = ((WittVector.map g) x).coeff

Tactic:
rfl

Result:
no goals

Proof state:
case mk'.intro.h
p : ℕ
R S : Type u
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 (g.comp (algebraMap ℤ R)) fun i => g (x.coeff i)) (φ n) = (aeval ((WittVector.map g) x).coeff) (φ n)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Result:
p : ℕ
R S : Type u
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 (x.coeff i)) = ((WittVector.map g) x).coeff