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
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ maximalIdeal ℤ_[p]
hn : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ↑m = ↑n
rw [maximalIdeal_eq_span_p] at hm hn
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
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
have := zmod_congr_of_sub_mem_span_aux 1 x m n
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
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
simp only [pow_one] at this
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
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
specialize this hm hn
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
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
apply_fun ZMod.castHom (show p ∣ p ^ 1 by rw [pow_one]) (ZMod p)  at this
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
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
simp only [map_intCast] at this
no goals
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
simpa only [Int.cast_ofNat] using this
no goals
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
rw [pow_one]