awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ < 1
⊢ max ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ ‖(↑x : ℚ_[p])‖ ≤ 1

Tactic:
max_le (le_of_lt hr) x.2

Premises used: le_of_lt, max_le, Subtype.property
-- 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])‖
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1

Tactic:
calc
      _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
      _ ≤ _ := Padic.nonarchimedean _ _
      _ ≤ _ := max_le (le_of_lt hr) x.2

Premises used: le_of_lt, Rat.cast, Padic.nonarchimedean, max_le, Subtype.property
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1

Tactic:
have H : ‖(r : ℚ_[p])‖ ≤ 1 := by
    rw [norm_sub_rev] at hr
    calc
      _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
      _ ≤ _ := Padic.nonarchimedean _ _
      _ ≤ _ := max_le (le_of_lt hr) x.2
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
obtain :
  ∀ (n : ℤ) (hzn : 0 ≤ n) (hnp : n < (↑p : ℤ))
    (hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑n : ℤ_[p])‖ < 1),
    ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1

Tactic:
obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H

Premises used: PadicInt.exists_mem_range_of_norm_rat_le_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑n : ℤ_[p])‖ < 1
⊢ 0 ≤ n

Tactic:
hzn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑n : ℤ_[p])‖ < 1
lift :
  ∀ (n : ℕ) (hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ))
    (hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑(↑n : ℤ) : ℤ_[p])‖ < 1),
    ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1

Tactic:
lift n to ℕ using hzn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑(↑n : ℤ) : ℤ_[p])‖ < 1
h : n < p ∧ ‖x - (↑n : ℤ_[p])‖ < 1
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1

Tactic:
use n
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑(↑n : ℤ) : ℤ_[p])‖ < 1
h : n < p
h₁ : ‖x - (↑n : ℤ_[p])‖ < 1
⊢ n < p ∧ ‖x - (↑n : ℤ_[p])‖ < 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑(↑n : ℤ) : ℤ_[p])‖ < 1
⊢ n < p

Tactic:
mod_cast hnp

Premises used: Nat.cast_lt._simp_1, cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑(↑n : ℤ) : ℤ_[p])‖ < 1
⊢ n < p

Tactic:
exact mod_cast hnp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑r : ℚ_[p]) H - (↑(↑n : ℤ) : ℤ_[p])‖ < 1
h : ‖(↑x : ℚ_[p]) - (↑n : ℚ_[p])‖ < 1
⊢ ‖x - (↑n : ℤ_[p])‖ < 1

Tactic:
simp only [norm_def, coe_sub, coe_natCast] at hn ⊢

Premises used: PadicInt.coe_sub, PadicInt.coe_natCast, PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑(↑(↑n : ℤ) : ℤ_[p]) : ℚ_[p])‖ < 1
⊢ (↑x : ℚ_[p]) - (↑n : ℚ_[p]) = (↑x : ℚ_[p]) - (↑r : ℚ_[p]) + HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])

Tactic:
ring
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑(↑(↑n : ℤ) : ℤ_[p]) : ℚ_[p])‖ < 1
h : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p]) + HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
⊢ ‖(↑x : ℚ_[p]) - (↑n : ℚ_[p])‖ < 1

Tactic:
rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑(↑(↑n : ℤ) : ℤ_[p]) : ℚ_[p])‖ < 1
h : max ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
⊢ ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p]) + HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1

Tactic:
apply lt_of_le_of_lt (Padic.nonarchimedean _ _)

Premises used: lt_of_le_of_lt, Padic.nonarchimedean
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑(↑(↑n : ℤ) : ℤ_[p]) : ℚ_[p])‖ < 1
h : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
⊢ max ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1

Tactic:
apply max_lt hr

Premises used: max_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
H : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
n : ℕ
hnp : LT.lt (α := ℤ) (↑n : ℤ) (↑p : ℤ)
hn : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑(↑(↑n : ℤ) : ℤ_[p]) : ℚ_[p])‖ < 1
⊢ ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1

Tactic:
simpa using hn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
obtain :
  ∀ (n : ℕ) (hn₁ : n < p) (hn₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))),
    ∃! n : ℕ, n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
⊢ ∃! n : ℕ, n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x

Premises used: PadicInt.exists_mem_range
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
right :
  ∀ (m : ℕ),
    (fun (n : ℕ) ↦ n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))) m →
      ∀ (hm₁ : m < p) (hm₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑m : ℤ_[p]))), m = n
⊢ ∃! n : ℕ, n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))

Tactic:
use n, ⟨hn₁, hn₂⟩, fun m ⟨hm₁, hm₂⟩ ↦ ?_
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
m : ℕ
h : (fun (n : ℕ) ↦ n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))) m
hm₁ : m < p
hm₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑m : ℤ_[p]))
⊢ Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)

Tactic:
have := (zmod_congr_of_sub_mem_max_ideal x n m hn₂ hm₂).symm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
m : ℕ
h : (fun (n : ℕ) ↦ n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))) m
hm₁ : m < p
hm₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑m : ℤ_[p]))
this : Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)
right : ∀ (this : m ≡ n [MOD p]), m = n
right₁ : ∀ (this : m % p = n % p), m = n
right₂ : ∀ (this : m % p = n), m = n
right₃ right₄ right₅ right₆ : ∀ (this : m = n), m = n
⊢ m = n

Tactic:
rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this

Premises used: Nat.mod_eq_of_lt, Nat.ModEq, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.zmodRepr < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))

Tactic:
Classical.choose_spec (existsUnique_mem_range x).exists

Premises used: PadicInt.zmodRepr, ExistsUnique.exists, Set.Mem, Classical.choose_spec, PadicInt.existsUnique_mem_range
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
y : ℕ
hy₁ : y < p
hy₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑y : ℤ_[p]))
⊢ x.zmodRepr = y

Tactic:
have h := (Classical.choose_spec (existsUnique_mem_range x)).right
  (h (zmodRepr x) (zmodRepr_spec x)).trans (h y ⟨hy₁, hy₂⟩).symm

Premises used: PadicInt.zmodRepr, PadicInt.zmodRepr_spec, Classical.choose_spec, And.right, And.intro, Eq.symm, PadicInt.existsUnique_mem_range, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.zmodRepr < p

Tactic:
(zmodRepr_spec _).1

Premises used: PadicInt.zmodRepr_spec, And.left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))

Tactic:
(zmodRepr_spec _).2

Premises used: PadicInt.zmodRepr_spec, And.right
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : (↑p : ℤ_[p]) ∣ x
apply : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑0 : ℤ_[p]))
⊢ x.zmodRepr = 0

Tactic:
apply zmodRepr_unique _ _ (Nat.Prime.pos Fact.out)

Premises used: PadicInt.zmodRepr_unique, Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : (↑p : ℤ_[p]) ∣ x
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑0 : ℤ_[p]))

Tactic:
simp [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, hx]

Premises used: PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ zmodRepr (p := p) 0 = 0

Tactic:
zmodRepr_eq_zero_of_dvd (dvd_zero _)

Premises used: dvd_zero, PadicInt.zmodRepr_eq_zero_of_dvd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
rw : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))
⊢ ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1

Tactic:
rw [← mem_nonunits, ← IsLocalRing.mem_maximalIdeal]

Premises used: IsLocalRing.mem_maximalIdeal, PadicInt.mem_nonunits
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))

Tactic:
sub_zmodRepr_mem _

Premises used: PadicInt.sub_zmodRepr_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))

Tactic:
exact sub_zmodRepr_mem _

Premises used: PadicInt.sub_zmodRepr_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
inl : ∀ (H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
inr : ∀ (H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1

Tactic:
rcases eq_or_ne ‖(x.zmodRepr : ℤ_[p])‖ ‖x‖ with H | H

Premises used: Norm.norm, PadicInt.zmodRepr, Nat.cast, eq_or_ne
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖
inl inl₁ : ‖x‖ = 1 ↔ ‖x‖ = 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1

Tactic:
rw [H]
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
⊢ ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1

Tactic:
have := x.norm_sub_zmodRepr_lt_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
inr : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 → ‖x‖ = 1
inr₁ : ‖x‖ = 1 → norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
inr :
  ∀ (this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]))
    (h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1), ‖x‖ = norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p])
⊢ ‖x‖ = 1

Tactic:
rw [← h] at this ⊢
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
h : ‖x‖ = 1
inr : ∀ (this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < ‖x‖) (h : ‖x‖ = 1), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1

Tactic:
rw [← h] at this ⊢
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p])
h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
⊢ ‖x‖ = norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p])

Tactic:
norm_eq_of_norm_sub_lt_right this

Premises used: Padic.norm_eq_of_norm_sub_lt_right
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p])
h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
⊢ ‖x‖ = norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p])

Tactic:
exact norm_eq_of_norm_sub_lt_right this

Premises used: Padic.norm_eq_of_norm_sub_lt_right
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < ‖x‖
h : ‖x‖ = 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖

Tactic:
(norm_eq_of_norm_sub_lt_left this).symm

Premises used: Eq.symm, Padic.norm_eq_of_norm_sub_lt_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < ‖x‖
h : ‖x‖ = 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖

Tactic:
exact (norm_eq_of_norm_sub_lt_left this).symm

Premises used: Eq.symm, Padic.norm_eq_of_norm_sub_lt_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.zmodRepr = 0 ↔ (↑p : ℤ_[p]) ∣ x

Tactic:
⟨fun H ↦ ?_, zmodRepr_eq_zero_of_dvd⟩

Premises used: Iff.intro, PadicInt.zmodRepr_eq_zero_of_dvd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
refine : ∀ (H : x.zmodRepr = 0), (↑p : ℤ_[p]) ∣ x
⊢ x.zmodRepr = 0 ↔ (↑p : ℤ_[p]) ∣ x

Tactic:
refine ⟨fun H ↦ ?_, zmodRepr_eq_zero_of_dvd⟩
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
rw : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
⊢ (↑p : ℤ_[p]) ∣ x

Tactic:
rw [← norm_lt_one_iff_dvd, ← sub_zero x, ← Nat.cast_zero, ← H]

Premises used: sub_zero, PadicInt.norm_lt_one_iff_dvd, Nat.cast_zero
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1

Tactic:
norm_sub_zmodRepr_lt_one _

Premises used: PadicInt.norm_sub_zmodRepr_lt_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1

Tactic:
exact norm_sub_zmodRepr_lt_one _

Premises used: PadicInt.norm_sub_zmodRepr_lt_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
rw : ‖x‖ = 1 ↔ ¬‖x‖ < 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ x.zmodRepr ≠ 0

Tactic:
rw [norm_natCast_zmodRepr_eq_one_iff, ne_eq, zmodRepr_eq_zero_iff_dvd, ← norm_lt_one_iff_dvd]

Premises used: PadicInt.norm_lt_one_iff_dvd, ne_eq, PadicInt.norm_natCast_zmodRepr_eq_one_iff, PadicInt.zmodRepr_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ = 1 ↔ ¬‖x‖ < 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ∨ x.zmodRepr = 0

Tactic:
grind [norm_natCast_zmodRepr_eq_one_iff_ne]

Premises used: PadicInt.norm_natCast_zmodRepr_eq_one_iff_ne
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
apply :
  Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
    (HSub.hSub (α := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) (↑x.zmodRepr : ℤ_[p]))
⊢ zmodRepr (p := p) (↑x.zmodRepr : ℤ_[p]) = x.zmodRepr

Tactic:
apply zmodRepr_unique _ _ (zmodRepr_lt_p _)

Premises used: PadicInt.zmodRepr_unique, PadicInt.zmodRepr_lt_p
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
    (HSub.hSub (α := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) (↑x.zmodRepr : ℤ_[p]))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
inl :
  ∀ (h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
inr : ∀ (h : x.zmodRepr = 0), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
rcases norm_natCast_zmodRepr_eq x with h | h

Premises used: PadicInt.norm_natCast_zmodRepr_eq
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
simp_all [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
inr : ‖x‖ = norm (E := ℤ_[p]) (↑0 : ℤ_[p]) ↔ ‖x‖ = 1 ∨ x = 0
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
rw [eq_comm, h]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖x‖ = norm (E := ℤ_[p]) (↑0 : ℤ_[p]) ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
simp [← norm_natCast_zmodRepr_eq_one_iff, h]

Premises used: PadicInt.norm_natCast_zmodRepr_eq_one_iff
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
nth_rw : zmodRepr (p := p) (↑(n % p + p * (n / p)) : ℤ_[p]) = n % p
⊢ zmodRepr (p := p) (↑n : ℤ_[p]) = n % p

Tactic:
nth_rw 1 [← Nat.mod_add_div n p]

Premises used: Nat.mod_add_div
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hy₁ : n % p < p
hy₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
    (HSub.hSub (α := ℤ_[p]) (↑(n % p + p * (n / p)) : ℤ_[p]) (↑(n % p) : ℤ_[p]))
⊢ zmodRepr (p := p) (↑(n % p + p * (n / p)) : ℤ_[p]) = n % p

Tactic:
apply zmodRepr_unique

Premises used: PadicInt.zmodRepr_unique
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ n % p < p

Tactic:
Nat.mod_lt _ (Nat.Prime.pos Fact.out)

Premises used: Nat.Prime.pos, Nat.mod_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ n % p < p

Tactic:
exact Nat.mod_lt _ (Nat.Prime.pos Fact.out)

Premises used: Nat.Prime.pos, Nat.mod_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
    (HSub.hSub (α := ℤ_[p]) (↑(n % p + p * (n / p)) : ℤ_[p]) (↑(n % p) : ℤ_[p]))

Tactic:
simp [maximalIdeal_eq_span_p, Ideal.mem_span_singleton]

Premises used: PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
rw : n % p = n
rw₁ rw₂ : n = n
⊢ zmodRepr (p := p) (↑n : ℤ_[p]) = n

Tactic:
rw [zmodRepr_natCast (p := p) n, Nat.mod_eq_of_lt hn]

Premises used: Nat.mod_eq_of_lt, PadicInt.zmodRepr_natCast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
⊢ zmodRepr (p := p) (↑(OfNat.ofNat n) : ℤ_[p]) = OfNat.ofNat n

Tactic:
zmodRepr_natCast_of_lt hn

Premises used: PadicInt.zmodRepr_natCast_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
h : Eq (α := ℤ_[p]) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℤ_[p])
⊢ zmodRepr (p := p) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
convert! zmodRepr_natCast_of_lt hn

Premises used: PadicInt.zmodRepr_natCast_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
h : ∀ (hn : OfNat.ofNat 0 < p), Eq (α := ℤ_[p]) (OfNat.ofNat 0) (↑(OfNat.ofNat 0) : ℤ_[p])
h₁ :
  ∀ (hn : OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1) < p),
    Eq (α := ℤ_[p]) (OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) (↑(OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) : ℤ_[p])
h₂ :
  ∀ (n : ℕ) (hn : OfNat.ofNat (n + 1 + 1) < p),
    Eq (α := ℤ_[p]) (OfNat.ofNat (n + 1 + 1)) (↑(OfNat.ofNat (n + 1 + 1)) : ℤ_[p])
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℤ_[p])

Tactic:
rcases n with _ | _ | n
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat 0 < p
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat 0) (↑(OfNat.ofNat 0) : ℤ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1) < p
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) (↑(OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) : ℤ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat (n + 1 + 1) < p
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat (n + 1 + 1)) (↑(OfNat.ofNat (n + 1 + 1)) : ℤ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
rw : ¬(↑p : ℤ_[p]) ∣ (↑x : ℤ_[p])
⊢ (↑x : ℤ_[p]).zmodRepr ≠ 0

Tactic:
rw [ne_eq, zmodRepr_eq_zero_iff_dvd]

Premises used: ne_eq, PadicInt.zmodRepr_eq_zero_iff_dvd