awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ ¬(↑p : ℤ_[p]) ∣ (↑x : ℤ_[p])

Tactic:
irreducible_p.not_dvd_isUnit x.isUnit

Premises used: Irreducible.not_dvd_isUnit, PadicInt.irreducible_p, Units.isUnit
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ ¬(↑p : ℤ_[p]) ∣ (↑x : ℤ_[p])

Tactic:
exact irreducible_p.not_dvd_isUnit x.isUnit

Premises used: Irreducible.not_dvd_isUnit, PadicInt.irreducible_p, Units.isUnit
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑(f 1) : ℤ_[p]))
a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑1 : ℤ_[p]))
⊢ Eq (α := ZMod v) (↑(f 1) : ZMod v) 1

Tactic:
rw [f_congr (1 : ℤ_[p]) _ 1, cast_one]

Premises used: OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑(f 1) : ℤ_[p]))

Tactic:
f_spec _

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑(f 1) : ℤ_[p]))

Tactic:
exact f_spec _
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑1 : ℤ_[p]))

Tactic:
simp only [sub_self, cast_one, Submodule.zero_mem]

Premises used: sub_self, Submodule.zero_mem, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f (x * y)) : ℤ_[p]))
a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f x * f y) : ℤ_[p]))
⊢ (↑(f (x * y)) : ZMod v) = HMul.hMul (α := ZMod v) (↑(f x) : ZMod v) (↑(f y) : ZMod v)

Tactic:
rw [f_congr (x * y) _ (f x * f y), cast_mul]

Premises used: HMul.hMul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f (x * y)) : ℤ_[p]))

Tactic:
f_spec _

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f (x * y)) : ℤ_[p]))

Tactic:
exact f_spec _
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {(↑v : ℤ_[p])}
⊢ x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p]) ∈ I

Tactic:
I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x))

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {(↑v : ℤ_[p])}
h : x * y - (↑(f x * f y) : ℤ_[p]) = x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f x * f y) : ℤ_[p]))

Tactic:
convert! I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x)) using 1

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {(↑v : ℤ_[p])}
h :
  x * y - HMul.hMul (α := ℤ_[p]) (↑(f x) : ℤ_[p]) (↑(f y) : ℤ_[p]) =
    x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])
⊢ x * y - (↑(f x * f y) : ℤ_[p]) = x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])

Tactic:
rw [cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {(↑v : ℤ_[p])}
⊢ x * y - HMul.hMul (α := ℤ_[p]) (↑(f x) : ℤ_[p]) (↑(f y) : ℤ_[p]) =
    x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])

Tactic:
ring
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑(f 0) : ℤ_[p]))
a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑0 : ℤ_[p]))
⊢ Eq (α := ZMod v) (↑(f 0) : ZMod v) 0

Tactic:
rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]

Premises used: Nat.cast_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑(f 0) : ℤ_[p]))

Tactic:
f_spec _

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑(f 0) : ℤ_[p]))

Tactic:
exact f_spec _
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑0 : ℤ_[p]))

Tactic:
simp only [sub_zero, cast_zero, Submodule.zero_mem]

Premises used: sub_zero, Submodule.zero_mem, Nat.cast_zero
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f (x + y)) : ℤ_[p]))
a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f x + f y) : ℤ_[p]))
⊢ (↑(f (x + y)) : ZMod v) = HAdd.hAdd (α := ZMod v) (↑(f x) : ZMod v) (↑(f y) : ZMod v)

Tactic:
rw [f_congr (x + y) _ (f x + f y), cast_add]

Premises used: Nat.cast_add, HAdd.hAdd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f (x + y)) : ℤ_[p]))

Tactic:
f_spec _

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f (x + y)) : ℤ_[p]))

Tactic:
exact f_spec _
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p])))

Tactic:
Ideal.add_mem _ (f_spec x) (f_spec y)

Premises used: Ideal.add_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
h : x + y - (↑(f x + f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f x + f y) : ℤ_[p]))

Tactic:
convert! Ideal.add_mem _ (f_spec x) (f_spec y) using 1

Premises used: Ideal.add_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
h : x + y - HAdd.hAdd (α := ℤ_[p]) (↑(f x) : ℤ_[p]) (↑(f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))
⊢ x + y - (↑(f x + f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))

Tactic:
rw [cast_add]

Premises used: Nat.cast_add
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ x + y - HAdd.hAdd (α := ℤ_[p]) (↑(f x) : ℤ_[p]) (↑(f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
rw : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))
⊢ ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑x.zmodRepr : ℤ_[p]))

Tactic:
rw [← maximalIdeal_eq_span_p]

Premises used: PadicInt.maximalIdeal_eq_span_p
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[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)
r : ℚ
x : ℤ_[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)
r : ℚ
x : ℤ_[p]
rw :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod p) (↑a : ZMod p) (↑b : ZMod p)
⊢ ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod p) (↑a : ZMod p) (↑b : ZMod p)

Tactic:
rw [← maximalIdeal_eq_span_p]

Premises used: PadicInt.maximalIdeal_eq_span_p
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod p) (↑a : ZMod p) (↑b : ZMod p)

Tactic:
zmod_congr_of_sub_mem_max_ideal

Premises used: PadicInt.zmod_congr_of_sub_mem_max_ideal
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod p) (↑a : ZMod p) (↑b : ZMod p)

Tactic:
exact zmod_congr_of_sub_mem_max_ideal

Premises used: PadicInt.zmod_congr_of_sub_mem_max_ideal
-- 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 x

Premises used: PadicInt.sub_zmodRepr_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Eq (α := ℤ_[p]) (ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x)) (↑x.zmodRepr : ℤ_[p])
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x))

Tactic:
convert! sub_zmodRepr_mem x using 2

Premises used: PadicInt.sub_zmodRepr_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Eq (α := ℤ_[p]) (ZMod.cast (n := p) (↑x.zmodRepr : ZMod p)) (↑x.zmodRepr : ℤ_[p])
⊢ Eq (α := ℤ_[p]) (ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x)) (↑x.zmodRepr : ℤ_[p])

Tactic:
dsimp [toZMod, toZModHom]

Premises used: PadicInt.toZModHom, PadicInt.toZMod
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h :
  ∀ (p' : ℕ) [hp_prime : Fact (Nat.Prime (0 + p' + 1))] (x : ℤ_[0 + p' + 1]),
    Eq (α := ℤ_[0 + p' + 1]) (ZMod.cast (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1)))
      (↑x.zmodRepr : ℤ_[0 + p' + 1])
⊢ Eq (α := ℤ_[p]) (ZMod.cast (n := p) (↑x.zmodRepr : ZMod p)) (↑x.zmodRepr : ℤ_[p])

Tactic:
rcases Nat.exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩

Premises used: Nat.Prime.pos, Nat.exists_eq_add_of_lt, rfl, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
h : ZMod.val (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1)) = x.zmodRepr
⊢ Eq (α := ℤ_[0 + p' + 1]) (↑(ZMod.val (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1))) : ℤ_[0 + p' + 1])
    (↑x.zmodRepr : ℤ_[0 + p' + 1])

Tactic:
rw [Nat.cast_inj]

Premises used: Nat.cast_inj
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
h : x.zmodRepr < (0 + p').succ
⊢ ZMod.val (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1)) = x.zmodRepr

Tactic:
apply mod_eq_of_lt

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ x.zmodRepr < (0 + p').succ

Tactic:
simpa only [zero_add] using zmodRepr_lt_p x

Premises used: zero_add, PadicInt.zmodRepr_lt_p
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
h :
  ∀ (x : ℤ_[p]),
    Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod p) toZMod) x ↔
      Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
⊢ Eq (α := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod p) toZMod) (maximalIdeal ℤ_[p])

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h :
  Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
⊢ Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod p) toZMod) x ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x

Tactic:
rw [RingHom.mem_ker]

Premises used: RingHom.mem_ker
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h :
  Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) →
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
h₁ :
  Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x →
    Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p)
⊢ Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x

Tactic:
simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x

Premises used: sub_zero, ZMod.cast_zero, PadicInt.toZMod_spec
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)

Tactic:
rw [← sub_zero x] at h

Premises used: sub_zero
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
h₁ : Eq (α := ZMod p) (↑x.zmodRepr : ZMod p) 0
⊢ Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p)

Tactic:
dsimp [toZMod, toZModHom]

Premises used: PadicInt.toZModHom, PadicInt.toZMod