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)
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
apply ZMod.ringHom_eq_of_ker_eq
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)
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)
ext x
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
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)
rw [RingHom.mem_ker, RingHom.mem_ker]
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
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
simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]
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
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
simp only [toZModPow, toZModHom, RingHom.coe_mk]
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
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
dsimp
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}

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}
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
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)]
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}
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}
rw [sub_self]
no goals
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}
apply Ideal.zero_mem _
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)
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}
rw [Ideal.mem_span_singleton]
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)
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)
rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩
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
⊢ ↑(appr x n) - ↑(appr x m) = ↑p ^ m * ↑c
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)
use c
no goals
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
⊢ ↑(appr x n) - ↑(appr x m) = ↑p ^ m * ↑c
rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]