awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]))
hm₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
⊢ Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)
have hn₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
Tactic: rw [maximalIdeal_eq_span_p] at hm hn
Cleared hypotheses: hm, hn
-- 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]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑m : ℤ_[p]))
hn : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑n : ℤ_[p]))
⊢ Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)
have 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))
Tactic: have := zmod_congr_of_sub_mem_span_aux 1 x m n
-- 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]) (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))
⊢ Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)
have 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))
Tactic: simp only [pow_one] 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]) (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 p) (↑m : ZMod p) (↑n : ZMod p)
have this₁ : Eq (α := ZMod (HPow.hPow (β := ℕ) p 1)) (↑(↑m : ℤ) : ZMod (p ^ 1)) (↑(↑n : ℤ) : ZMod (p ^ 1))
Tactic: specialize this hm hn
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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))
⊢ p ∣ HPow.hPow (β := ℕ) p 1
have rw : p ∣ p
Tactic: rw [pow_one]
-- 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]) (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) (↑m : ZMod p) (↑n : ZMod p)
have this₁ : Eq (α := ZMod p) ((ZMod.castHom sorry (ZMod p) : (a : ZMod (p ^ 1)) → ZMod p) (↑(↑m : ℤ) : ZMod (p ^ 1)))
  ((ZMod.castHom sorry (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
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]) (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)
have this₁ : Eq (α := ZMod p) (↑(↑m : ℤ) : ZMod p) (↑(↑n : ℤ) : ZMod p)
Tactic: simp only [map_intCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃ n < p, Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
have simp : ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
Tactic: simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
have obtain : ∀ (r : ℚ) (hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1), ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
Tactic: obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
have hr₁ : ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ < 1
Tactic: rw [norm_sub_rev] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p])‖ < 1
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
have _ : norm (E := ℚ_[p]) (↑r : ℚ_[p]) = ‖(↑r : ℚ_[p]) - (↑x : ℚ_[p]) + (↑x : ℚ_[p])‖
Tactic: calc
      _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
      _ ≤ _ := Padic.nonarchimedean _ _
      _ ≤ _ := max_le (le_of_lt hr) x.2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ < 1
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
have H : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 < p, ‖x - (↑n : ℤ_[p])‖ < 1
have 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
Tactic: obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ ∃ n < p, ‖x - (↑n : ℤ_[p])‖ < 1
have 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
Tactic: lift n to ℕ using hzn
Cleared hypotheses: n, hzn, hnp, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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, ‖x - (↑n : ℤ_[p])‖ < 1
have h : n < p ∧ ‖x - (↑n : ℤ_[p])‖ < 1
Tactic: use n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 ∧ ‖x - (↑n : ℤ_[p])‖ < 1
have h : n < p
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ n < p ∧ ‖x - (↑n : ℤ_[p])‖ < 1
have h₁ : ‖x - (↑n : ℤ_[p])‖ < 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ ‖x - (↑n : ℤ_[p])‖ < 1
have h : ‖(↑x : ℚ_[p]) - (↑n : ℚ_[p])‖ < 1
Tactic: simp only [norm_def, coe_sub, coe_natCast] at hn ⊢
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])‖ < 1
have h : ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p]) + HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
Tactic: rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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]) - (↑r : ℚ_[p]) + HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
have h : max ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
Tactic: apply lt_of_le_of_lt (Padic.nonarchimedean _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ max ‖(↑x : ℚ_[p]) - (↑r : ℚ_[p])‖ ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
have h : ‖HSub.hSub (α := ℚ_[p]) (↑r : ℚ_[p]) (↑n : ℚ_[p])‖ < 1
Tactic: apply max_lt hr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃! n : ℕ, n < p ∧ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑n : ℤ_[p]))
have 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]))
Tactic: obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
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]))
have 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
Tactic: use n, ⟨hn₁, hn₂⟩, fun m ⟨hm₁, hm₂⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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]))
⊢ m = n
have this : Eq (α := ZMod p) (↑m : ZMod p) (↑n : ZMod p)
Tactic: have := (zmod_congr_of_sub_mem_max_ideal x n m hn₂ hm₂).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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)
⊢ m = n
have right : ∀ (this : m ≡ n [MOD p]), m = n
Tactic: rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ m = n
have right₁ : ∀ (this : m % p = n % p), m = n
Tactic: rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ m = n
have right₂ : ∀ (this : m % p = n), m = n
Tactic: rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ m = n
have right₃ : ∀ (this : m = n), m = n
Tactic: rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : (↑p : ℤ_[p]) ∣ x
⊢ x.zmodRepr = 0
have apply : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑0 : ℤ_[p]))
Tactic: apply zmodRepr_unique _ _ (Nat.Prime.pos Fact.out)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
have rw : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))
Tactic: rw [← mem_nonunits, ← IsLocalRing.mem_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
have inl : ∀ (H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
Tactic: rcases eq_or_ne ‖(x.zmodRepr : ℤ_[p])‖ ‖x‖ with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
have inr : ∀ (H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
Tactic: rcases eq_or_ne ‖(x.zmodRepr : ℤ_[p])‖ ‖x‖ with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
have inl : ‖x‖ = 1 ↔ ‖x‖ = 1
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
have this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
Tactic: have := x.norm_sub_zmodRepr_lt_one
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) ≠ ‖x‖
this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
have inr : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 → ‖x‖ = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ ‖x‖ = 1
have inr₁ : ‖x‖ = 1 → norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ ‖x‖ = 1
have 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])
Tactic: rw [← h] at this ⊢
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1
have inr : ∀ (this : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < ‖x‖) (h : ‖x‖ = 1), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖
Tactic: rw [← h] at this ⊢
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.zmodRepr = 0 ↔ (↑p : ℤ_[p]) ∣ x
have refine : ∀ (H : x.zmodRepr = 0), (↑p : ℤ_[p]) ∣ x
Tactic: refine ⟨fun H ↦ ?_, zmodRepr_eq_zero_of_dvd⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ (↑p : ℤ_[p]) ∣ x
have rw : ‖x - (↑x.zmodRepr : ℤ_[p])‖ < 1
Tactic: rw [← norm_lt_one_iff_dvd, ← sub_zero x, ← Nat.cast_zero, ← H]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1 ↔ x.zmodRepr ≠ 0
have rw : ‖x‖ = 1 ↔ ¬‖x‖ < 1
Tactic: rw [norm_natCast_zmodRepr_eq_one_iff, ne_eq, zmodRepr_eq_zero_iff_dvd, ← norm_lt_one_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ zmodRepr (p := p) (↑x.zmodRepr : ℤ_[p]) = x.zmodRepr
have apply : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
  (HSub.hSub (α := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) (↑x.zmodRepr : ℤ_[p]))
Tactic: apply zmodRepr_unique _ _ (zmodRepr_lt_p _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
have inl : ∀ (h : norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = 1), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
Tactic: rcases norm_natCast_zmodRepr_eq x with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
have inr : ∀ (h : x.zmodRepr = 0), norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
Tactic: rcases norm_natCast_zmodRepr_eq x with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ norm (E := ℤ_[p]) (↑x.zmodRepr : ℤ_[p]) = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
have inr : ‖x‖ = norm (E := ℤ_[p]) (↑0 : ℤ_[p]) ↔ ‖x‖ = 1 ∨ x = 0
Tactic: rw [eq_comm, h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ zmodRepr (p := p) (↑n : ℤ_[p]) = n % p
have nth_rw : zmodRepr (p := p) (↑(n % p + p * (n / p)) : ℤ_[p]) = n % p
Tactic: nth_rw 1 [← Nat.mod_add_div n p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ zmodRepr (p := p) (↑(n % p + p * (n / p)) : ℤ_[p]) = n % p
have hy₁ : n % p < p
Tactic: apply zmodRepr_unique
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hy₁ : n % p < p
⊢ zmodRepr (p := p) (↑(n % p + p * (n / p)) : ℤ_[p]) = n % p
have hy₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
  (HSub.hSub (α := ℤ_[p]) (↑(n % p + p * (n / p)) : ℤ_[p]) (↑(n % p) : ℤ_[p]))
Tactic: apply zmodRepr_unique
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
⊢ zmodRepr (p := p) (↑n : ℤ_[p]) = n
have rw : n % p = n
Tactic: rw [zmodRepr_natCast (p := p) n, Nat.mod_eq_of_lt hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
rw : n % p = n
⊢ zmodRepr (p := p) (↑n : ℤ_[p]) = n
have rw₁ : n = n
Tactic: rw [zmodRepr_natCast (p := p) n, Nat.mod_eq_of_lt hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
⊢ zmodRepr (p := p) (OfNat.ofNat n) = OfNat.ofNat n
have h : Eq (α := ℤ_[p]) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℤ_[p])
Tactic: convert! zmodRepr_natCast_of_lt hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℤ_[p])
have h : ∀ (hn : OfNat.ofNat 0 < p), Eq (α := ℤ_[p]) (OfNat.ofNat 0) (↑(OfNat.ofNat 0) : ℤ_[p])
Tactic: rcases n with _ | _ | n
Cleared hypotheses: n, hn