case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y) → x = y

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y) ↔ x = y
constructor
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
⊢ x = y
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y) → x = y
intro h
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
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
⊢ x = y
rw [← lift_self x, ← lift_self y]
no goals
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
simp [lift, limNthHom, nthHom, h]
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n✝ : ℕ
⊢ ↑(toZModPow n✝) x = ↑(toZModPow n✝) x
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), ↑(toZModPow n) x = ↑(toZModPow n) y
rintro rfl _
no goals
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n✝ : ℕ
⊢ ↑(toZModPow n✝) x = ↑(toZModPow n✝) x
rfl