awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
simp : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑(r.num * r.den.gcdA p % (↑p : ℤ)) : ZMod p) (↑r.den : ZMod p) = 0
⊢ Eq (α := ZMod p) (↑(r.num - r.num * r.den.gcdA p % (↑p : ℤ) * (↑r.den : ℤ)) : ZMod p) 0

Tactic:
simp only [Int.cast_natCast, Int.cast_mul, Int.cast_sub]

Premises used: Int.cast_natCast, Int.cast_sub, Int.cast_mul
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
⊢ 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)
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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.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

Premises used: CharP.cast_eq_zero, Int.cast_natCast, EuclideanDomain.mod_zero, MulZeroClass.zero_mul, Int.cast_add, Int.cast_mul, add_zero
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
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
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑(r.num * r.den.gcdA p % (↑p : ℤ)) : ZMod p) (↑r.den : ZMod p) = 0

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
rw : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcd p) : ZMod p) = 0
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcdA p) : ZMod p) * (↑r.den : ZMod p) = 0

Tactic:
rw [mul_right_comm, mul_assoc, ← this]

Premises used: mul_assoc, mul_right_comm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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
rw : (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑1 : ZMod p) = 0
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcd p) : ZMod p) = 0

Tactic:
rw [rdcp.gcd_eq_one]

Premises used: Nat.Coprime.gcd_eq_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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) (↑1 : ZMod p) = 0

Tactic:
simp only [mul_one, cast_one, sub_self]

Premises used: sub_self, mul_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
suffices : r.den.Coprime p
⊢ (↑r.num : ZMod p) - HMul.hMul (α := ZMod p) (↑r.num : ZMod p) (↑(r.den.gcd p) : ZMod p) = 0

Tactic:
suffices rdcp : r.den.Coprime p by
    rw [rdcp.gcd_eq_one]
    simp only [mul_one, cast_one, sub_self]
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
a : p.Coprime r.den
⊢ r.den.Coprime p

Tactic:
apply Coprime.symm

Premises used: Nat.Coprime.symm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
a : ¬p ∣ r.den
⊢ p.Coprime r.den

Tactic:
apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right

Premises used: Or.resolve_right, Nat.coprime_or_dvd_of_prime, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
a : 1 ≤ norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])
⊢ ¬p ∣ r.den

Tactic:
rw [← Int.natCast_dvd_natCast, ← norm_int_lt_one_iff_dvd, not_lt]

Premises used: PadicInt.norm_int_lt_one_iff_dvd, not_lt, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
a : norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p]) = 1
⊢ 1 ≤ norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])

Tactic:
apply ge_of_eq

Premises used: ge_of_eq
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
a : IsUnit (M := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])
⊢ norm (E := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p]) = 1

Tactic:
rw [← isUnit_iff]

Premises used: PadicInt.isUnit_iff
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
⊢ IsUnit (M := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])

Tactic:
isUnit_den r h

Premises used: PadicInt.isUnit_den
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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)
⊢ IsUnit (M := ℤ_[p]) (↑(↑r.den : ℤ) : ℤ_[p])

Tactic:
exact isUnit_den r h

Premises used: PadicInt.isUnit_den
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
rw :
  (↑p : ℤ_[p]) ∣
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p])
⊢ ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])‖ < 1

Tactic:
rw [norm_lt_one_iff_dvd, ← (isUnit_den r h).dvd_mul_right]

Premises used: PadicInt.norm_lt_one_iff_dvd, PadicInt.isUnit_den, IsUnit.dvd_mul_right
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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 : ℤ)
⊢ Dvd.dvd (α := ℤ_[p]) ((Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (↑p : ℤ) : ℤ_[p])
    ((Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (r.num - n * (↑r.den : ℤ)) : ℤ_[p])

Tactic:
(map_dvd (Int.castRingHom ℤ_[p])) this

Premises used: PadicInt, map_dvd, Int.castRingHom
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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 : ℤ)
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 : ℤ))
⊢ (↑p : ℤ_[p]) ∣
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑(modPart p r) : ℤ_[p])) * (↑r.den : ℤ_[p])

Tactic:
convert! (map_dvd (Int.castRingHom ℤ_[p])) this

Premises used: PadicInt, map_dvd, Int.castRingHom
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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 : ℤ)
h₁ : Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h * (↑r.den : ℤ_[p]) = (↑r.num : ℤ_[p])
⊢ (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:
simp only [n, sub_mul, Int.cast_natCast, eq_intCast, Int.cast_mul, sub_left_inj,
      Int.cast_sub]

Premises used: Int.cast_natCast, Int.cast_sub, sub_left_inj, eq_intCast, sub_mul, Int.cast_mul
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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 : ℤ)
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]))
⊢ Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h * (↑r.den : ℤ_[p]) = (↑r.num : ℤ_[p])

Tactic:
apply Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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 : ℤ)
h₁ : Eq (α := ℚ_[p]) (↑(r * (↑r.den : ℚ)) : ℚ_[p]) (↑r.num : ℚ_[p])
⊢ HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p]) = (↑(↑r.num : ℤ_[p]) : ℚ_[p])

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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 : ℤ)
⊢ Eq (α := ℚ_[p]) (↑(r * (↑r.den : ℚ)) : ℚ_[p]) (↑r.num : ℚ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
suffices : (↑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])

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
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
⊢ (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)

Tactic:
norm_sub_modPart_aux r h

Premises used: PadicInt.modPart, PadicInt.norm_sub_modPart_aux
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ := modPart p r
⊢ (↑p : ℤ) ∣ r.num - n * (↑r.den : ℤ)

Tactic:
exact norm_sub_modPart_aux r h

Premises used: PadicInt.norm_sub_modPart_aux
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
⊢ ∃ (n : ℤ), 0 ≤ n ∧ n < (↑p : ℤ) ∧ ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) h - (↑n : ℤ_[p])‖ < 1

Tactic:
⟨modPart p r, modPart_nonneg _, modPart_lt_p _, norm_sub_modPart _ h⟩

Premises used: PadicInt.modPart_nonneg, PadicInt.modPart_lt_p, PadicInt.modPart, And.intro, PadicInt.norm_sub_modPart, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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]))
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑a : ℤ_[p])

Tactic:
rw [Ideal.mem_span_singleton] at ha hb

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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])
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])

Tactic:
rw [Ideal.mem_span_singleton] at ha hb

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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])
rw : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))

Tactic:
rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natCast_pow]

Premises used: sub_eq_zero, Int.cast_sub, Int.natCast_pow, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x

Tactic:
rw [← dvd_neg, neg_sub] at ha

Premises used: neg_sub, dvd_neg
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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])
ha₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑b : ℤ_[p])

Tactic:
rw [← dvd_neg, neg_sub] at ha

Premises used: neg_sub, dvd_neg
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) - x + (x - (↑b : ℤ_[p]))

Tactic:
have := dvd_add ha hb
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (this : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a - b), 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

Premises used: Int.cast_sub, add_assoc, sub_eq_add_neg, PadicInt.pow_p_dvd_int_iff, neg_add_cancel_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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))

Tactic:
simpa using zmod_congr_of_sub_mem_span_aux n x a b ha hb

Premises used: Nat.cast, PadicInt.zmod_congr_of_sub_mem_span_aux
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))

Tactic:
rw [maximalIdeal_eq_span_p] at hm hn

Premises used: PadicInt.maximalIdeal_eq_span_p
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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]))
hm₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))

Tactic:
rw [maximalIdeal_eq_span_p] at hm hn

Premises used: PadicInt.maximalIdeal_eq_span_p
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
⊢ ∀
    (ha :
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1})
        (x - (↑(↑m : ℤ) : ℤ_[p])))
    (hb :
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1})
        (x - (↑(↑n : ℤ) : ℤ_[p]))),
    Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))

Tactic:
have := zmod_congr_of_sub_mem_span_aux 1 x m n
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
this :
  ∀
    (ha :
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1})
        (x - (↑(↑m : ℤ) : ℤ_[p])))
    (hb :
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1})
        (x - (↑(↑n : ℤ) : ℤ_[p]))),
    Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))
⊢ ∀ (ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑(↑m : ℤ) : ℤ_[p])))
    (hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑(↑n : ℤ) : ℤ_[p]))),
    Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))

Tactic:
simp only [pow_one] at this

Premises used: pow_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
this :
  ∀ (ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑(↑m : ℤ) : ℤ_[p])))
    (hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑(↑n : ℤ) : ℤ_[p]))),
    Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))
⊢ Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))

Tactic:
specialize this hm hn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
this : Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))
rw rw₁ : p ∣ p
⊢ p ∣ HPow.hPow (β := ℕ) p 1

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
this : Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))
⊢ Eq (α := ZMod p) ((ZMod.castHom ⋯ (ZMod p) : (a : ZMod (p ^ 1)) → ZMod p) (↑(↑m : ℤ) : ZMod (p ^ 1)))
    ((ZMod.castHom ⋯ (ZMod p) : (a : ZMod (p ^ 1)) → ZMod p) (↑(↑n : ℤ) : ZMod (p ^ 1)))

Tactic:
apply_fun ZMod.castHom (show p ∣ p ^ 1 by rw [pow_one]) (ZMod p) at this

Premises used: ZMod, ZMod.castHom
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
this :
  Eq (α := ZMod p) ((ZMod.castHom ⋯ (ZMod p) : (a : ZMod (p ^ 1)) → ZMod p) (↑(↑m : ℤ) : ZMod (p ^ 1)))
    ((ZMod.castHom ⋯ (ZMod p) : (a : ZMod (p ^ 1)) → ZMod p) (↑(↑n : ℤ) : ZMod (p ^ 1)))
⊢ Eq (α := ZMod p) (↑(↑m : ℤ) : ZMod p) (↑(↑n : ℤ) : ZMod p)

Tactic:
simp only [map_intCast] at this

Premises used: map_intCast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
this : Eq (α := ZMod p) (↑(↑m : ℤ) : ZMod p) (↑(↑n : ℤ) : ZMod p)
⊢ Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)

Tactic:
simpa only [Int.cast_natCast] using this

Premises used: Int.cast_natCast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
simp : ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
⊢ ∃ n < p, Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))

Tactic:
simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]

Premises used: PadicInt.maximalIdeal_eq_span_p, PadicInt.norm_lt_one_iff_dvd, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
obtain : ∀ (r : ℚ) (hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1), ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1

Tactic:
obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one

Premises used: zero_lt_one, Padic.rat_dense, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
⊢ ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ < 1

Tactic:
rw [norm_sub_rev] at hr

Premises used: norm_sub_rev
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ < 1
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) = ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p]) + (↑x : ℚ_[p])‖

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ < 1
⊢ ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p]) + (↑x : ℚ_[p])‖ ≤ max ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ ‖(↑x : ℚ_[p])‖

Tactic:
Padic.nonarchimedean _ _

Premises used: Padic.nonarchimedean