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

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ ((WittVector.map g) (f x y)).coeff n = (f ((WittVector.map g) x) ((WittVector.map g) y)).coeff n

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ ((WittVector.map g) (f x y)).coeff n = (f ((WittVector.map g) x) ((WittVector.map g) y)).coeff n

Tactic:
simp (config := { unfoldPartialApp := true }) only [map_coeff, hf, map_aeval, peval, uncurry]

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ (eval₂Hom (g.comp (algebraMap ℤ R)) fun i => g (![x.coeff, y.coeff] i.1 i.2)) (φ n) =
    (aeval fun a => ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2) (φ 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 → 𝕎 R
hf : IsPoly₂ p f
g : R →+* S
x y : 𝕎 R
⊢ (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ (eval₂Hom (g.comp (algebraMap ℤ R)) fun i => g (![x.coeff, y.coeff] i.1 i.2)) (φ n) =
    (aeval fun a => ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2) (φ 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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ (fun i => g (![x.coeff, y.coeff] i.1 i.2)) = fun a =>
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2

Proof state:
case h.mk
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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
i : Fin 2
k : ℕ
⊢ g (![x.coeff, y.coeff] (i, k).1 (i, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] (i, k).1 (i, k).2

Tactic:
fin_cases i <;> simp

Result:
no goals

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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ (fun i => g (![x.coeff, y.coeff] i.1 i.2)) = fun a =>
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2

Tactic:
ext ⟨i, k⟩

Result:
case h.mk
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 → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
n : ℕ
i : Fin 2
k : ℕ
⊢ g (![x.coeff, y.coeff] (i, k).1 (i, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] (i, k).1 (i, k).2