case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
obtain ⟨φ, hf⟩ := hf
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
obtain ⟨ψ, hg⟩ := hg
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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✝
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
intros
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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✝
ext n
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq p φ ψ]
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
intro k
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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))
case mk'.intro.mk'.intro.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
apply MvPolynomial.funext
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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))
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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))
intro x
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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))
simp only [hom_bind₁]
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
specialize h (ULift ℤ) (mk p fun i => ⟨x i⟩) k
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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))
case mk'.intro.mk'.intro.h.h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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))
simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
case h.e'_2
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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.168788
idx : Type ?u.168791
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)
case mk'.intro.mk'.intro.h.h.a
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
convert h using 1
no goals
case h.e'_2
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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.168788
idx : Type ?u.168791
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)
all_goals
  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
case h.e'_3
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case h.e'_3
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
case h.e'_3
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
case h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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✝)
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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)
ext1
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
case h
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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✝)
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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 }
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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
simp only [coeff_mk]
no goals
p : ℕ
R S : Type u
σ : Type ?u.168788
idx : Type ?u.168791
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 }
rfl