[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ f) (wittPolynomial p ℤ n) = ↑(bind₁ g) (wittPolynomial p ℤ n)
⊢ f = g
[PROOFSTEP]
ext1 n
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ f) (wittPolynomial p ℤ n) = ↑(bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ f n = g n
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ f) (wittPolynomial p ℤ n) = ↑(bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = ↑(MvPolynomial.map (Int.castRingHom ℚ)) (g n)
[PROOFSTEP]
rw [← Function.funext_iff] at h
[GOAL]
case h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : (fun n => ↑(bind₁ f) (wittPolynomial p ℤ n)) = fun n => ↑(bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = ↑(MvPolynomial.map (Int.castRingHom ℚ)) (g n)
[PROOFSTEP]
replace h := congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
[GOAL]
case h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  ((fun fam => ↑(bind₁ (↑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      ↑(bind₁ f) (wittPolynomial p ℤ n)) =
    (fun fam => ↑(bind₁ (↑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      ↑(bind₁ g) (wittPolynomial p ℤ n)
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = ↑(MvPolynomial.map (Int.castRingHom ℚ)) (g n)
[PROOFSTEP]
simpa only [Function.comp, map_bind₁, map_wittPolynomial, ← bind₁_bind₁, bind₁_wittPolynomial_xInTermsOfW,
  bind₁_X_right] using h
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), ↑(bind₁ f) (wittPolynomial p ℤ n) = ↑(bind₁ g) (wittPolynomial p ℤ n)
⊢ f = g
[PROOFSTEP]
ext1 n
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), ↑(bind₁ f) (wittPolynomial p ℤ n) = ↑(bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ f n = g n
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), ↑(bind₁ f) (wittPolynomial p ℤ n) = ↑(bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = ↑(MvPolynomial.map (Int.castRingHom ℚ)) (g n)
[PROOFSTEP]
rw [← Function.funext_iff] at h
[GOAL]
case h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : (fun n => ↑(bind₁ f) (wittPolynomial p ℤ n)) = fun n => ↑(bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = ↑(MvPolynomial.map (Int.castRingHom ℚ)) (g n)
[PROOFSTEP]
replace h := congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
[GOAL]
case h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
n : ℕ
h :
  ((fun fam => ↑(bind₁ (↑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      ↑(bind₁ f) (wittPolynomial p ℤ n)) =
    (fun fam => ↑(bind₁ (↑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      ↑(bind₁ g) (wittPolynomial p ℤ n)
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = ↑(MvPolynomial.map (Int.castRingHom ℚ)) (g n)
[PROOFSTEP]
simpa only [Function.comp, map_bind₁, map_wittPolynomial, ← bind₁_bind₁, bind₁_wittPolynomial_xInTermsOfW,
  bind₁_X_right] using h
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ ⦃R : Type ?u.179228⦄ [inst : CommRing R] (x : 𝕎 R), (id x).coeff = fun n => ↑(aeval x.coeff) (X n)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
R✝ : Type ?u.179228
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (id x✝).coeff = fun n => ↑(aeval x✝.coeff) (X n)
[PROOFSTEP]
simp only [aeval_X, id]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hf : IsPoly p f
hg : IsPoly p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
[PROOFSTEP]
obtain ⟨ψ, hg⟩ := hg
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
[PROOFSTEP]
intros
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ f x✝ = g x✝
[PROOFSTEP]
ext n
[GOAL]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (f x✝) n = coeff (g x✝) n
[PROOFSTEP]
rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq p φ ψ]
[GOAL]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ ∀ (n : ℕ), ↑(bind₁ φ) (wittPolynomial p ℤ n) = ↑(bind₁ ψ) (wittPolynomial p ℤ n)
[PROOFSTEP]
intro k
[GOAL]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ ↑(bind₁ φ) (wittPolynomial p ℤ k) = ↑(bind₁ ψ) (wittPolynomial p ℤ k)
[PROOFSTEP]
apply MvPolynomial.funext
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ ∀ (x : ℕ → ℤ),
    ↑(MvPolynomial.eval x) (↑(bind₁ φ) (wittPolynomial p ℤ k)) =
      ↑(MvPolynomial.eval x) (↑(bind₁ ψ) (wittPolynomial p ℤ k))
[PROOFSTEP]
intro x
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ φ) (wittPolynomial p ℤ k)) =
    ↑(MvPolynomial.eval x) (↑(bind₁ ψ) (wittPolynomial p ℤ k))
[PROOFSTEP]
simp only [hom_bind₁]
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x) = ↑(ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
[PROOFSTEP]
specialize h (ULift ℤ) (mk p fun i => ⟨x i⟩) k
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h : ↑(ghostComponent k) (f (mk p fun i => { down := x i })) = ↑(ghostComponent k) (g (mk p fun i => { down := x i }))
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
[PROOFSTEP]
simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
[PROOFSTEP]
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
[GOAL]
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(RingEquiv.symm ULift.ringEquiv)
      (↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i))
        (wittPolynomial p ℤ k)) =
    ↑(RingEquiv.symm ULift.ringEquiv)
      (↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k))
[PROOFSTEP]
simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
[GOAL]
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k)
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_2
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
case h.e'_3
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
[PROOFSTEP]
all_goals
  --  porting note: this proof started with `funext i`
  simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
  ext1
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
  simp only [coeff_mk]; rfl
[GOAL]
case h.e'_2
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
[PROOFSTEP]
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
[GOAL]
case h.e'_2
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (eval₂Hom (RingHom.id ℤ) x) C)) fun i =>
          ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
                ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
            (φ i))
      (wittPolynomial p ℤ k) =
    ↑(aeval fun n => ↑(aeval (mk p fun i => { down := x i }).coeff) (φ n)) (wittPolynomial p ℤ k)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (fun i =>
      ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
            ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
        (φ i)) =
    fun n => ↑(aeval (mk p fun i => { down := x i }).coeff) (φ n)
[PROOFSTEP]
ext1
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
      (φ x✝) =
    ↑(aeval (mk p fun i => { down := x i }).coeff) (φ x✝)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ (fun i => ↑↑(RingEquiv.symm ULift.ringEquiv) (x i)) = (mk p fun i => { down := x i }).coeff
[PROOFSTEP]
simp only [coeff_mk]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ (fun i => ↑↑(RingEquiv.symm ULift.ringEquiv) (x i)) = fun i => { down := x i }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
[PROOFSTEP]
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
[GOAL]
case h.e'_3
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (eval₂Hom (RingHom.id ℤ) x) C)) fun i =>
          ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
                ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
            (ψ i))
      (wittPolynomial p ℤ k) =
    ↑(aeval fun n => ↑(aeval (mk p fun i => { down := x i }).coeff) (ψ n)) (wittPolynomial p ℤ k)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (fun i =>
      ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
            ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
        (ψ i)) =
    fun n => ↑(aeval (mk p fun i => { down := x i }).coeff) (ψ n)
[PROOFSTEP]
ext1
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
      (ψ x✝) =
    ↑(aeval (mk p fun i => { down := x i }).coeff) (ψ x✝)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ (fun i => ↑↑(RingEquiv.symm ULift.ringEquiv) (x i)) = (mk p fun i => { down := x i }).coeff
[PROOFSTEP]
simp only [coeff_mk]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ (fun i => ↑↑(RingEquiv.symm ULift.ringEquiv) (x i)) = fun i => { down := x i }
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type ?u.543600⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly p f
⊢ IsPoly p fun R _Rcr => g ∘ f
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type ?u.543600⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ IsPoly p fun R _Rcr => g ∘ f
[PROOFSTEP]
obtain ⟨ψ, hg⟩ := hg
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type ?u.543600⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ IsPoly p fun R _Rcr => g ∘ f
[PROOFSTEP]
use fun n => bind₁ φ (ψ n)
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type ?u.543600⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), ((g ∘ f) x).coeff = fun n => ↑(aeval x.coeff) (↑(bind₁ φ) (ψ n))
[PROOFSTEP]
intros
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
g f : ⦃R : Type ?u.543600⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.543600⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type ?u.543600
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ ((g ∘ f) x✝).coeff = fun n => ↑(aeval x✝.coeff) (↑(bind₁ φ) (ψ n))
[PROOFSTEP]
simp only [aeval_bind₁, Function.comp, hg, hf]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
hf : IsPoly p f
hg : IsPoly p g
⊢ IsPoly₂ p fun R _Rcr x y => h (f x) (g y)
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ IsPoly₂ p fun R _Rcr x y => h (f x) (g y)
[PROOFSTEP]
obtain ⟨ψ, hg⟩ := hg
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ IsPoly₂ p fun R _Rcr x y => h (f x) (g y)
[PROOFSTEP]
obtain ⟨χ, hh⟩ := hh
[GOAL]
case mk'.intro.mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun R _Rcr x y => h (f x) (g y)
[PROOFSTEP]
refine'
  ⟨⟨fun n ↦
      bind₁ (uncurry <| ![fun k ↦ rename (Prod.mk (0 : Fin 2)) (φ k), fun k ↦ rename (Prod.mk (1 : Fin 2)) (ψ k)])
        (χ n),
      _⟩⟩
[GOAL]
case mk'.intro.mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
⊢ ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R),
    (h (f x) (g y)).coeff = fun n =>
      peval
        ((fun n =>
            ↑(bind₁ (uncurry ![fun k => ↑(rename (Prod.mk 0)) (φ k), fun k => ↑(rename (Prod.mk 1)) (ψ k)])) (χ n))
          n)
        ![x.coeff, y.coeff]
[PROOFSTEP]
intros
[GOAL]
case mk'.intro.mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (h (f x✝) (g y✝)).coeff = fun n =>
    peval
      ((fun n => ↑(bind₁ (uncurry ![fun k => ↑(rename (Prod.mk 0)) (φ k), fun k => ↑(rename (Prod.mk 1)) (ψ k)])) (χ n))
        n)
      ![x✝.coeff, y✝.coeff]
[PROOFSTEP]
funext n
[GOAL]
case mk'.intro.mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ coeff (h (f x✝) (g y✝)) n =
    peval
      ((fun n => ↑(bind₁ (uncurry ![fun k => ↑(rename (Prod.mk 0)) (φ k), fun k => ↑(rename (Prod.mk 1)) (ψ k)])) (χ n))
        n)
      ![x✝.coeff, y✝.coeff]
[PROOFSTEP]
simp only [peval, aeval_bind₁, Function.comp, hh, hf, hg, uncurry]
[GOAL]
case mk'.intro.mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ ↑(aeval fun a => Matrix.vecCons (fun n => ↑(aeval x✝.coeff) (φ n)) ![fun n => ↑(aeval y✝.coeff) (ψ n)] a.fst a.snd)
      (χ n) =
    ↑(aeval fun i =>
          ↑(aeval fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
            (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)] i.fst i.snd))
      (χ n)
[PROOFSTEP]
apply eval₂Hom_congr rfl _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ (fun a => Matrix.vecCons (fun n => ↑(aeval x✝.coeff) (φ n)) ![fun n => ↑(aeval y✝.coeff) (ψ n)] a.fst a.snd) =
    fun i =>
    ↑(aeval fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)] i.fst i.snd)
[PROOFSTEP]
ext ⟨i, n⟩
[GOAL]
case h.mk
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ : ℕ
i : Fin 2
n : ℕ
⊢ Matrix.vecCons (fun n => ↑(aeval x✝.coeff) (φ n)) ![fun n => ↑(aeval y✝.coeff) (ψ n)] (i, n).fst (i, n).snd =
    ↑(aeval fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)] (i, n).fst
        (i, n).snd)
[PROOFSTEP]
fin_cases i
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ Matrix.vecCons (fun n => ↑(aeval x✝.coeff) (φ n)) ![fun n => ↑(aeval y✝.coeff) (ψ n)]
      ({ val := 0, isLt := (_ : 0 < 2) }, n).fst ({ val := 0, isLt := (_ : 0 < 2) }, n).snd =
    ↑(aeval fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)]
        ({ val := 0, isLt := (_ : 0 < 2) }, n).fst ({ val := 0, isLt := (_ : 0 < 2) }, n).snd)
[PROOFSTEP]
simp only [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp, Matrix.cons_val_zero, Matrix.head_cons,
  Matrix.cons_val_one]
  -- porting note: added the rest of the proof.
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ Matrix.vecCons (fun n => ↑(aeval x✝.coeff) (φ n)) ![fun n => ↑(aeval y✝.coeff) (ψ n)]
      ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, n).fst ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, n).snd =
    ↑(aeval fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)]
        ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, n).fst ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, n).snd)
[PROOFSTEP]
simp only [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp, Matrix.cons_val_zero, Matrix.head_cons,
  Matrix.cons_val_one]
  -- porting note: added the rest of the proof.
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ Matrix.vecCons (fun n => ↑(eval₂Hom (algebraMap ℤ R✝) x✝.coeff) (φ n))
      ![fun n => ↑(eval₂Hom (algebraMap ℤ R✝) y✝.coeff) (ψ n)] { val := 0, isLt := (_ : 0 < 2) } n =
    ↑(eval₂Hom (algebraMap ℤ R✝) fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)]
        { val := 0, isLt := (_ : 0 < 2) } n)
[PROOFSTEP]
open Matrix in
  simp only [algebraMap_int_eq, coe_eval₂Hom, Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one,
    cons_val_zero, cons_val_one, eval₂Hom_rename, Function.comp, head_fin_const]
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ Matrix.vecCons (fun n => ↑(eval₂Hom (algebraMap ℤ R✝) x✝.coeff) (φ n))
      ![fun n => ↑(eval₂Hom (algebraMap ℤ R✝) y✝.coeff) (ψ n)] { val := 0, isLt := (_ : 0 < 2) } n =
    ↑(eval₂Hom (algebraMap ℤ R✝) fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)]
        { val := 0, isLt := (_ : 0 < 2) } n)
[PROOFSTEP]
simp only [algebraMap_int_eq, coe_eval₂Hom, Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one,
  cons_val_zero, cons_val_one, eval₂Hom_rename, Function.comp, head_fin_const]
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ Matrix.vecCons (fun n => ↑(eval₂Hom (algebraMap ℤ R✝) x✝.coeff) (φ n))
      ![fun n => ↑(eval₂Hom (algebraMap ℤ R✝) y✝.coeff) (ψ n)] { val := 1, isLt := (_ : (fun a => a < 2) 1) } n =
    ↑(eval₂Hom (algebraMap ℤ R✝) fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)]
        { val := 1, isLt := (_ : (fun a => a < 2) 1) } n)
[PROOFSTEP]
open Matrix in
  simp only [algebraMap_int_eq, coe_eval₂Hom, Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one,
    cons_val_zero, cons_val_one, eval₂Hom_rename, Function.comp, head_fin_const]
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type ?u.560828⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type ?u.560828⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n => peval (χ n) ![x.coeff, y.coeff]
R✝ : Type ?u.560828
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ Matrix.vecCons (fun n => ↑(eval₂Hom (algebraMap ℤ R✝) x✝.coeff) (φ n))
      ![fun n => ↑(eval₂Hom (algebraMap ℤ R✝) y✝.coeff) (ψ n)] { val := 1, isLt := (_ : (fun a => a < 2) 1) } n =
    ↑(eval₂Hom (algebraMap ℤ R✝) fun a => Matrix.vecCons x✝.coeff ![y✝.coeff] a.fst a.snd)
      (Matrix.vecCons (fun k => ↑(rename (Prod.mk 0)) (φ k)) ![fun k => ↑(rename (Prod.mk 1)) (ψ k)]
        { val := 1, isLt := (_ : (fun a => a < 2) 1) } n)
[PROOFSTEP]
simp only [algebraMap_int_eq, coe_eval₂Hom, Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one,
  cons_val_zero, cons_val_one, eval₂Hom_rename, Function.comp, head_fin_const]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly₂ p f
⊢ IsPoly₂ p fun R _Rcr x y => g (f x y)
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun R _Rcr x y => g (f x y)
[PROOFSTEP]
obtain ⟨ψ, hg⟩ := hg
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ IsPoly₂ p fun R _Rcr x y => g (f x y)
[PROOFSTEP]
use fun n => bind₁ φ (ψ n)
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x y : 𝕎 R),
    (g (f x y)).coeff = fun n => peval (↑(bind₁ φ) (ψ n)) ![x.coeff, y.coeff]
[PROOFSTEP]
intros
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
g : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type ?u.617903⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type ?u.617903⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type ?u.617903
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (g (f x✝ y✝)).coeff = fun n => peval (↑(bind₁ φ) (ψ n)) ![x✝.coeff, y✝.coeff]
[PROOFSTEP]
simp only [peval, aeval_bind₁, Function.comp, hg, hf]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
⊢ IsPoly p fun R _Rcr x => f x x
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ IsPoly p fun R _Rcr x => f x x
[PROOFSTEP]
refine' ⟨⟨fun n => bind₁ (uncurry ![X, X]) (φ n), _⟩⟩
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x x).coeff = fun n => ↑(aeval x.coeff) ((fun n => ↑(bind₁ (uncurry ![X, X])) (φ n)) n)
[PROOFSTEP]
intros
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (f x✝ x✝).coeff = fun n => ↑(aeval x✝.coeff) ((fun n => ↑(bind₁ (uncurry ![X, X])) (φ n)) n)
[PROOFSTEP]
funext n
[GOAL]
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (f x✝ x✝) n = ↑(aeval x✝.coeff) ((fun n => ↑(bind₁ (uncurry ![X, X])) (φ n)) n)
[PROOFSTEP]
simp only [hf, peval, uncurry, aeval_bind₁]
[GOAL]
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ ↑(aeval fun a => Matrix.vecCons x✝.coeff ![x✝.coeff] a.fst a.snd) (φ n) =
    ↑(aeval fun i => ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] i.fst i.snd)) (φ n)
[PROOFSTEP]
apply eval₂Hom_congr rfl _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ (fun a => Matrix.vecCons x✝.coeff ![x✝.coeff] a.fst a.snd) = fun i =>
    ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] i.fst i.snd)
[PROOFSTEP]
ext ⟨i, k⟩
[GOAL]
case h.mk
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
i : Fin 2
k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] (i, k).fst (i, k).snd =
    ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] (i, k).fst (i, k).snd)
[PROOFSTEP]
fin_cases i
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] ({ val := 0, isLt := (_ : 0 < 2) }, k).fst
      ({ val := 0, isLt := (_ : 0 < 2) }, k).snd =
    ↑(aeval x✝.coeff)
      (Matrix.vecCons X ![X] ({ val := 0, isLt := (_ : 0 < 2) }, k).fst ({ val := 0, isLt := (_ : 0 < 2) }, k).snd)
[PROOFSTEP]
simp only [Matrix.head_cons, aeval_X, Matrix.cons_val_zero, Matrix.cons_val_one]
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).fst
      ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).snd =
    ↑(aeval x✝.coeff)
      (Matrix.vecCons X ![X] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).fst
        ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).snd)
[PROOFSTEP]
simp only [Matrix.head_cons, aeval_X, Matrix.cons_val_zero, Matrix.cons_val_one]
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] { val := 0, isLt := (_ : 0 < 2) } k =
    ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] { val := 0, isLt := (_ : 0 < 2) } k)
[PROOFSTEP]
open Matrix in
  simp only [Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one, cons_val_zero, aeval_X, head_fin_const,
    cons_val_one]
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] { val := 0, isLt := (_ : 0 < 2) } k =
    ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] { val := 0, isLt := (_ : 0 < 2) } k)
[PROOFSTEP]
simp only [Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one, cons_val_zero, aeval_X, head_fin_const,
  cons_val_one]
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] { val := 1, isLt := (_ : (fun a => a < 2) 1) } k =
    ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] { val := 1, isLt := (_ : (fun a => a < 2) 1) } k)
[PROOFSTEP]
open Matrix in
  simp only [Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one, cons_val_zero, aeval_X, head_fin_const,
    cons_val_one]
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type ?u.635087⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type ?u.635087⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
R✝ : Type ?u.635087
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ Matrix.vecCons x✝.coeff ![x✝.coeff] { val := 1, isLt := (_ : (fun a => a < 2) 1) } k =
    ↑(aeval x✝.coeff) (Matrix.vecCons X ![X] { val := 1, isLt := (_ : (fun a => a < 2) 1) } k)
[PROOFSTEP]
simp only [Fin.mk_zero, Fin.mk_one, cons_val', empty_val', cons_val_fin_one, cons_val_zero, aeval_X, head_fin_const,
  cons_val_one]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type ?u.656753⦄ [inst : CommRing R] (x : 𝕎 R),
    (-x).coeff = fun n => ↑(aeval x.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.656753
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (-x✝).coeff = fun n => ↑(aeval x✝.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
[PROOFSTEP]
funext n
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.656753
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (-x✝) n = ↑(aeval x✝.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
[PROOFSTEP]
rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.656753
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = ↑(eval₂Hom (algebraMap ℤ R✝) (x✝.coeff ∘ Prod.snd)) (wittNeg p n)
[PROOFSTEP]
apply eval₂Hom_congr rfl _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.656753
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ uncurry ![x✝.coeff] = x✝.coeff ∘ Prod.snd
[PROOFSTEP]
ext ⟨i, k⟩
[GOAL]
case h.mk
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.656753
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
i : Fin 1
k : ℕ
⊢ uncurry ![x✝.coeff] (i, k) = (x✝.coeff ∘ Prod.snd) (i, k)
[PROOFSTEP]
fin_cases i
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.656753
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ uncurry ![x✝.coeff] ({ val := 0, isLt := (_ : 0 < 1) }, k) =
    (x✝.coeff ∘ Prod.snd) ({ val := 0, isLt := (_ : 0 < 1) }, k)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type ?u.675319⦄ [inst : CommRing R] (x : 𝕎 R), 0.coeff = fun n => ↑(aeval x.coeff) (OfNat.ofNat 0 n)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.675319
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ 0.coeff = fun n => ↑(aeval x✝.coeff) (OfNat.ofNat 0 n)
[PROOFSTEP]
funext n
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.675319
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff 0 n = ↑(aeval x✝.coeff) (OfNat.ofNat 0 n)
[PROOFSTEP]
simp only [Pi.zero_apply, AlgHom.map_zero, zero_coeff]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ ↑(bind₁ 0) (wittPolynomial p R n) = 0
[PROOFSTEP]
rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, RingHom.map_zero]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑(bind₁ onePoly) (wittPolynomial p ℤ n) = 1
[PROOFSTEP]
ext
  -- porting note: `ext` was not in the mathport output.
[GOAL]
case a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(bind₁ onePoly) (wittPolynomial p ℤ n)) = MvPolynomial.coeff m✝ 1
[PROOFSTEP]
rw [wittPolynomial_eq_sum_C_mul_X_pow, AlgHom.map_sum, Finset.sum_eq_single 0]
[GOAL]
case a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0))) = MvPolynomial.coeff m✝ 1
[PROOFSTEP]
simp only [onePoly, one_pow, one_mul, AlgHom.map_pow, C_1, pow_zero, bind₁_X_right, if_true, eq_self_iff_true]
[GOAL]
case a.h₀
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑(bind₁ onePoly) (↑C (↑p ^ b) * X b ^ p ^ (n - b)) = 0
[PROOFSTEP]
intro i _hi hi0
[GOAL]
case a.h₀
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ ↑(bind₁ onePoly) (↑C (↑p ^ i) * X i ^ p ^ (n - i)) = 0
[PROOFSTEP]
simp only [onePoly, if_neg hi0, zero_pow (pow_pos hp.1.pos _), mul_zero, AlgHom.map_pow, bind₁_X_right, AlgHom.map_mul]
[GOAL]
case a.h₁
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
[PROOFSTEP]
rw [Finset.mem_range]
  -- porting note: was `decide`
[GOAL]
case a.h₁
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ¬0 < n + 1 → ↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
[PROOFSTEP]
simp only [add_pos_iff, or_true, not_true, pow_zero, map_one, ge_iff_le, nonpos_iff_eq_zero, tsub_zero, one_mul,
  gt_iff_lt, IsEmpty.forall_iff]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type ?u.716878⦄ [inst : CommRing R] (x : 𝕎 R), 1.coeff = fun n => ↑(aeval x.coeff) (onePoly n)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.716878
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ 1.coeff = fun n => ↑(aeval x✝.coeff) (onePoly n)
[PROOFSTEP]
funext n
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.716878
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff 1 n = ↑(aeval x✝.coeff) (onePoly n)
[PROOFSTEP]
cases n
[GOAL]
case h.zero
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.716878
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ coeff 1 Nat.zero = ↑(aeval x✝.coeff) (onePoly Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, lt_self_iff_false, one_coeff_zero, onePoly, ite_true, map_one]
[GOAL]
case h.succ
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.716878
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n✝ : ℕ
⊢ coeff 1 (Nat.succ n✝) = ↑(aeval x✝.coeff) (onePoly (Nat.succ n✝))
[PROOFSTEP]
simp only [Nat.succ_pos', one_coeff_eq_of_pos, onePoly, Nat.succ_ne_zero, ite_false, map_zero]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type ?u.719431⦄ [inst : CommRing R] (x y : 𝕎 R),
    (x + y).coeff = fun n => peval (wittAdd p n) ![x.coeff, y.coeff]
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.719431
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ + y✝).coeff = fun n => peval (wittAdd p n) ![x✝.coeff, y✝.coeff]
[PROOFSTEP]
ext
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.719431
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ coeff (x✝¹ + y✝) x✝ = peval (wittAdd p x✝) ![x✝¹.coeff, y✝.coeff]
[PROOFSTEP]
exact add_coeff _ _ _
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type ?u.719741⦄ [inst : CommRing R] (x y : 𝕎 R),
    (x * y).coeff = fun n => peval (wittMul p n) ![x.coeff, y.coeff]
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.719741
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ * y✝).coeff = fun n => peval (wittMul p n) ![x✝.coeff, y✝.coeff]
[PROOFSTEP]
ext
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type ?u.719741
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ coeff (x✝¹ * y✝) x✝ = peval (wittMul p x✝) ![x✝¹.coeff, y✝.coeff]
[PROOFSTEP]
exact mul_coeff _ _ _
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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)
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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)
[PROOFSTEP]
ext n
[GOAL]
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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
[PROOFSTEP]
simp only [map_coeff, hf, map_aeval]
[GOAL]
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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
[PROOFSTEP]
ext
  -- porting note: this `ext` was not present in the mathport output
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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✝
[PROOFSTEP]
simp only [map_coeff]
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
hg : IsPoly₂ p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly₂ p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y
[PROOFSTEP]
obtain ⟨ψ, hg⟩ := hg
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y
[PROOFSTEP]
intros
[GOAL]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ f x✝ y✝ = g x✝ y✝
[PROOFSTEP]
ext n
[GOAL]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ coeff (f x✝ y✝) n = coeff (g x✝ y✝) n
[PROOFSTEP]
rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq' p φ ψ]
  --  porting note: `clear x y` does not work, since `x, y` are now hygienic
[GOAL]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ ∀ (n : ℕ), ↑(bind₁ φ) (wittPolynomial p ℤ n) = ↑(bind₁ ψ) (wittPolynomial p ℤ n)
[PROOFSTEP]
intro k
[GOAL]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
⊢ ↑(bind₁ φ) (wittPolynomial p ℤ k) = ↑(bind₁ ψ) (wittPolynomial p ℤ k)
[PROOFSTEP]
apply MvPolynomial.funext
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
⊢ ∀ (x : Fin 2 × ℕ → ℤ),
    ↑(MvPolynomial.eval x) (↑(bind₁ φ) (wittPolynomial p ℤ k)) =
      ↑(MvPolynomial.eval x) (↑(bind₁ ψ) (wittPolynomial p ℤ k))
[PROOFSTEP]
intro x
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ φ) (wittPolynomial p ℤ k)) =
    ↑(MvPolynomial.eval x) (↑(bind₁ ψ) (wittPolynomial p ℤ k))
[PROOFSTEP]
simp only [hom_bind₁]
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ↑(ghostComponent n) (f x y) = ↑(ghostComponent n) (g x y)
φ : ℕ → 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
[PROOFSTEP]
specialize h (ULift ℤ) (mk p fun i => ⟨x (0, i)⟩) (mk p fun i => ⟨x (1, i)⟩) k
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(ghostComponent k) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })) =
    ↑(ghostComponent k) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) }))
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
[PROOFSTEP]
simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
[GOAL]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
[PROOFSTEP]
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
[GOAL]
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(RingEquiv.symm ULift.ringEquiv)
      (↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (φ i))
        (wittPolynomial p ℤ k)) =
    ↑(RingEquiv.symm ULift.ringEquiv)
      (↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k))
[PROOFSTEP]
simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
[GOAL]
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k)
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_2
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
case h.e'_3
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
[PROOFSTEP]
all_goals
  --  porting note: this proof started with `funext i`
  simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
  ext1
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
  ext ⟨b, _⟩
  fin_cases b <;> simp only [coeff_mk, uncurry] <;> rfl
[GOAL]
case h.e'_2
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
[PROOFSTEP]
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
[GOAL]
case h.e'_2
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (eval₂Hom (RingHom.id ℤ) x) C)) fun i =>
          ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
                ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
            (φ i))
      (wittPolynomial p ℤ k) =
    ↑(aeval fun n =>
          peval (φ n) ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff])
      (wittPolynomial p ℤ k)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ (fun i =>
      ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
            ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
        (φ i)) =
    fun n => peval (φ n) ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
[PROOFSTEP]
ext1
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
      (φ x✝) =
    peval (φ x✝) ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ (fun i => ↑↑(RingEquiv.symm ULift.ringEquiv) (x i)) =
    uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
[PROOFSTEP]
ext ⟨b, _⟩
[GOAL]
case h.mk.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
b : Fin 2
snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x (b, snd✝))).down =
    (uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff] (b, snd✝)).down
[PROOFSTEP]
fin_cases b
[GOAL]
case h.mk.h.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 0, isLt := (_ : 0 < 2) }, snd✝))).down =
    (uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
        ({ val := 0, isLt := (_ : 0 < 2) }, snd✝)).down
[PROOFSTEP]
simp only [coeff_mk, uncurry]
[GOAL]
case h.mk.h.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, snd✝))).down =
    (uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
        ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, snd✝)).down
[PROOFSTEP]
simp only [coeff_mk, uncurry]
[GOAL]
case h.mk.h.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 0, isLt := (_ : 0 < 2) }, snd✝))).down =
    (Matrix.vecCons (fun i => { down := x (0, i) }) ![fun i => { down := x (1, i) }] { val := 0, isLt := (_ : 0 < 2) }
        snd✝).down
[PROOFSTEP]
rfl
[GOAL]
case h.mk.h.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, snd✝))).down =
    (Matrix.vecCons (fun i => { down := x (0, i) }) ![fun i => { down := x (1, i) }]
        { val := 1, isLt := (_ : (fun a => a < 2) 1) } snd✝).down
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (MvPolynomial.eval x) C)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (↑(MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
[PROOFSTEP]
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
[GOAL]
case h.e'_3
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.comp (eval₂Hom (RingHom.id ℤ) x) C)) fun i =>
          ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
                ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
            (ψ i))
      (wittPolynomial p ℤ k) =
    ↑(aeval fun n =>
          peval (ψ n) ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff])
      (wittPolynomial p ℤ k)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
⊢ (fun i =>
      ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
            ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
        (ψ i)) =
    fun n => peval (ψ n) ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
[PROOFSTEP]
ext1
[GOAL]
case h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ ↑(eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv)) (RingHom.id ℤ)) fun i =>
          ↑↑(RingEquiv.symm ULift.ringEquiv) (x i))
      (ψ x✝) =
    peval (ψ x✝) ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
⊢ (fun i => ↑↑(RingEquiv.symm ULift.ringEquiv) (x i)) =
    uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
[PROOFSTEP]
ext ⟨b, _⟩
[GOAL]
case h.mk.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ : ℕ
b : Fin 2
snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x (b, snd✝))).down =
    (uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff] (b, snd✝)).down
[PROOFSTEP]
fin_cases b
[GOAL]
case h.mk.h.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 0, isLt := (_ : 0 < 2) }, snd✝))).down =
    (uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
        ({ val := 0, isLt := (_ : 0 < 2) }, snd✝)).down
[PROOFSTEP]
simp only [coeff_mk, uncurry]
[GOAL]
case h.mk.h.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, snd✝))).down =
    (uncurry ![(mk p fun i => { down := x (0, i) }).coeff, (mk p fun i => { down := x (1, i) }).coeff]
        ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, snd✝)).down
[PROOFSTEP]
simp only [coeff_mk, uncurry]
[GOAL]
case h.mk.h.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 0, isLt := (_ : 0 < 2) }, snd✝))).down =
    (Matrix.vecCons (fun i => { down := x (0, i) }) ![fun i => { down := x (1, i) }] { val := 0, isLt := (_ : 0 < 2) }
        snd✝).down
[PROOFSTEP]
rfl
[GOAL]
case h.mk.h.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  ↑(aeval (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) =
    ↑(aeval (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
x✝ snd✝ : ℕ
⊢ (↑↑(RingEquiv.symm ULift.ringEquiv) (x ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, snd✝))).down =
    (Matrix.vecCons (fun i => { down := x (0, i) }) ![fun i => { down := x (1, i) }]
        { val := 1, isLt := (_ : (fun a => a < 2) 1) } snd✝).down
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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)
[PROOFSTEP]
obtain ⟨φ, hf⟩ := hf
[GOAL]
case mk'.intro
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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)
[PROOFSTEP]
ext n
[GOAL]
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 : ℕ
⊢ coeff (↑(WittVector.map g) (f x y)) n = coeff (f (↑(WittVector.map g) x) (↑(WittVector.map g) y)) n
[PROOFSTEP]
simp only [map_coeff, hf, map_aeval, peval, uncurry]
[GOAL]
case mk'.intro.h
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 (RingHom.comp g (algebraMap ℤ R)) fun i => ↑g (Matrix.vecCons x.coeff ![y.coeff] i.fst i.snd)) (φ n) =
    ↑(aeval fun a => Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff] a.fst a.snd) (φ n)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 (Matrix.vecCons x.coeff ![y.coeff] i.fst i.snd)) = fun a =>
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff] a.fst a.snd
[PROOFSTEP]
try ext ⟨i, k⟩; fin_cases i
[GOAL]
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 (Matrix.vecCons x.coeff ![y.coeff] i.fst i.snd)) = fun a =>
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff] a.fst a.snd
[PROOFSTEP]
ext ⟨i, k⟩
[GOAL]
case h.mk
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 (Matrix.vecCons x.coeff ![y.coeff] (i, k).fst (i, k).snd) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff] (i, k).fst (i, k).snd
[PROOFSTEP]
fin_cases i
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g
      (Matrix.vecCons x.coeff ![y.coeff] ({ val := 0, isLt := (_ : 0 < 2) }, k).fst
        ({ val := 0, isLt := (_ : 0 < 2) }, k).snd) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff]
      ({ val := 0, isLt := (_ : 0 < 2) }, k).fst ({ val := 0, isLt := (_ : 0 < 2) }, k).snd
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g
      (Matrix.vecCons x.coeff ![y.coeff] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).fst
        ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).snd) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff]
      ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).fst ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).snd
[PROOFSTEP]
all_goals
  simp only [map_coeff, Matrix.cons_val_zero, Matrix.head_cons, Matrix.cons_val_one]
    -- porting note: added the rest of the proof
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g
      (Matrix.vecCons x.coeff ![y.coeff] ({ val := 0, isLt := (_ : 0 < 2) }, k).fst
        ({ val := 0, isLt := (_ : 0 < 2) }, k).snd) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff]
      ({ val := 0, isLt := (_ : 0 < 2) }, k).fst ({ val := 0, isLt := (_ : 0 < 2) }, k).snd
[PROOFSTEP]
simp only [map_coeff, Matrix.cons_val_zero, Matrix.head_cons, Matrix.cons_val_one]
  -- porting note: added the rest of the proof
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g
      (Matrix.vecCons x.coeff ![y.coeff] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).fst
        ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).snd) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff]
      ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).fst ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, k).snd
[PROOFSTEP]
simp only [map_coeff, Matrix.cons_val_zero, Matrix.head_cons, Matrix.cons_val_one]
  -- porting note: added the rest of the proof
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g (Matrix.vecCons x.coeff ![y.coeff] { val := 0, isLt := (_ : 0 < 2) } k) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff] { val := 0, isLt := (_ : 0 < 2) } k
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g (Matrix.vecCons x.coeff ![y.coeff] { val := 1, isLt := (_ : (fun a => a < 2) 1) } k) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } k
[PROOFSTEP]
all_goals
  simp only [Fin.mk_zero, Fin.mk_one, Matrix.cons_val', Matrix.empty_val', Matrix.cons_val_one, Matrix.cons_val_fin_one,
    Matrix.cons_val_zero, map_coeff, Matrix.head_fin_const]
[GOAL]
case h.mk.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g (Matrix.vecCons x.coeff ![y.coeff] { val := 0, isLt := (_ : 0 < 2) } k) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff] { val := 0, isLt := (_ : 0 < 2) } k
[PROOFSTEP]
simp only [Fin.mk_zero, Fin.mk_one, Matrix.cons_val', Matrix.empty_val', Matrix.cons_val_one, Matrix.cons_val_fin_one,
  Matrix.cons_val_zero, map_coeff, Matrix.head_fin_const]
[GOAL]
case h.mk.tail.head
p : ℕ
R S : Type u
σ : Type u_1
idx : Type u_2
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 k : ℕ
⊢ ↑g (Matrix.vecCons x.coeff ![y.coeff] { val := 1, isLt := (_ : (fun a => a < 2) 1) } k) =
    Matrix.vecCons (↑(WittVector.map g) x).coeff ![(↑(WittVector.map g) y).coeff]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } k
[PROOFSTEP]
simp only [Fin.mk_zero, Fin.mk_one, Matrix.cons_val', Matrix.empty_val', Matrix.cons_val_one, Matrix.cons_val_fin_one,
  Matrix.cons_val_zero, map_coeff, Matrix.head_fin_const]