Theorem: Int.int_valuation_eq_zero_iff (ECTate/Algebra/ValuedRing.lean)

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]
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

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]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p ≠ 0 ↔ k % ↑p ≠ 0

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]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p = 0 ↔ k % ↑p = 0

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
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

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
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

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
State after:
no goals

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
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]

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]
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]

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
State after:
no goals

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]
State after:
no goals

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]
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

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]
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

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 *
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

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]
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

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
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

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:
rw [Nat.succ_eq_add_one] at a
State after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : (a✝ + 1) % p = 0
⊢ mod ↑(a✝ + 1) ↑p = 0

State before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : (a✝ + 1) % p = 0
⊢ mod ↑(a✝ + 1) ↑p = 0
Tactic:
exact Iff.mp natAbs_eq_zero a
State after:
no goals