awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
⊢ Membership.mem (γ := Set ℤ_[p])
    (⋃ (y : ℤ_[p]), ⋃ (_ : Membership.mem (γ := Set ℤ_[p]) (Nat.cast '' (↑(Finset.range (p ^ k)) : Set ℕ)) y), ball y ε)
    z
have simp : ∃ x ∈ (↑(Finset.range (p ^ k)) : Set ℕ), dist z (↑x : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε
Tactic: simp only [PadicInt, Set.mem_iUnion, Metric.mem_ball, exists_prop, Set.exists_mem_image]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
⊢ ∃ x ∈ (↑(Finset.range (p ^ k)) : Set ℕ), dist z (↑x : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε
have refine_1 : z.appr k ∈ (↑(Finset.range (p ^ k)) : Set ℕ)
Tactic: refine ⟨z.appr k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
refine_1 : z.appr k ∈ (↑(Finset.range (p ^ k)) : Set ℕ)
⊢ ∃ x ∈ (↑(Finset.range (p ^ k)) : Set ℕ), dist z (↑x : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε
have refine_2 : dist z (↑(z.appr k) : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε
Tactic: refine ⟨z.appr k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ CompactSpace ℤ_[p]
have rw : TotallyBounded (α := ℤ_[p]) Set.univ ∧ IsComplete (α := ℤ_[p]) Set.univ
Tactic: rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ ProperSpace ℚ_[p]
have suffices : LocallyCompactSpace ℚ_[p]
Tactic: suffices LocallyCompactSpace ℚ_[p] from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ LocallyCompactSpace ℚ_[p]
have this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) (closedBall 0 1)
Tactic: have : closedBall 0 1 ∈ 𝓝 (0 : ℚ_[p]) := closedBall_mem_nhds _ zero_lt_one
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) (closedBall 0 1)
⊢ LocallyCompactSpace ℚ_[p]
have this₁ : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) {y : ℚ_[p] | ‖y‖ ≤ 1}
Tactic: simp only [closedBall, dist_eq_norm_sub, sub_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) {y : ℚ_[p] | ‖y‖ ≤ 1}
⊢ LocallyCompactSpace ℚ_[p]
have refine : IsCompact (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}
Tactic: refine IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup ?_ this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ modPart p r < (↑p : ℤ)
have h : Eq (α := ℤ) (↑p : ℤ) |(↑p : ℤ)|
Tactic: convert! Int.emod_lt_abs _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : Eq (α := ℤ) (↑p : ℤ) |(↑p : ℤ)|
⊢ modPart p r < (↑p : ℤ)
have convert_3 : Ne (α := ℤ) (↑p : ℤ) 0
Tactic: convert! Int.emod_lt_abs _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
⊢ (↑p : ℤ) ∣ r.num - r.num * r.den.gcdA p % (↑p : ℤ) * (↑r.den : ℤ)
have rw : Eq (α := ZMod p) (↑(r.num - r.num * r.den.gcdA p % (↑p : ℤ) * (↑r.den : ℤ)) : ZMod p) 0
Tactic: rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
⊢ Eq (α := ZMod p) (↑(r.num - r.num * r.den.gcdA p % (↑p : ℤ) * (↑r.den : ℤ)) : ZMod p) 0
have simp : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑(r.num * r.den.gcdA p % (↑p : ℤ)) : ZMod p) (↑r.den : ZMod p) = 0
Tactic: simp only [Int.cast_natCast, Int.cast_mul, Int.cast_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑(r.num * r.den.gcdA p % (↑p : ℤ)) : ZMod p) (↑r.den : ZMod p) = 0
have this : Eq (α := ZMod p) ((fun (x : ℤ) ↦ HMod.hMod (α := ZMod p) (↑x : ZMod p) (↑p : ZMod p)) (↑(r.den.gcd p) : ℤ))
  ((fun (x : ℤ) ↦ HMod.hMod (α := ZMod p) (↑x : ZMod p) (↑p : ZMod p))
    ((↑r.den : ℤ) * r.den.gcdA p + (↑p : ℤ) * r.den.gcdB p))
Tactic: have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this :
  Eq (α := ZMod p) ((fun (x : ℤ) ↦ HMod.hMod (α := ZMod p) (↑x : ZMod p) (↑p : ZMod p)) (↑(r.den.gcd p) : ℤ))
    ((fun (x : ℤ) ↦ HMod.hMod (α := ZMod p) (↑x : ZMod p) (↑p : ZMod p))
      ((↑r.den : ℤ) * r.den.gcdA p + (↑p : ℤ) * r.den.gcdB p))
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑(r.num * r.den.gcdA p % (↑p : ℤ)) : ZMod p) (↑r.den : ZMod p) = 0
have this₁ : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
Tactic: simp only [Int.cast_natCast, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add,
    Int.cast_mul, zero_mul, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑(r.num * r.den.gcdA p % (↑p : ℤ)) : ZMod p) (↑r.den : ZMod p) = 0
have push_cast : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcdA p) : ZMod p) * (↑r.den : ZMod p) = 0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcdA p) : ZMod p) * (↑r.den : ZMod p) = 0
have rw : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcd p) : ZMod p) = 0
Tactic: rw [mul_right_comm, mul_assoc, ← this]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
rdcp : r.den.Coprime p
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcd p) : ZMod p) = 0
have rw : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑1 : ZMod p) = 0
Tactic: rw [rdcp.gcd_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcd p) : ZMod p) = 0
have suffices : r.den.Coprime p
Tactic: suffices rdcp : r.den.Coprime p by
    rw [rdcp.gcd_eq_one]
    simp only [mul_one, cast_one, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ r.den.Coprime p
have a : p.Coprime r.den
Tactic: apply Coprime.symm
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ p.Coprime r.den
have a : ¬p ∣ r.den
Tactic: apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ ¬p ∣ r.den
have a : 1 ≤ norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])
Tactic: rw [← Int.natCast_dvd_natCast, ← norm_int_lt_one_iff_dvd, not_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ 1 ≤ norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])
have a : norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p]) = 1
Tactic: apply ge_of_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
this : (↑(r.den.gcd p) : ZMod p) = HMul.hMul (α := ZMod p) (↑r.den : ZMod p) (↑(r.den.gcdA p) : ZMod p)
⊢ norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p]) = 1
have a : IsUnit (M := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])
Tactic: rw [← isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
⊢ ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])‖ < 1
have rw : (↑p : ℤ_[p]) ∣
  (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p])
Tactic: rw [norm_lt_one_iff_dvd, ← (isUnit_den r h).dvd_mul_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
this : (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)
⊢ (↑p : ℤ_[p]) ∣
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p])
have h₁ : (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p]) =
  (Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (r.num - n * (↑r.den : ℤ))
Tactic: convert! (map_dvd (Int.castRingHom ℤ_[p])) this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
this : (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)
⊢ (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p]) =
    (Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (r.num - n * (↑r.den : ℤ))
have h₁ : Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h * (↑r.den : ℤ_[p]) = (↑r.num : ℤ_[p])
Tactic: simp only [n, sub_mul, Int.cast_natCast, eq_intCast, Int.cast_mul, sub_left_inj,
      Int.cast_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
this : (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)
⊢ Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h * (↑r.den : ℤ_[p]) = (↑r.num : ℤ_[p])
have h₁ : Eq (α := ℚ_[p])
  ((fun (a : { x : ℚ_[p] // ‖x‖ ≤ 1 }) ↦ (↑a : ℚ_[p]))
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h * (↑r.den : ℤ_[p])))
  ((fun (a : { x : ℚ_[p] // ‖x‖ ≤ 1 }) ↦ (↑a : ℚ_[p])) (↑r.num : ℤ_[p]))
Tactic: apply Subtype.coe_injective
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
this : (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)
⊢ HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p]) = (↑(↑r.num : ℤ_[p]) : ℚ_[p])
have h₁ : Eq (α := ℚ_[p]) (↑(r * (↑r.den : ℚ)) : ℚ_[p]) (↑r.num : ℚ_[p])
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
⊢ (↑p : ℤ_[p]) ∣
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p])
have suffices : (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)
Tactic: suffices ↑p ∣ r.num - n * r.den by
    convert! (map_dvd (Int.castRingHom ℤ_[p])) this
    simp only [n, sub_mul, Int.cast_natCast, eq_intCast, Int.cast_mul, sub_left_inj,
      Int.cast_sub]
    apply Subtype.coe_injective
    simp only [coe_mul, coe_natCast]
    norm_cast
    simp
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑b : ℤ_[p]))
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))
have ha₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑a : ℤ_[p])
Tactic: rw [Ideal.mem_span_singleton] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑b : ℤ_[p]))
ha₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑a : ℤ_[p])
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))
have hb₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
Tactic: rw [Ideal.mem_span_singleton] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑a : ℤ_[p])
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))
have rw : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑a : ℤ_[p])
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have ha₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
Tactic: rw [← dvd_neg, neg_sub] at ha
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
Tactic: have := dvd_add ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
  HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
rwa :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa₁ : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x + -(↑b : ℤ_[p]))),
  HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
rwa :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₁ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x + -(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa₂ : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + (-x + (x + -(↑b : ℤ_[p])))),
  HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
rwa :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₁ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x + -(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₂ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + (-x + (x + -(↑b : ℤ_[p])))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa₃ : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HAdd.hAdd (α := ℤ_[p]) (↑a : ℤ_[p]) (-(↑b : ℤ_[p]))),
  HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
rwa :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₁ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x + -(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₂ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + (-x + (x + -(↑b : ℤ_[p])))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₃ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HAdd.hAdd (α := ℤ_[p]) (↑a : ℤ_[p]) (-(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa₄ : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HSub.hSub (α := ℤ_[p]) (↑a : ℤ_[p]) (↑b : ℤ_[p])),
  HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
rwa :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₁ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x + -(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₂ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + (-x + (x + -(↑b : ℤ_[p])))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₃ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HAdd.hAdd (α := ℤ_[p]) (↑a : ℤ_[p]) (-(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₄ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HSub.hSub (α := ℤ_[p]) (↑a : ℤ_[p]) (↑b : ℤ_[p])),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa₅ : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑(a - b) : ℤ_[p])), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
hb : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])
this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))
rwa :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x - (↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₁ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + -x + (x + -(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₂ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) + (-x + (x + -(↑b : ℤ_[p])))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₃ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HAdd.hAdd (α := ℤ_[p]) (↑a : ℤ_[p]) (-(↑b : ℤ_[p]))),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₄ :
  ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ HSub.hSub (α := ℤ_[p]) (↑a : ℤ_[p]) (↑b : ℤ_[p])),
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
rwa₅ : ∀ (this : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑(a - b) : ℤ_[p])), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
have rwa₆ : ∀ (this : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
Tactic: 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] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
⊢ Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)
have hm₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
Tactic: rw [maximalIdeal_eq_span_p] at hm hn
Cleared hypotheses: hm, hn