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

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

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

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