internlm/Lean-Github huggingface dataset:
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
simp only [min, if_pos (le_of_lt h)]
Proof state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)
Tactic:
apply le_of_eq
Proof state after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (a + b)
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (a + b)
Tactic:
rw [nat_val_add_eq_min p a b h]
Proof state after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p a
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p a
Tactic:
rw [inf_eq_left]
Proof state after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ≤ nat_valuation p b
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ≤ nat_valuation p b
Tactic:
exact h.le
Proof state after:
no goals
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b ∨ nat_valuation p b < nat_valuation p a
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
cases h with
| inl h =>
simp only [min, if_pos (le_of_eq h)]
sorry
| inr h =>
simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
apply le_of_eq
rw [nat_val_add_eq_min p b a h]
simp
exact h.le
Proof state after:
no goals
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
simp only [min, if_pos (le_of_eq h)]
Proof state after:
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
Proof state after:
case inr.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (b + a)
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (b + a)
Tactic:
apply le_of_eq
Proof state after:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (b + a)
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (b + a)
Tactic:
rw [nat_val_add_eq_min p b a h]
Proof state after:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p b
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p b
Tactic:
simp
Proof state after:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p b ≤ nat_valuation p a
Theorem: Int.nat_val_add_ge_min
Proof state before:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p b ≤ nat_valuation p a
Tactic:
exact h.le
Proof state after:
no goals
Theorem: Int.natAbs_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℤ
⊢ natAbs (a + b) = max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.int_val_add_ge_min
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
⊢ min (int_val p a) (int_val p b) ≤ int_val p (a + b)
Tactic:
simp [int_val, natAbs_add]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
⊢ nat_valuation p (natAbs a) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)) ∨
    nat_valuation p (natAbs b) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b))
Theorem: Int.int_val_add_ge_min
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
⊢ nat_valuation p (natAbs a) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)) ∨
    nat_valuation p (natAbs b) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b))
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.int_val_add_eq_min
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
h : int_val p a < int_val p b
⊢ int_val p (a + b) = int_val p a
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ ↔ a = 0
Tactic:
apply Iff.intro
Proof state after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Tactic:
. intro hval
  simp [int_val, nat_valuation] at hval
  cases abs_a : (natAbs a) with
  | zero => exact natAbs_eq_zero.1 abs_a
  | succ n =>
    cases hp : p with
    | zero =>
      rw [hp] at gt1
      apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
    | succ p' =>
      cases hp' : p' with
      | zero =>
        rw [hp, hp'] at gt1
        apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
      | succ n =>
        simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
Proof state after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Tactic:
. intro ha
  simp [ha, int_val, nat_valuation]
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0
Tactic:
intro hval
Proof state after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval : int_val p a = ⊤
⊢ a = 0
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval : int_val p a = ⊤
⊢ a = 0
Tactic:
simp [int_val, nat_valuation] at hval
Proof state after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
⊢ a = 0
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
⊢ a = 0
Tactic:
cases abs_a : (natAbs a) with
| zero => exact natAbs_eq_zero.1 abs_a
| succ n =>
  cases hp : p with
  | zero =>
    rw [hp] at gt1
    apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
  | succ p' =>
    cases hp' : p' with
    | zero =>
      rw [hp, hp'] at gt1
      apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
    | succ n =>
      simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
abs_a : natAbs a = Nat.zero
⊢ a = 0
Tactic:
exact natAbs_eq_zero.1 abs_a
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
⊢ a = 0
Tactic:
cases hp : p with
| zero =>
  rw [hp] at gt1
  apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
| succ p' =>
  cases hp' : p' with
  | zero =>
    rw [hp, hp'] at gt1
    apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
  | succ n =>
    simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
hp : p = Nat.zero
⊢ a = 0
Tactic:
rw [hp] at gt1
Proof state after:
case mp.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.zero
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
hp : p = Nat.zero
⊢ a = 0
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.zero
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
hp : p = Nat.zero
⊢ a = 0
Tactic:
apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
hp : p = Nat.succ p'
⊢ a = 0
Tactic:
cases hp' : p' with
| zero =>
  rw [hp, hp'] at gt1
  apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
| succ n =>
  simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
hp : p = Nat.succ p'
hp' : p' = Nat.zero
⊢ a = 0
Tactic:
rw [hp, hp'] at gt1
Proof state after:
case mp.succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
gt1 : 1 < Nat.succ Nat.zero
hp : p = Nat.succ p'
hp' : p' = Nat.zero
⊢ a = 0
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
gt1 : 1 < Nat.succ Nat.zero
hp : p = Nat.succ p'
hp' : p' = Nat.zero
⊢ a = 0
Tactic:
apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mp.succ.succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n✝ : ℕ
abs_a : natAbs a = Nat.succ n✝
p' : ℕ
hp : p = Nat.succ p'
n : ℕ
hp' : p' = Nat.succ n
⊢ a = 0
Tactic:
simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
Proof state after:
no goals
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Tactic:
intro ha
Proof state after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
ha : a = 0
⊢ int_val p a = ⊤
Theorem: Int.int_val_eq_top_iff_zero
Proof state before:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
ha : a = 0
⊢ int_val p a = ⊤
Tactic:
simp [ha, int_val, nat_valuation]
Proof state after:
no goals
Theorem: Int.nat_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
k : ℕ
⊢ nat_valuation p k = 0 ↔ k % p ≠ 0
Tactic:
have := nat_val_aux_succ
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
k : ℕ
this :
  ∀ (q m : ℕ) (hq : 1 < q + 2),
    nat_valuation_aux (q + 2) hq (m + 1) =
      if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation_aux (q + 2) hq ((m + 1) / (q + 2)) + 1
⊢ nat_valuation p k = 0 ↔ k % p ≠ 0
Theorem: Int.nat_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
k : ℕ
this :
  ∀ (q m : ℕ) (hq : 1 < q + 2),
    nat_valuation_aux (q + 2) hq (m + 1) =
      if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation_aux (q + 2) hq ((m + 1) / (q + 2)) + 1
⊢ nat_valuation p k = 0 ↔ k % p ≠ 0
Tactic:
simp only [nat_valuation, ne_eq]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
k : ℕ
this :
  ∀ (q m : ℕ) (hq : 1 < q + 2),
    nat_valuation_aux (q + 2) hq (m + 1) =
      if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation_aux (q + 2) hq ((m + 1) / (q + 2)) + 1
⊢ (match p, k with
      | x, 0 => ⊤
      | 0, Nat.succ n => 0
      | 1, Nat.succ x => ⊤
      | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
      0 ↔
    ¬k % p = 0
Theorem: Int.nat_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
k : ℕ
this :
  ∀ (q m : ℕ) (hq : 1 < q + 2),
    nat_valuation_aux (q + 2) hq (m + 1) =
      if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation_aux (q + 2) hq ((m + 1) / (q + 2)) + 1
⊢ (match p, k with
      | x, 0 => ⊤
      | 0, Nat.succ n => 0
      | 1, Nat.succ x => ⊤
      | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
      0 ↔
    ¬k % p = 0
Tactic:
aesop
Proof state after:
no goals
Theorem: Int.Int.neg_emod_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : ℤ
⊢ -p % k = 0 ↔ p % k = 0
Tactic:
simp [← Int.dvd_iff_emod_eq_zero]
Proof state after:
no goals
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ int_val p k = 0 ↔ k % ↑p ≠ 0
Tactic:
simp only [int_val]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ nat_valuation p (natAbs k) = 0 ↔ k % ↑p ≠ 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ nat_valuation p (natAbs k) = 0 ↔ k % ↑p ≠ 0
Tactic:
rw [nat_valuation_eq_zero_iff hp]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p ≠ 0 ↔ k % ↑p ≠ 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p ≠ 0 ↔ k % ↑p ≠ 0
Tactic:
rw [not_iff_not]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p = 0 ↔ k % ↑p = 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p = 0 ↔ k % ↑p = 0
Tactic:
aesop
Proof state after:
case mp
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : natAbs k % p = 0
⊢ ↑p ∣ k

case mpr
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : ↑p ∣ k
⊢ natAbs k % p = 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : natAbs k % p = 0
⊢ ↑p ∣ k

case mpr
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : ↑p ∣ k
⊢ natAbs k % p = 0
Tactic:
. cases k
  . rwa [ofNat_eq_coe, dvd_iff_mod_eq_zero, ← Int.natAbs_eq_zero]
  .
    rw [dvd_iff_mod_eq_zero]
    rw [mod]
    simp at *
    rw [dvd_iff_mod_eq_zero]
    norm_cast
    rw [Nat.succ_eq_add_one] at a
    exact Iff.mp natAbs_eq_zero a
Proof state after:
case mpr
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : ↑p ∣ k
⊢ natAbs k % p = 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mpr
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : ↑p ∣ k
⊢ natAbs k % p = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : natAbs k % p = 0
⊢ ↑p ∣ k
Tactic:
cases k
Proof state after:
case mp.ofNat
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs (ofNat a✝) % p = 0
⊢ ↑p ∣ ofNat a✝

case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ ↑p ∣ -[a✝+1]
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.ofNat
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs (ofNat a✝) % p = 0
⊢ ↑p ∣ ofNat a✝

case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ ↑p ∣ -[a✝+1]
Tactic:
. rwa [ofNat_eq_coe, dvd_iff_mod_eq_zero, ← Int.natAbs_eq_zero]
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ ↑p ∣ -[a✝+1]
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ ↑p ∣ -[a✝+1]
Tactic:
.
  rw [dvd_iff_mod_eq_zero]
  rw [mod]
  simp at *
  rw [dvd_iff_mod_eq_zero]
  norm_cast
  rw [Nat.succ_eq_add_one] at a
  exact Iff.mp natAbs_eq_zero a
Proof state after:
no goals
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.ofNat
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs (ofNat a✝) % p = 0
⊢ ↑p ∣ ofNat a✝
Tactic:
rwa [ofNat_eq_coe, dvd_iff_mod_eq_zero, ← Int.natAbs_eq_zero]
Proof state after:
no goals
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ ↑p ∣ -[a✝+1]
Tactic:
rw [dvd_iff_mod_eq_zero]
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ mod -[a✝+1] ↑p = 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ mod -[a✝+1] ↑p = 0
Tactic:
rw [mod]
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ (match -[a✝+1], ↑p with
    | ofNat m, ofNat n => ofNat (m % n)
    | ofNat m, -[n+1] => ofNat (m % Nat.succ n)
    | -[m+1], ofNat n => -ofNat (Nat.succ m % n)
    | -[m+1], -[n+1] => -ofNat (Nat.succ m % Nat.succ n)) =
    0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ (match -[a✝+1], ↑p with
    | ofNat m, ofNat n => ofNat (m % n)
    | ofNat m, -[n+1] => ofNat (m % Nat.succ n)
    | -[m+1], ofNat n => -ofNat (Nat.succ m % n)
    | -[m+1], -[n+1] => -ofNat (Nat.succ m % Nat.succ n)) =
    0
Tactic:
simp at *
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ ↑p ∣ ↑a✝ + 1
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ ↑p ∣ ↑a✝ + 1
Tactic:
rw [dvd_iff_mod_eq_zero]
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ mod (↑a✝ + 1) ↑p = 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ mod (↑a✝ + 1) ↑p = 0
Tactic:
norm_cast
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ mod ↑(a✝ + 1) ↑p = 0