Theorem: nat_valuation_aux'_of_not_dvd (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ nat_valuation_aux' q hq m hm = 0
Tactic:
rw [nat_valuation_aux']
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ (match m, hm with
    | m, hm => ↑(nat_valuation_aux'' q hq m hm 0)) =
    0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ (match m, hm with
    | m, hm => ↑(nat_valuation_aux'' q hq m hm 0)) =
    0
Tactic:
simp [nat_valuation_aux''_of_not_dvd q hq m hm hmq]
State after:
no goals