[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Injective f
⊢ Injective (mapFun f)
[PROOFSTEP]
intros _ _ h
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Injective f
a₁✝ a₂✝ : 𝕎 α
h : mapFun f a₁✝ = mapFun f a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext p
[GOAL]
case h
p✝ : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p✝)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Injective f
a₁✝ a₂✝ : WittVector p✝ α
h : mapFun f a₁✝ = mapFun f a₂✝
p : ℕ
⊢ coeff a₁✝ p = coeff a₂✝ p
[PROOFSTEP]
exact hf (congr_arg (fun x => coeff x p) h : _)
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Surjective f
x : 𝕎 β
⊢ mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n)) = x
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Surjective f
x : 𝕎 β
n : ℕ
⊢ coeff (mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n))) n = coeff x n
[PROOFSTEP]
simp only [mapFun, coeff_mk, comp_apply, Classical.choose_spec (hf (x.coeff n))]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) 0 = 0
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) 1 = 1
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x + y) = mapFun (↑f) x + mapFun (↑f) y
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x - y) = mapFun (↑f) x - mapFun (↑f) y
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x * y) = mapFun (↑f) x * mapFun (↑f) y
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (-x) = -mapFun (↑f) x
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (n • x) = n • mapFun (↑f) x
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
z : ℤ
⊢ mapFun (↑f) (z • x) = z • mapFun (↑f) x
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (x ^ n) = mapFun (↑f) x ^ n
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (Nat.unaryCast n) = ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (Nat.unaryCast Nat.zero) = ↑Nat.zero
[PROOFSTEP]
simp [*, Nat.unaryCast, add, one, zero]
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n✝ : ℕ
n_ih✝ : mapFun (↑f) (Nat.unaryCast n✝) = ↑n✝
⊢ mapFun (↑f) (Nat.unaryCast (Nat.succ n✝)) = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*, Nat.unaryCast, add, one, zero]
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ 0 = ↑0
[PROOFSTEP]
rfl
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n✝ : ℕ
n_ih✝ : mapFun (↑f) (Nat.unaryCast n✝) = ↑n✝
⊢ ↑n✝ + 1 = ↑(Nat.succ n✝)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℤ
⊢ mapFun (↑f) (Int.castDef n) = ↑n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ mapFun (↑f) (Int.castDef (Int.ofNat a✝)) = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp [*, Int.castDef, add, one, neg, zero, nat_cast]
[GOAL]
case negSucc
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ mapFun (↑f) (Int.castDef (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp [*, Int.castDef, add, one, neg, zero, nat_cast]
[GOAL]
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ ↑a✝ = ↑↑a✝
[PROOFSTEP]
rfl
[GOAL]
case negSucc
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ -↑(a✝ + 1) = ↑(Int.negSucc a✝)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R✝ : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R✝
R : Type u_6
i : Fin 0
j : ℕ
⊢ coeff ![] j = ![]
[PROOFSTEP]
rcases i with ⟨_ | _ | _ | _ | i_val, ⟨⟩⟩
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun 0 = 0
[PROOFSTEP]
ghost_fun_tac 0,![]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun 1 = 1
[PROOFSTEP]
ghost_fun_tac 1,![]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (x + y) = WittVector.ghostFun x + WittVector.ghostFun y
[PROOFSTEP]
ghost_fun_tac X 0 + X 1,![x.coeff, y.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
i : ℕ
⊢ WittVector.ghostFun (Nat.unaryCast i) = ↑i
[PROOFSTEP]
induction i
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (Nat.unaryCast Nat.zero) = ↑Nat.zero
[PROOFSTEP]
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.coe_nat]
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
n✝ : ℕ
n_ih✝ : WittVector.ghostFun (Nat.unaryCast n✝) = ↑n✝
⊢ WittVector.ghostFun (Nat.unaryCast (Nat.succ n✝)) = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.coe_nat]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (x - y) = WittVector.ghostFun x - WittVector.ghostFun y
[PROOFSTEP]
ghost_fun_tac X 0 - X 1,![x.coeff, y.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (x * y) = WittVector.ghostFun x * WittVector.ghostFun y
[PROOFSTEP]
ghost_fun_tac X 0 * X 1,![x.coeff, y.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (-x) = -WittVector.ghostFun x
[PROOFSTEP]
ghost_fun_tac-X 0,![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
i : ℤ
⊢ WittVector.ghostFun (Int.castDef i) = ↑i
[PROOFSTEP]
cases i
[GOAL]
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
a✝ : ℕ
⊢ WittVector.ghostFun (Int.castDef (Int.ofNat a✝)) = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.coe_nat, -Pi.coe_int]
[GOAL]
case negSucc
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
a✝ : ℕ
⊢ WittVector.ghostFun (Int.castDef (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.coe_nat, -Pi.coe_int]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
m : ℕ
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
[PROOFSTEP]
ghost_fun_tac m • (X 0 : MvPolynomial _ ℤ),![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
m : ℤ
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
[PROOFSTEP]
ghost_fun_tac m • (X 0 : MvPolynomial _ ℤ),![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
m : ℕ
⊢ WittVector.ghostFun (x ^ m) = WittVector.ghostFun x ^ m
[PROOFSTEP]
ghost_fun_tac X 0 ^ m,![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
⊢ LeftInverse (fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) WittVector.ghostFun
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
⊢ (fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x) = x
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
⊢ coeff ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x)) n = coeff x n
[PROOFSTEP]
have := bind₁_wittPolynomial_xInTermsOfW p R n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
⊢ coeff ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x)) n = coeff x n
[PROOFSTEP]
apply_fun aeval x.coeff at this 
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : ↑(aeval x.coeff) (↑(bind₁ (W_ R)) (xInTermsOfW p R n)) = ↑(aeval x.coeff) (X n)
⊢ coeff ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x)) n = coeff x n
[PROOFSTEP]
simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
⊢ Function.RightInverse (fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) WittVector.ghostFun
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) = x
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) n = x n
[PROOFSTEP]
have := bind₁_xInTermsOfW_wittPolynomial p R n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : ↑(bind₁ (xInTermsOfW p R)) (W_ R n) = X n
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) n = x n
[PROOFSTEP]
apply_fun aeval x at this 
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : ↑(aeval x) (↑(bind₁ (xInTermsOfW p R)) (W_ R n)) = ↑(aeval x) (X n)
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) n = x n
[PROOFSTEP]
simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
⊢ (fun x => coeff x 0) 1 = 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => coeff x 0, map_one' := (_ : coeff 1 0 = 1) },
          map_mul' := (_ : ∀ (x y : 𝕎 R), coeff (x * y) 0 = coeff x 0 * coeff y 0) })
      0 =
    0
[PROOFSTEP]
simp
