[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : ↑p ^ i = 0
⊢ i = n
[PROOFSTEP]
contrapose! hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : i ≠ n
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
replace hin := lt_of_le_of_ne hin hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
clear hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
  rw [RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i = ↑(WittVector.truncate n) (↑p ^ i)
[PROOFSTEP]
rw [RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = ↑(WittVector.truncate n) (↑p ^ i)
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
rw [this, ne_eq, ext_iff, not_forall]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = ↑(WittVector.truncate n) (↑p ^ i)
⊢ ∃ x, ¬coeff x (↑(WittVector.truncate n) (↑p ^ i)) = coeff x 0
[PROOFSTEP]
clear this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ∃ x, ¬coeff x (↑(WittVector.truncate n) (↑p ^ i)) = coeff x 0
[PROOFSTEP]
use⟨i, hin⟩
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬coeff { val := i, isLt := hin } (↑(WittVector.truncate n) (↑p ^ i)) = coeff { val := i, isLt := hin } 0
[PROOFSTEP]
rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬1 = 0
[PROOFSTEP]
haveI : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : Nontrivial R
⊢ ¬1 = 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
[PROOFSTEP]
rw [card, ZMod.card]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : ZMod (p ^ n)
⊢ ?m.71174 ∣ p ^ n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ↑(RingHom.comp (truncate hm) (RingEquiv.toRingHom (zmodEquivTrunc p m))) x =
    ↑(zmodEquivTrunc p n) (↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) x)
[PROOFSTEP]
rw [commutes _ _ hm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ↑(RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p n)) (ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n)))) x =
    ↑(zmodEquivTrunc p n) (↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) x)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ ↑(RingEquiv.symm (zmodEquivTrunc p n)) (↑(truncate hm) x) =
    ↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) (↑(RingEquiv.symm (zmodEquivTrunc p m)) x)
[PROOFSTEP]
apply (zmodEquivTrunc p n).injective
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ ↑(zmodEquivTrunc p n) (↑(RingEquiv.symm (zmodEquivTrunc p n)) (↑(truncate hm) x)) =
    ↑(zmodEquivTrunc p n)
      (↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) (↑(RingEquiv.symm (zmodEquivTrunc p m)) x))
[PROOFSTEP]
rw [← commutes' _ _ hm]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ ↑(zmodEquivTrunc p n) (↑(RingEquiv.symm (zmodEquivTrunc p n)) (↑(truncate hm) x)) =
    ↑(truncate hm) (↑(zmodEquivTrunc p m) (↑(RingEquiv.symm (zmodEquivTrunc p m)) x))
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
⊢ RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate hm) =
    RingHom.comp (ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n)))
      (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m)))
[PROOFSTEP]
ext
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x✝ : TruncatedWittVector p m (ZMod p)
⊢ ↑(RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate hm)) x✝ =
    ↑(RingHom.comp (ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n)))
          (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))))
      x✝
[PROOFSTEP]
apply commutes_symm'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m)))
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)) =
    RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n)
[PROOFSTEP]
rw [commutes_symm, RingHom.comp_assoc]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n) =
    RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m)
[PROOFSTEP]
rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ RingHom.comp (TruncatedWittVector.truncate hk)
      (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)) =
    RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁)
[PROOFSTEP]
rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc, PadicInt.zmod_cast_comp_toZModPow _ _ hk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ RingHom.comp (toPadicInt p) (fromPadicInt p) = RingHom.id ℤ_[p]
[PROOFSTEP]
rw [← PadicInt.toZModPow_eq_iff_ext]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    RingHom.comp (PadicInt.toZModPow n) (RingHom.comp (toPadicInt p) (fromPadicInt p)) =
      RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p])
[PROOFSTEP]
intro n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (PadicInt.toZModPow n) (RingHom.comp (toPadicInt p) (fromPadicInt p)) =
    RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p])
[PROOFSTEP]
rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (toZModPow p n) (fromPadicInt p) = RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p])
[PROOFSTEP]
simp only [fromPadicInt, toZModPow, RingHom.comp_id]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n))
      (lift (fun k => RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k)) (PadicInt.toZModPow k))
        (_ :
          ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂),
            RingHom.comp (TruncatedWittVector.truncate hk)
                (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)) =
              RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))) =
    PadicInt.toZModPow n
[PROOFSTEP]
rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n)))
        (RingEquiv.toRingHom (zmodEquivTrunc p n)))
      (PadicInt.toZModPow n) =
    PadicInt.toZModPow n
[PROOFSTEP]
simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑(RingHom.comp (toPadicInt p) (fromPadicInt p)) x = ↑(RingHom.id ℤ_[p]) x
[PROOFSTEP]
rw [toPadicInt_comp_fromPadicInt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ RingHom.comp (fromPadicInt p) (toPadicInt p) = RingHom.id (𝕎 (ZMod p))
[PROOFSTEP]
apply WittVector.hom_ext
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (k : ℕ),
    RingHom.comp (truncate k) (RingHom.comp (fromPadicInt p) (toPadicInt p)) =
      RingHom.comp (truncate k) (RingHom.id (𝕎 (ZMod p)))
[PROOFSTEP]
intro n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (truncate n) (RingHom.comp (fromPadicInt p) (toPadicInt p)) =
    RingHom.comp (truncate n) (RingHom.id (𝕎 (ZMod p)))
[PROOFSTEP]
rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p n)) (RingHom.comp (PadicInt.toZModPow n) (toPadicInt p)) =
    RingHom.comp (truncate n) (RingHom.id (𝕎 (ZMod p)))
[PROOFSTEP]
simp only [toPadicInt, toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingHom.id_comp, ← RingHom.comp_assoc,
  RingEquiv.toRingHom_comp_symm_toRingHom]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ ↑(RingHom.comp (fromPadicInt p) (toPadicInt p)) x = ↑(RingHom.id (𝕎 (ZMod p))) x
[PROOFSTEP]
rw [fromPadicInt_comp_toPadicInt]
