[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ modPart p r < ↑p
[PROOFSTEP]
convert Int.emod_lt _ _
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = |↑p|
[PROOFSTEP]
simp
[GOAL]
case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp_prime.1.ne_zero
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp_prime.1.ne_zero
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ IsUnit ↑r.den
[PROOFSTEP]
rw [isUnit_iff]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ‖↑r.den‖ = 1
[PROOFSTEP]
apply le_antisymm (r.den : ℤ_[p]).2
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ 1 ≤ ‖↑↑r.den‖
[PROOFSTEP]
rw [← not_lt, coe_nat_cast]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ¬‖↑r.den‖ < 1
[PROOFSTEP]
intro norm_denom_lt
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ False
[PROOFSTEP]
have hr : ‖(r * r.den : ℚ_[p])‖ = ‖(r.num : ℚ_[p])‖ := by
  congr
  rw_mod_cast [@Rat.mul_den_eq_num r]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ ‖↑r * ↑r.den‖ = ‖↑r.num‖
[PROOFSTEP]
congr
[GOAL]
case e_a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ ↑r * ↑r.den = ↑r.num
[PROOFSTEP]
rw_mod_cast [@Rat.mul_den_eq_num r]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r * ↑r.den‖ = ‖↑r.num‖
⊢ False
[PROOFSTEP]
rw [padicNormE.mul] at hr
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
⊢ False
[PROOFSTEP]
have key : ‖(r.num : ℚ_[p])‖ < 1 := by
  calc
    _ = _ := hr.symm
    _ < 1 * 1 := (mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one)
    _ = 1 := mul_one 1
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
⊢ ‖↑r.num‖ < 1
[PROOFSTEP]
calc
  _ = _ := hr.symm
  _ < 1 * 1 := (mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one)
  _ = 1 := mul_one 1
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
⊢ False
[PROOFSTEP]
have : ↑p ∣ r.num ∧ (p : ℤ) ∣ r.den :=
  by
  simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]
  exact ⟨key, norm_denom_lt⟩
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
⊢ ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
[PROOFSTEP]
simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
⊢ ‖↑↑r.num‖ < 1 ∧ ‖↑↑↑r.den‖ < 1
[PROOFSTEP]
exact ⟨key, norm_denom_lt⟩
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
⊢ False
[PROOFSTEP]
apply hp_prime.1.not_dvd_one
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
⊢ p ∣ 1
[PROOFSTEP]
rwa [← r.reduced.gcd_eq_one, Nat.dvd_gcd_iff, ← Int.coe_nat_dvd_left, ← Int.coe_nat_dvd]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑p ∣ r.num - r.num * gcdA r.den p % ↑p * ↑r.den
[PROOFSTEP]
rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑(r.num - r.num * gcdA r.den p % ↑p * ↑r.den) = 0
[PROOFSTEP]
simp only [Int.cast_ofNat, ZMod.nat_cast_mod, Int.cast_mul, Int.cast_sub]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
[PROOFSTEP]
have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : (fun x => ↑x % ↑p) ↑(Nat.gcd r.den p) = (fun x => ↑x % ↑p) (↑r.den * gcdA r.den p + ↑p * gcdB r.den p)
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
[PROOFSTEP]
simp only [Int.cast_ofNat, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add, Int.cast_mul, zero_mul,
  add_zero] at this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
[PROOFSTEP]
push_cast
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑r.num * ↑(gcdA r.den p) * ↑r.den = 0
[PROOFSTEP]
rw [mul_right_comm, mul_assoc, ← this]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑r.num * ↑(Nat.gcd r.den p) = 0
[PROOFSTEP]
suffices rdcp : r.den.coprime p
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
rdcp : coprime r.den p
⊢ ↑r.num - ↑r.num * ↑(Nat.gcd r.den p) = 0
[PROOFSTEP]
rw [rdcp.gcd_eq_one]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
rdcp : coprime r.den p
⊢ ↑r.num - ↑r.num * ↑1 = 0
[PROOFSTEP]
simp only [mul_one, cast_one, sub_self]
[GOAL]
case rdcp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ coprime r.den p
[PROOFSTEP]
apply coprime.symm
[GOAL]
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ coprime p r.den
[PROOFSTEP]
apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right
[GOAL]
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ¬p ∣ r.den
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← norm_int_lt_one_iff_dvd, not_lt]
[GOAL]
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ 1 ≤ ‖↑↑r.den‖
[PROOFSTEP]
apply ge_of_eq
[GOAL]
case rdcp.a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ‖↑↑r.den‖ = 1
[PROOFSTEP]
rw [← isUnit_iff]
[GOAL]
case rdcp.a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ IsUnit ↑↑r.den
[PROOFSTEP]
exact isUnit_den r h
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ‖{ val := ↑r, property := h } - ↑(modPart p r)‖ < 1
[PROOFSTEP]
let n := modPart p r
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ‖{ val := ↑r, property := h } - ↑(modPart p r)‖ < 1
[PROOFSTEP]
rw [norm_lt_one_iff_dvd, ← (isUnit_den r h).dvd_mul_right]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ ({ val := ↑r, property := h } - ↑(modPart p r)) * ↑r.den
[PROOFSTEP]
suffices ↑p ∣ r.num - n * r.den by
  convert (Int.castRingHom ℤ_[p]).map_dvd this
  simp only [sub_mul, Int.cast_ofNat, eq_intCast, Int.cast_mul, sub_left_inj, Int.cast_sub]
  apply Subtype.coe_injective
  simp only [coe_mul, Subtype.coe_mk, coe_nat_cast]
  rw_mod_cast [@Rat.mul_den_eq_num r]
  rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑p ∣ ({ val := ↑r, property := h } - ↑(modPart p r)) * ↑r.den
[PROOFSTEP]
convert (Int.castRingHom ℤ_[p]).map_dvd this
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ({ val := ↑r, property := h } - ↑(modPart p r)) * ↑r.den = ↑(Int.castRingHom ℤ_[p]) (r.num - n * ↑r.den)
[PROOFSTEP]
simp only [sub_mul, Int.cast_ofNat, eq_intCast, Int.cast_mul, sub_left_inj, Int.cast_sub]
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ { val := ↑r, property := h } * ↑r.den = ↑r.num
[PROOFSTEP]
apply Subtype.coe_injective
[GOAL]
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ (fun a => ↑a) ({ val := ↑r, property := h } * ↑r.den) = (fun a => ↑a) ↑r.num
[PROOFSTEP]
simp only [coe_mul, Subtype.coe_mk, coe_nat_cast]
[GOAL]
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑r * ↑r.den = ↑↑r.num
[PROOFSTEP]
rw_mod_cast [@Rat.mul_den_eq_num r]
[GOAL]
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
h : ‖↑r‖ ≤ 1
⊢ ↑↑r.num = ↑r.num
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ r.num - n * ↑r.den
[PROOFSTEP]
exact norm_sub_modPart_aux r h
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b
[PROOFSTEP]
rw [Ideal.mem_span_singleton] at ha hb
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b
[PROOFSTEP]
rw [← sub_eq_zero, ← Int.cast_sub, ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.coe_nat_pow]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
[PROOFSTEP]
rw [← dvd_neg, neg_sub] at ha
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha✝ : ↑p ^ n ∣ x - ↑a
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
[PROOFSTEP]
have := dvd_add ha hb
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha✝ : ↑p ^ n ∣ x - ↑a
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - x + (x - ↑b)
⊢ ↑p ^ n ∣ a - b
[PROOFSTEP]
rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ← Int.cast_sub,
  pow_p_dvd_int_iff, Nat.cast_pow] at this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b
[PROOFSTEP]
simpa using zmod_congr_of_sub_mem_span_aux n x a b ha hb
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ maximalIdeal ℤ_[p]
hn : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ↑m = ↑n
[PROOFSTEP]
rw [maximalIdeal_eq_span_p] at hm hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
⊢ ↑m = ↑n
[PROOFSTEP]
have := zmod_congr_of_sub_mem_span_aux 1 x m n
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : x - ↑↑m ∈ Ideal.span {↑p ^ 1} → x - ↑↑n ∈ Ideal.span {↑p ^ 1} → ↑↑m = ↑↑n
⊢ ↑m = ↑n
[PROOFSTEP]
simp only [pow_one] at this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : x - ↑↑m ∈ Ideal.span {↑p} → x - ↑↑n ∈ Ideal.span {↑p} → ↑↑m = ↑↑n
⊢ ↑m = ↑n
[PROOFSTEP]
specialize this hm hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n
[PROOFSTEP]
apply_fun ZMod.castHom (show p ∣ p ^ 1 by rw [pow_one]) (ZMod p) at this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ p ∣ p ^ 1
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑(ZMod.castHom (_ : p ∣ p ^ 1) (ZMod p)) ↑↑m = ↑(ZMod.castHom (_ : p ∣ p ^ 1) (ZMod p)) ↑↑n
⊢ ↑m = ↑n
[PROOFSTEP]
simp only [map_intCast] at this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n
[PROOFSTEP]
simpa only [Int.cast_ofNat] using this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∃ n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
[PROOFSTEP]
obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
[PROOFSTEP]
have H : ‖(r : ℚ_[p])‖ ≤ 1 := by
  rw [norm_sub_rev] at hr
  calc
    _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
    _ ≤ _ := (padicNormE.nonarchimedean _ _)
    _ ≤ _ := max_le (le_of_lt hr) x.2
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ‖↑r‖ ≤ 1
[PROOFSTEP]
rw [norm_sub_rev] at hr
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ ≤ 1
[PROOFSTEP]
calc
  _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
  _ ≤ _ := (padicNormE.nonarchimedean _ _)
  _ ≤ _ := max_le (le_of_lt hr) x.2
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ = ‖↑r - ↑x + ↑x‖
[PROOFSTEP]
ring_nf
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
[PROOFSTEP]
obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑n‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
[PROOFSTEP]
lift n to ℕ using hzn
[GOAL]
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
[PROOFSTEP]
use n
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ n < p ∧ ‖x - ↑n‖ < 1
[PROOFSTEP]
constructor
[GOAL]
case h.left
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ n < p
[PROOFSTEP]
exact_mod_cast hnp
[GOAL]
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ ‖x - ↑n‖ < 1
[PROOFSTEP]
simp only [norm_def, coe_sub, Subtype.coe_mk, coe_nat_cast] at hn ⊢
[GOAL]
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑n‖ < 1
[PROOFSTEP]
rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ↑x - ↑n = ↑x - ↑r + (↑r - ↑n)
[PROOFSTEP]
ring
[GOAL]
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r + (↑r - ↑n)‖ < 1
[PROOFSTEP]
apply lt_of_le_of_lt (padicNormE.nonarchimedean _ _)
[GOAL]
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ max ‖↑x - ↑r‖ ‖↑r - ↑n‖ < 1
[PROOFSTEP]
apply max_lt hr
[GOAL]
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1
[PROOFSTEP]
simpa using hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ (fun x => ↑(f x)) 1 = 1
[PROOFSTEP]
dsimp only
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ↑(f 1) = 1
[PROOFSTEP]
rw [f_congr (1 : ℤ_[p]) _ 1, cast_one]
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 1 - ↑(f 1) ∈ Ideal.span {↑v}
[PROOFSTEP]
exact f_spec _
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 1 - ↑1 ∈ Ideal.span {↑v}
[PROOFSTEP]
simp only [sub_self, cast_one, Submodule.zero_mem]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ∀ (x y : ℤ_[p]),
    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
        OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y
[PROOFSTEP]
intro x y
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y
[PROOFSTEP]
dsimp only
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ ↑(f (x * y)) = ↑(f x) * ↑(f y)
[PROOFSTEP]
rw [f_congr (x * y) _ (f x * f y), cast_mul]
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x * y - ↑(f (x * y)) ∈ Ideal.span {↑v}
[PROOFSTEP]
exact f_spec _
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x * y - ↑(f x * f y) ∈ Ideal.span {↑v}
[PROOFSTEP]
let I : Ideal ℤ_[p] := Ideal.span {↑v}
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {↑v}
⊢ x * y - ↑(f x * f y) ∈ Ideal.span {↑v}
[PROOFSTEP]
convert I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x)) using 1
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {↑v}
⊢ x * y - ↑(f x * f y) = x * (y - ↑(f y)) + (x - ↑(f x)) * ↑(f y)
[PROOFSTEP]
rw [cast_mul]
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {↑v}
⊢ x * y - ↑(f x) * ↑(f y) = x * (y - ↑(f y)) + (x - ↑(f x)) * ↑(f y)
[PROOFSTEP]
ring
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : ℤ_[p]),
                OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                  OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
      0 =
    0
[PROOFSTEP]
dsimp only
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ↑(f 0) = 0
[PROOFSTEP]
rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 0 - ↑(f 0) ∈ Ideal.span {↑v}
[PROOFSTEP]
exact f_spec _
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 0 - ↑0 ∈ Ideal.span {↑v}
[PROOFSTEP]
simp only [sub_zero, cast_zero, Submodule.zero_mem]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ∀ (x y : ℤ_[p]),
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ℤ_[p]),
                  OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ℤ_[p]),
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                        OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ℤ_[p]),
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                        OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
          y
[PROOFSTEP]
intro x y
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : ℤ_[p]),
                OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                  OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
      (x + y) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ℤ_[p]),
                  OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
        x +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ℤ_[p]),
                  OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } x *
                      OneHom.toFun { toFun := fun x => ↑(f x), map_one' := (_ : (fun x => ↑(f x)) 1 = 1) } y) })
        y
[PROOFSTEP]
dsimp only
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ ↑(f (x + y)) = ↑(f x) + ↑(f y)
[PROOFSTEP]
rw [f_congr (x + y) _ (f x + f y), cast_add]
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - ↑(f (x + y)) ∈ Ideal.span {↑v}
[PROOFSTEP]
exact f_spec _
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - ↑(f x + f y) ∈ Ideal.span {↑v}
[PROOFSTEP]
convert Ideal.add_mem _ (f_spec x) (f_spec y) using 1
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - ↑(f x + f y) = x - ↑(f x) + (y - ↑(f y))
[PROOFSTEP]
rw [cast_add]
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - (↑(f x) + ↑(f y)) = x - ↑(f x) + (y - ↑(f y))
[PROOFSTEP]
ring
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑(zmodRepr x) ∈ Ideal.span {↑p}
[PROOFSTEP]
rw [← maximalIdeal_eq_span_p]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
exact sub_zmodRepr_mem
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑p} → x - ↑b ∈ Ideal.span {↑p} → ↑a = ↑b
[PROOFSTEP]
rw [← maximalIdeal_eq_span_p]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ maximalIdeal ℤ_[p] → x - ↑b ∈ maximalIdeal ℤ_[p] → ↑a = ↑b
[PROOFSTEP]
exact zmod_congr_of_sub_mem_max_ideal
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ x - ↑(↑toZMod x) ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
convert sub_zmodRepr_mem x using 2
[GOAL]
case h.e'_4.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ↑(↑toZMod x) = ↑(zmodRepr x)
[PROOFSTEP]
dsimp [toZMod, toZModHom]
[GOAL]
case h.e'_4.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ↑↑(zmodRepr x) = ↑(zmodRepr x)
[PROOFSTEP]
rcases exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
[GOAL]
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑↑(zmodRepr x) = ↑(zmodRepr x)
[PROOFSTEP]
change ↑((_ : ZMod (0 + p' + 1)).val) = (_ : ℤ_[0 + p' + 1])
[GOAL]
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(ZMod.val ↑(zmodRepr x)) = ↑(zmodRepr x)
[PROOFSTEP]
simp only [ZMod.val_nat_cast, add_zero, add_def, Nat.cast_inj, zero_add]
[GOAL]
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ zmodRepr x % (p' + 1) = zmodRepr x
[PROOFSTEP]
apply mod_eq_of_lt
[GOAL]
case h.e'_4.h.e'_6.intro.h
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ zmodRepr x < p' + 1
[PROOFSTEP]
simpa only [zero_add] using zmodRepr_lt_p x
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ RingHom.ker toZMod = maximalIdeal ℤ_[p]
[PROOFSTEP]
ext x
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
rw [RingHom.mem_ker]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ↑toZMod x = 0 ↔ x ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
constructor
[GOAL]
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ↑toZMod x = 0 → x ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
intro h
[GOAL]
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : ↑toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x
[GOAL]
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → ↑toZMod x = 0
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x ∈ maximalIdeal ℤ_[p]
⊢ ↑toZMod x = 0
[PROOFSTEP]
rw [← sub_zero x] at h
[GOAL]
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑toZMod x = 0
[PROOFSTEP]
dsimp [toZMod, toZModHom]
[GOAL]
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑(zmodRepr x) = 0
[PROOFSTEP]
convert zmod_congr_of_sub_mem_max_ideal x _ 0 _ h
[GOAL]
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ 0 = ↑0
case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
norm_cast
[GOAL]
case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
apply sub_zmodRepr_mem
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n < p ^ n
[PROOFSTEP]
induction' n with n ih generalizing x
[GOAL]
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ x : ℤ_[p]
⊢ appr x zero < p ^ zero
[PROOFSTEP]
simp only [appr, zero_eq, _root_.pow_zero, zero_lt_one]
[GOAL]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ appr x (succ n) < p ^ succ n
[PROOFSTEP]
simp only [appr, map_natCast, ZMod.nat_cast_self, RingHom.map_pow, Int.natAbs, RingHom.map_mul]
[GOAL]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ (if h : x - ↑(appr x n) = 0 then appr x n
    else
      appr x n +
        p ^ n *
          ZMod.val
            (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
              0 ^
                match valuation (x - ↑(appr x n)) - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => succ m)) <
    p ^ succ n
[PROOFSTEP]
have hp : p ^ n < p ^ (n + 1) := by apply pow_lt_pow hp_prime.1.one_lt (lt_add_one n)
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ p ^ n < p ^ (n + 1)
[PROOFSTEP]
apply pow_lt_pow hp_prime.1.one_lt (lt_add_one n)
[GOAL]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
⊢ (if h : x - ↑(appr x n) = 0 then appr x n
    else
      appr x n +
        p ^ n *
          ZMod.val
            (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
              0 ^
                match valuation (x - ↑(appr x n)) - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => succ m)) <
    p ^ succ n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : x - ↑(appr x n) = 0
⊢ appr x n < p ^ succ n
[PROOFSTEP]
apply lt_trans (ih _) hp
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ appr x n +
      p ^ n *
        ZMod.val
          (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
            0 ^
              match valuation (x - ↑(appr x n)) - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => succ m) <
    p ^ succ n
[PROOFSTEP]
calc
  _ < p ^ n + p ^ n * (p - 1) := ?_
  _ = p ^ (n + 1) := ?_
[GOAL]
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ appr x n +
      p ^ n *
        ZMod.val
          (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
            0 ^
              match valuation (x - ↑(appr x n)) - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => succ m) <
    p ^ n + p ^ n * (p - 1)
[PROOFSTEP]
apply add_lt_add_of_lt_of_le (ih _)
[GOAL]
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n *
      ZMod.val
        (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
          0 ^
            match valuation (x - ↑(appr x n)) - ↑n with
            | Int.ofNat m => m
            | Int.negSucc m => succ m) ≤
    p ^ n * (p - 1)
[PROOFSTEP]
apply Nat.mul_le_mul_left
[GOAL]
case neg.calc_1.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ ZMod.val
      (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
        0 ^
          match valuation (x - ↑(appr x n)) - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => succ m) ≤
    p - 1
[PROOFSTEP]
apply le_pred_of_lt
[GOAL]
case neg.calc_1.h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ ZMod.val
      (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
        0 ^
          match valuation (x - ↑(appr x n)) - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => succ m) <
    p
[PROOFSTEP]
apply ZMod.val_lt
[GOAL]
case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
[PROOFSTEP]
rw [mul_tsub, mul_one, ← _root_.pow_succ']
[GOAL]
case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)
[PROOFSTEP]
apply add_tsub_cancel_of_le (le_of_lt hp)
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ Monotone (appr x)
[PROOFSTEP]
apply monotone_nat_of_le_succ
[GOAL]
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (n : ℕ), appr x n ≤ appr x (n + 1)
[PROOFSTEP]
intro n
[GOAL]
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n ≤ appr x (n + 1)
[PROOFSTEP]
dsimp [appr]
[GOAL]
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n ≤
    if hy : x - ↑(appr x n) = 0 then appr x n
    else appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n)))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
h✝ : x - ↑(appr x n) = 0
⊢ appr x n ≤ appr x n
[PROOFSTEP]
rfl
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(appr x n) = 0
⊢ appr x n ≤
    appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff h✝) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n)))
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ p ^ m ∣ appr x n - appr x m
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
h : m ≤ m + k
⊢ p ^ m ∣ appr x (m + k) - appr x m
[PROOFSTEP]
clear h
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
⊢ p ^ m ∣ appr x (m + k) - appr x m
[PROOFSTEP]
induction' k with k ih
[GOAL]
case intro.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m : ℕ
⊢ p ^ m ∣ appr x (m + zero) - appr x m
[PROOFSTEP]
simp only [zero_eq, add_zero, le_refl, tsub_eq_zero_of_le, ne_eq, Nat.isUnit_iff, dvd_zero]
[GOAL]
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
⊢ p ^ m ∣ appr x (m + succ k) - appr x m
[PROOFSTEP]
rw [Nat.succ_eq_add_one, ← add_assoc]
[GOAL]
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
⊢ p ^ m ∣ appr x (m + k + 1) - appr x m
[PROOFSTEP]
dsimp [appr]
[GOAL]
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
⊢ p ^ m ∣
    (if hy : x - ↑(appr x (m + k)) = 0 then appr x (m + k)
      else
        appr x (m + k) +
          p ^ (m + k) *
            ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k))))) -
      appr x m
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : x - ↑(appr x (m + k)) = 0
⊢ p ^ m ∣ appr x (m + k) - appr x m
[PROOFSTEP]
exact ih
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k)) = 0
⊢ p ^ m ∣
    appr x (m + k) +
        p ^ (m + k) *
          ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k)))) -
      appr x m
[PROOFSTEP]
rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k)))) +
      (appr x (m + k) - appr x m)
[PROOFSTEP]
apply dvd_add _ ih
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k))))
[PROOFSTEP]
apply dvd_mul_of_dvd_left
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k)) = 0
⊢ p ^ m ∣ p ^ (m + k)
[PROOFSTEP]
apply pow_dvd_pow _ (Nat.le_add_right m k)
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑(appr x n) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
simp only [Ideal.mem_span_singleton]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), ↑p ^ zero ∣ x - ↑(appr x zero)
[PROOFSTEP]
simp only [zero_eq, _root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
[GOAL]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
⊢ ∀ (x : ℤ_[p]), ↑p ^ succ n ∣ x - ↑(appr x (succ n))
[PROOFSTEP]
intro x
[GOAL]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
⊢ ↑p ^ succ n ∣ x - ↑(appr x (succ n))
[PROOFSTEP]
dsimp only [appr]
[GOAL]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
⊢ ↑p ^ succ n ∣
    x -
      ↑(if hy : x - ↑(appr x n) = 0 then appr x n
        else
          appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣ x - ↑(appr x n)
[PROOFSTEP]
rw [h]
[GOAL]
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣ 0
[PROOFSTEP]
apply dvd_zero
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
[PROOFSTEP]
push_cast
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x -
      (↑(appr x n) +
        ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n)))))
[PROOFSTEP]
rw [sub_add_eq_sub_sub]
[GOAL]
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n) -
      ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
[PROOFSTEP]
obtain ⟨c, hc⟩ := ih x
[GOAL]
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n) -
      ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
[PROOFSTEP]
simp only [map_natCast, ZMod.nat_cast_self, RingHom.map_pow, RingHom.map_mul, ZMod.nat_cast_val]
[GOAL]
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ ↑p ^ succ n ∣ x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
have hc' : c ≠ 0 := by
  rintro rfl
  simp only [mul_zero] at hc
  contradiction
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ c ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
hc : x - ↑(appr x n) = ↑p ^ n * 0
⊢ False
[PROOFSTEP]
simp only [mul_zero] at hc
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
hc : x - ↑(appr x n) = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
conv_rhs =>
  congr
  simp only [hc]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
| x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
  congr
  simp only [hc]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
| x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
  congr
  simp only [hc]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
| x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
congr
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
| x - ↑(appr x n)
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
| ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
simp only [hc]
[GOAL]
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ ↑p ^ n * c - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
[PROOFSTEP]
rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ valuation (x - ↑(appr x n)) = valuation (↑p ^ n * c)
[PROOFSTEP]
rw [hc]
[GOAL]
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ ↑p ^ n * c - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (↑p ^ n * c) - ↑n))
[PROOFSTEP]
rw [valuation_p_pow_mul _ _ hc', add_sub_cancel', _root_.pow_succ', ← mul_sub]
[GOAL]
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * (c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c)))
[PROOFSTEP]
apply mul_dvd_mul_left
[GOAL]
case neg.intro.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
[PROOFSTEP]
obtain hc0 | hc0 := c.valuation.natAbs.eq_zero_or_pos
[GOAL]
case neg.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
[PROOFSTEP]
simp only [hc0, mul_one, _root_.pow_zero]
[GOAL]
case neg.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
[PROOFSTEP]
rw [mul_comm, unitCoeff_spec h] at hc
[GOAL]
case neg.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
[PROOFSTEP]
suffices c = unitCoeff h by
  rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
  apply toZMod_spec
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
this : c = ↑(unitCoeff h)
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
[PROOFSTEP]
rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
this : c = ↑(unitCoeff h)
⊢ c - ↑(↑toZMod c) ∈ maximalIdeal ℤ_[p]
[PROOFSTEP]
apply toZMod_spec
[GOAL]
case neg.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ c = ↑(unitCoeff h)
[PROOFSTEP]
obtain ⟨c, rfl⟩ : IsUnit c := by
  -- TODO: write a `CanLift` instance for units
  rw [Int.natAbs_eq_zero] at hc0
  rw [isUnit_iff, norm_eq_pow_val hc', hc0, neg_zero, zpow_zero]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ IsUnit c
[PROOFSTEP]
rw [Int.natAbs_eq_zero] at hc0
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : valuation c = 0
⊢ IsUnit c
[PROOFSTEP]
rw [isUnit_iff, norm_eq_pow_val hc', hc0, neg_zero, zpow_zero]
[GOAL]
case neg.intro.h.inl.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : Int.natAbs (valuation ↑c) = 0
⊢ ↑c = ↑(unitCoeff h)
[PROOFSTEP]
rw [DiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : Int.natAbs (valuation ↑c) = 0
⊢ Irreducible ↑p
[PROOFSTEP]
exact irreducible_p
[GOAL]
case neg.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
[PROOFSTEP]
rw [zero_pow hc0]
[GOAL]
case neg.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0)
[PROOFSTEP]
simp only [sub_zero, ZMod.cast_zero, mul_zero]
[GOAL]
case neg.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c
[PROOFSTEP]
rw [unitCoeff_spec hc']
[GOAL]
case neg.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ Int.natAbs (valuation c)
[PROOFSTEP]
exact (dvd_pow_self (p : ℤ_[p]) hc0.ne').mul_left _
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑((fun x => appr x n) x) ∈ Ideal.span {↑(p ^ n)}
[PROOFSTEP]
intros
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x✝ : ℤ_[p]
⊢ x✝ - ↑((fun x => appr x n) x✝) ∈ Ideal.span {↑(p ^ n)}
[PROOFSTEP]
rw [Nat.cast_pow]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x✝ : ℤ_[p]
⊢ x✝ - ↑((fun x => appr x n) x✝) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
exact appr_spec n _
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑(p ^ n)} → x - ↑b ∈ Ideal.span {↑(p ^ n)} → ↑a = ↑b
[PROOFSTEP]
intro x a b ha hb
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ ↑a = ↑b
[PROOFSTEP]
apply zmod_congr_of_sub_mem_span n x a b
[GOAL]
case ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ x - ↑a ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
simpa using ha
[GOAL]
case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ x - ↑b ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
simpa using hb
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}
[PROOFSTEP]
ext x
[GOAL]
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}
[PROOFSTEP]
rw [RingHom.mem_ker]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ ↑(toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
constructor
[GOAL]
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}
[PROOFSTEP]
intro h
[GOAL]
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}
[PROOFSTEP]
suffices x.appr n = 0 by
  convert appr_spec n x
  simp only [this, sub_zero, cast_zero]
[GOAL]
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}
[PROOFSTEP]
convert appr_spec n x
[GOAL]
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)
[PROOFSTEP]
simp only [this, sub_zero, cast_zero]
[GOAL]
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
[PROOFSTEP]
dsimp [toZModPow, toZModHom] at h
[GOAL]
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
[PROOFSTEP]
rw [ZMod.nat_cast_zmod_eq_zero_iff_dvd] at h
[GOAL]
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
[PROOFSTEP]
apply eq_zero_of_dvd_of_lt h (appr_lt _ _)
[GOAL]
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
[PROOFSTEP]
intro h
[GOAL]
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
[PROOFSTEP]
rw [← sub_zero x] at h
[GOAL]
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
[PROOFSTEP]
dsimp [toZModPow, toZModHom]
[GOAL]
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
[PROOFSTEP]
rw [zmod_congr_of_sub_mem_span n x _ 0 _ h, cast_zero]
[GOAL]
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}
[PROOFSTEP]
apply appr_spec
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m
[PROOFSTEP]
apply ZMod.ringHom_eq_of_ker_eq
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ RingHom.ker (RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n)) = RingHom.ker (toZModPow m)
[PROOFSTEP]
ext x
[GOAL]
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ x ∈ RingHom.ker (RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n)) ↔
    x ∈ RingHom.ker (toZModPow m)
[PROOFSTEP]
rw [RingHom.mem_ker, RingHom.mem_ker]
[GOAL]
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n)) x = 0 ↔ ↑(toZModPow m) x = 0
[PROOFSTEP]
simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]
[GOAL]
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑(toZModPow n) x) = 0 ↔ ↑(toZModPow m) x = 0
[PROOFSTEP]
simp only [toZModPow, toZModHom, RingHom.coe_mk]
[GOAL]
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑{ toOneHom := { toFun := fun x => ↑(appr x n), map_one' := (_ : (fun x => ↑(appr x n)) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ℤ_[p]),
                    OneHom.toFun { toFun := fun x => ↑(appr x n), map_one' := (_ : (fun x => ↑(appr x n)) 1 = 1) }
                        (x * y) =
                      OneHom.toFun { toFun := fun x => ↑(appr x n), map_one' := (_ : (fun x => ↑(appr x n)) 1 = 1) } x *
                        OneHom.toFun { toFun := fun x => ↑(appr x n), map_one' := (_ : (fun x => ↑(appr x n)) 1 = 1) }
                          y) }
          x) =
      0 ↔
    ↑{ toOneHom := { toFun := fun x => ↑(appr x m), map_one' := (_ : (fun x => ↑(appr x m)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ℤ_[p]),
                  OneHom.toFun { toFun := fun x => ↑(appr x m), map_one' := (_ : (fun x => ↑(appr x m)) 1 = 1) }
                      (x * y) =
                    OneHom.toFun { toFun := fun x => ↑(appr x m), map_one' := (_ : (fun x => ↑(appr x m)) 1 = 1) } x *
                      OneHom.toFun { toFun := fun x => ↑(appr x m), map_one' := (_ : (fun x => ↑(appr x m)) 1 = 1) }
                        y) }
        x =
      0
[PROOFSTEP]
dsimp
[GOAL]
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑↑(appr x n) = 0 ↔ ↑(appr x m) = 0
[PROOFSTEP]
rw [ZMod.cast_nat_cast (pow_dvd_pow p h), zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]
[GOAL]
case h.h.ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(appr x n) - ↑(appr x n) ∈ Ideal.span {↑p ^ m}
[PROOFSTEP]
rw [sub_self]
[GOAL]
case h.h.ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ 0 ∈ Ideal.span {↑p ^ m}
[PROOFSTEP]
apply Ideal.zero_mem _
[GOAL]
case h.h.hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(appr x n) - ↑(appr x m) ∈ Ideal.span {↑p ^ m}
[PROOFSTEP]
rw [Ideal.mem_span_singleton]
[GOAL]
case h.h.hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑p ^ m ∣ ↑(appr x n) - ↑(appr x m)
[PROOFSTEP]
rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩
[GOAL]
case h.h.hb.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : appr x n - appr x m = p ^ m * c
⊢ ↑p ^ m ∣ ↑(appr x n) - ↑(appr x m)
[PROOFSTEP]
use c
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : appr x n - appr x m = p ^ m * c
⊢ ↑(appr x n) - ↑(appr x m) = ↑p ^ m * ↑c
[PROOFSTEP]
rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑(toZModPow n) x) = ↑(toZModPow m) x
[PROOFSTEP]
rw [← zmod_cast_comp_toZModPow _ _ h]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑(toZModPow n) x) = ↑(RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n)) x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ DenseRange Nat.cast
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ closure (Set.range Nat.cast)
[PROOFSTEP]
rw [Metric.mem_closure_range_iff]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (ε : ℝ), ε > 0 → ∃ k, dist x ↑k < ε
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
ε : ℝ
hε : ε > 0
⊢ ∃ k, dist x ↑k < ε
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ k, dist x ↑k < ε
[PROOFSTEP]
use x.appr n
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist x ↑(appr x n) < ε
[PROOFSTEP]
rw [dist_eq_norm]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(appr x n)‖ < ε
[PROOFSTEP]
apply lt_of_le_of_lt _ hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(appr x n)‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
rw [norm_le_pow_iff_mem_span_pow]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ x - ↑(appr x n) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
apply appr_spec
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ DenseRange Int.cast
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ closure (Set.range Int.cast)
[PROOFSTEP]
refine DenseRange.induction_on denseRange_nat_cast x ?_ ?_
[GOAL]
case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}
[PROOFSTEP]
exact isClosed_closure
[GOAL]
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)
[PROOFSTEP]
intro a
[GOAL]
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ closure (Set.range Int.cast)
[PROOFSTEP]
apply subset_closure
[GOAL]
case refine_2.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ Set.range Int.cast
[PROOFSTEP]
exact Set.mem_range_self _
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
⊢ nthHom f 0 = 0
[PROOFSTEP]
simp [nthHom]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
⊢ (fun n => 0) = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
i j : ℕ
h : i ≤ j
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i
[PROOFSTEP]
specialize f_compat i j h
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i
[PROOFSTEP]
rw [← Int.coe_nat_pow, ← ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.cast_sub]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0
[PROOFSTEP]
dsimp [nthHom]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑↑(ZMod.val (↑(f j) r)) - ↑↑(ZMod.val (↑(f i) r)) = 0
[PROOFSTEP]
rw [← f_compat, RingHom.comp_apply]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑↑(ZMod.val (↑(f j) r)) - ↑↑(ZMod.val (↑(ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (↑(f j) r))) = 0
[PROOFSTEP]
simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.nat_cast_val, ZMod.int_cast_cast]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
⊢ IsCauSeq (padicNorm p) fun n => ↑(nthHom f r n)
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) i) < ε
[PROOFSTEP]
obtain ⟨k, hk⟩ : ∃ k : ℕ, (p : ℚ) ^ (-((k : ℕ) : ℤ)) < ε := exists_pow_neg_lt_rat p hε
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) i) < ε
[PROOFSTEP]
use k
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∀ (j : ℕ), j ≥ k → padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) k) < ε
[PROOFSTEP]
intro j hj
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) k) < ε
[PROOFSTEP]
refine' lt_of_le_of_lt _ hk
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) k) ≤ ↑p ^ (-↑k)
[PROOFSTEP]
norm_cast
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p ↑(nthHom f r j - nthHom f r k) ≤ ↑p ^ (-↑k)
[PROOFSTEP]
rw [← padicNorm.dvd_iff_norm_le]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ ↑(p ^ k) ∣ nthHom f r j - nthHom f r k
[PROOFSTEP]
exact_mod_cast pow_dvd_nthHom_sub f_compat r k j hj
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
⊢ nthHomSeq f_compat 1 ≈ 1
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
[PROOFSTEP]
change _ < _ at hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
[PROOFSTEP]
use 1
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
⊢ ∀ (j : ℕ), j ≥ 1 → padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
[PROOFSTEP]
intro j hj
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
[PROOFSTEP]
haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow _ _ (by linarith) hp_prime.1.one_lt⟩
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ 0 < j
[PROOFSTEP]
linarith
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
[PROOFSTEP]
suffices ((1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this✝ : Fact (1 < p ^ j)
this : ↑1 = 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
[PROOFSTEP]
simp [nthHomSeq, nthHom, this, hε]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ ↑1 = 1
[PROOFSTEP]
rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
⊢ nthHomSeq f_compat (r + s) ≈ nthHomSeq f_compat r + nthHomSeq f_compat s
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i,
    ∀ (j : ℕ), j ≥ i → padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ i,
    ∀ (j : ℕ), j ≥ i → padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
[PROOFSTEP]
use n
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∀ (j : ℕ), j ≥ n → padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
[PROOFSTEP]
intro j hj
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
[PROOFSTEP]
dsimp [nthHomSeq]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p
      (↑(nthHom (fun k2 => f k2) (r + s) j) - (↑(nthHom (fun k2 => f k2) r j) + ↑(nthHom (fun k2 => f k2) s j))) <
    ε
[PROOFSTEP]
apply lt_of_le_of_lt _ hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p
      (↑(nthHom (fun k2 => f k2) (r + s) j) - (↑(nthHom (fun k2 => f k2) r j) + ↑(nthHom (fun k2 => f k2) s j))) ≤
    ↑p ^ (-↑n)
[PROOFSTEP]
rw [← Int.cast_add, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ← ZMod.int_cast_zmod_eq_zero_iff_dvd]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(nthHom (fun k2 => f k2) (r + s) j - (nthHom (fun k2 => f k2) r j + nthHom (fun k2 => f k2) s j)) = 0
[PROOFSTEP]
dsimp [nthHom]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑(ZMod.val (↑(f j) (r + s))) - ↑(ZMod.val (↑(f j) r) + ZMod.val (↑(f j) s))) = 0
[PROOFSTEP]
simp only [ZMod.nat_cast_val, RingHom.map_add, Int.cast_sub, ZMod.int_cast_cast, Int.cast_add]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑(f j) r + ↑(f j) s) - ↑↑(ZMod.val (↑(f j) r) + ZMod.val (↑(f j) s)) = 0
[PROOFSTEP]
rw [ZMod.cast_add (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj)]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑(f j) r) + ↑(↑(f j) s) - ↑↑(ZMod.val (↑(f j) r) + ZMod.val (↑(f j) s)) = 0
[PROOFSTEP]
simp only [cast_add, ZMod.nat_cast_val, Int.cast_add, ZMod.int_cast_cast, sub_self]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
⊢ nthHomSeq f_compat (r * s) ≈ nthHomSeq f_compat r * nthHomSeq f_compat s
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i,
    ∀ (j : ℕ), j ≥ i → padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ i,
    ∀ (j : ℕ), j ≥ i → padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
[PROOFSTEP]
use n
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∀ (j : ℕ), j ≥ n → padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
[PROOFSTEP]
intro j hj
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
[PROOFSTEP]
dsimp [nthHomSeq]
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom (fun k2 => f k2) (r * s) j) - ↑(nthHom (fun k2 => f k2) r j) * ↑(nthHom (fun k2 => f k2) s j)) <
    ε
[PROOFSTEP]
apply lt_of_le_of_lt _ hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom (fun k2 => f k2) (r * s) j) - ↑(nthHom (fun k2 => f k2) r j) * ↑(nthHom (fun k2 => f k2) s j)) ≤
    ↑p ^ (-↑n)
[PROOFSTEP]
rw [← Int.cast_mul, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ← ZMod.int_cast_zmod_eq_zero_iff_dvd]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(nthHom (fun k2 => f k2) (r * s) j - nthHom (fun k2 => f k2) r j * nthHom (fun k2 => f k2) s j) = 0
[PROOFSTEP]
dsimp [nthHom]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑(ZMod.val (↑(f j) (r * s))) - ↑(ZMod.val (↑(f j) r)) * ↑(ZMod.val (↑(f j) s))) = 0
[PROOFSTEP]
simp only [ZMod.nat_cast_val, RingHom.map_mul, Int.cast_sub, ZMod.int_cast_cast, Int.cast_mul]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑(f j) r * ↑(f j) s) - ↑(↑(f j) r) * ↑(↑(f j) s) = 0
[PROOFSTEP]
rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
obtain ⟨ε', hε'0, hε'⟩ : ∃ v : ℚ, (0 : ℝ) < v ∧ ↑v < ε := exists_rat_btwn hε
[GOAL]
case intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'0 : 0 < ↑ε'
hε' : ↑ε' < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
norm_cast at hε'0
[GOAL]
case intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0
[GOAL]
case intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
use N
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
intro n hn
[GOAL]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
[PROOFSTEP]
apply _root_.lt_trans _ hε'
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ↑ε'
[PROOFSTEP]
change (padicNormE _ : ℝ) < _
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑(↑padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n))) < ↑ε'
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n)) < ε'
[PROOFSTEP]
exact hN _ hn
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
⊢ limNthHom f_compat 0 = 0
[PROOFSTEP]
simp [limNthHom]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
⊢ ofIntSeq 0 (_ : IsCauSeq (padicNorm p) fun n => ↑(OfNat.ofNat 0 n)) = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n : ℕ
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
obtain ⟨k, hk⟩ :=
  limNthHom_spec f_compat r _ (show (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) from Nat.zpow_pos_of_pos hp_prime.1.pos _)
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
have := le_of_lt (hk (max n k) (le_max_right _ _))
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k))‖ ≤ ↑p ^ (-↑n)
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
rw [norm_le_pow_iff_mem_span_pow] at this
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
dsimp [lift]
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ limNthHom f_compat r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
rw [sub_eq_sub_add_sub (limNthHom f_compat r) _ ↑(nthHom f r (max n k))]
[GOAL]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑(ZMod.val (↑(f n) r)) + (limNthHom f_compat r - ↑(nthHom f r (max n k))) ∈
    Ideal.span {↑p ^ n}
[PROOFSTEP]
apply Ideal.add_mem _ _ this
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
rw [Ideal.mem_span_singleton]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n ∣ ↑(nthHom f r (max n k)) - ↑(ZMod.val (↑(f n) r))
[PROOFSTEP]
convert (Int.castRingHom ℤ_[p]).map_dvd (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))
[GOAL]
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n = ↑(Int.castRingHom ℤ_[p]) (↑p ^ n)
[PROOFSTEP]
rw [map_pow]
[GOAL]
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n = ↑(Int.castRingHom ℤ_[p]) ↑p ^ n
[PROOFSTEP]
rfl
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑(ZMod.val (↑(f n) r)) =
    ↑(Int.castRingHom ℤ_[p]) (nthHom (fun k2 => f k2) r (max n k) - nthHom (fun k2 => f k2) r n)
[PROOFSTEP]
rw [map_sub]
[GOAL]
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
n k : ℕ
hk : ∀ (n_1 : ℕ), n_1 ≥ k → ‖limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom (fun k2 => f k2) r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑(ZMod.val (↑(f n) r)) =
    ↑(Int.castRingHom ℤ_[p]) (nthHom (fun k2 => f k2) r (max n k)) -
      ↑(Int.castRingHom ℤ_[p]) (nthHom (fun k2 => f k2) r n)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
⊢ RingHom.comp (toZModPow n) (lift f_compat) = f n
[PROOFSTEP]
ext r
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
r : R
⊢ ↑(RingHom.comp (toZModPow n) (lift f_compat)) r = ↑(f n) r
[PROOFSTEP]
rw [RingHom.comp_apply, ← ZMod.nat_cast_zmod_val (f n r), ← map_natCast <| toZModPow n, ← sub_eq_zero, ←
  RingHom.map_sub, ← RingHom.mem_ker, ker_toZModPow]
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
r : R
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
apply lift_sub_val_mem_span
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
⊢ lift f_compat = g
[PROOFSTEP]
ext1 r
[GOAL]
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ ↑(lift f_compat) r = ↑g r
[PROOFSTEP]
apply eq_of_forall_dist_le
[GOAL]
case a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ ∀ (ε : ℝ), ε > 0 → dist (↑(lift f_compat) r) (↑g r) ≤ ε
[PROOFSTEP]
intro ε hε
[GOAL]
case a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ε
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
[GOAL]
case a.h.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ε
[PROOFSTEP]
apply le_trans _ (le_of_lt hn)
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ↑p ^ (-↑n)
[PROOFSTEP]
rw [dist_eq_norm, norm_le_pow_iff_mem_span_pow, ← ker_toZModPow, RingHom.mem_ker, RingHom.map_sub, ← RingHom.comp_apply,
  ← RingHom.comp_apply, lift_spec, hg, sub_self]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
z : ℤ_[p]
⊢ ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      z =
    z
[PROOFSTEP]
show _ = RingHom.id _ z
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
z : ℤ_[p]
⊢ ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      z =
    ↑(RingHom.id ℤ_[p]) z
[PROOFSTEP]
rw [@lift_unique p _ ℤ_[p] _ _ zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
z : ℤ_[p]
⊢ ∀ (n : ℕ), RingHom.comp (toZModPow n) (RingHom.id ℤ_[p]) = toZModPow n
[PROOFSTEP]
intro
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
z : ℤ_[p]
n✝ : ℕ
⊢ RingHom.comp (toZModPow n✝) (RingHom.id ℤ_[p]) = toZModPow n✝
[PROOFSTEP]
rw [RingHom.comp_id]
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y) ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y) → x = y
[PROOFSTEP]
intro h
[GOAL]
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
⊢ x = y
[PROOFSTEP]
rw [← lift_self x, ← lift_self y]
[GOAL]
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
⊢ ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      x =
    ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      y
[PROOFSTEP]
simp [lift, limNthHom, nthHom, h]
[GOAL]
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
[PROOFSTEP]
rintro rfl _
[GOAL]
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n✝ : ℕ
⊢ ↑(toZModPow n✝) x = ↑(toZModPow n✝) x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') ↔ g = g'
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') → g = g'
[PROOFSTEP]
intro hg
[GOAL]
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
⊢ g = g'
[PROOFSTEP]
ext x : 1
[GOAL]
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ ↑g x = ↑g' x
[PROOFSTEP]
apply ext_of_toZModPow.mp
[GOAL]
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ ∀ (n : ℕ), ↑(toZModPow n) (↑g x) = ↑(toZModPow n) (↑g' x)
[PROOFSTEP]
intro n
[GOAL]
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
n : ℕ
⊢ ↑(toZModPow n) (↑g x) = ↑(toZModPow n) (↑g' x)
[PROOFSTEP]
show (toZModPow n).comp g x = (toZModPow n).comp g' x
[GOAL]
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
n : ℕ
⊢ ↑(RingHom.comp (toZModPow n) g) x = ↑(RingHom.comp (toZModPow n) g') x
[PROOFSTEP]
rw [hg n]
[GOAL]
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ g = g' → ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
[PROOFSTEP]
rintro rfl _
[GOAL]
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g : R →+* ℤ_[p]
n✝ : ℕ
⊢ RingHom.comp (toZModPow n✝) g = RingHom.comp (toZModPow n✝) g
[PROOFSTEP]
rfl