case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ x ∈ RingHom.ker (toZModPow n) ↔ x ∈ Ideal.span {↑p ^ n}
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}
ext x
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ ↑(toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ x ∈ RingHom.ker (toZModPow n) ↔ x ∈ Ideal.span {↑p ^ n}
rw [RingHom.mem_ker]
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ ↑(toZModPow n) x = 0 → x ∈ Ideal.span {↑p ^ n}

case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ x ∈ Ideal.span {↑p ^ n} → ↑(toZModPow n) x = 0
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ ↑(toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}
constructor
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
⊢ x ∈ Ideal.span {↑p ^ n}
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ ↑(toZModPow n) x = 0 → x ∈ Ideal.span {↑p ^ n}
intro h
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
⊢ appr x n = 0
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
⊢ x ∈ Ideal.span {↑p ^ n}
suffices x.appr n = 0 by
  convert appr_spec n x
  simp only [this, sub_zero, cast_zero]
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(appr x n) = 0
⊢ appr x n = 0
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
⊢ appr x n = 0
dsimp [toZModPow, toZModHom] at h
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ appr x n
⊢ appr x n = 0
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(appr x n) = 0
⊢ appr x n = 0
rw [ZMod.nat_cast_zmod_eq_zero_iff_dvd] at h
no goals
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ appr x n
⊢ appr x n = 0
apply eq_zero_of_dvd_of_lt h (appr_lt _ _)
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
this : appr x n = 0
⊢ x = x - ↑(appr x n)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
this : appr x n = 0
⊢ x ∈ Ideal.span {↑p ^ n}
convert appr_spec n x
no goals
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : ↑(toZModPow n) x = 0
this : appr x n = 0
⊢ x = x - ↑(appr x n)
simp only [this, sub_zero, cast_zero]
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x ∈ Ideal.span {↑p ^ n}
⊢ ↑(toZModPow n) x = 0
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ x ∈ Ideal.span {↑p ^ n} → ↑(toZModPow n) x = 0
intro h
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(toZModPow n) x = 0
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x ∈ Ideal.span {↑p ^ n}
⊢ ↑(toZModPow n) x = 0
rw [← sub_zero x] at h
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(appr x n) = 0
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(toZModPow n) x = 0
dsimp [toZModPow, toZModHom]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(appr x n) ∈ Ideal.span {↑p ^ n}
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(appr x n) = 0
rw [zmod_congr_of_sub_mem_span n x _ 0 _ h, cast_zero]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(appr x n) ∈ Ideal.span {↑p ^ n}
apply appr_spec