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 = 0
Tactic:
have hmq_bool : ¬m % q == 0 := by
  intro H
  apply hmq (eq_of_beq H)
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
hmq_bool : ¬(m % q == 0) = true
⊢ 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
hmq_bool : ¬(m % q == 0) = true
⊢ nat_valuation_aux'' q hq m hm 0 = 0
Tactic:
rw [nat_valuation_aux'', dif_neg hmq_bool]
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ ¬(m % q == 0) = true
Tactic:
intro H
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
H : (m % q == 0) = true
⊢ False

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
H : (m % q == 0) = true
⊢ False
Tactic:
apply hmq (eq_of_beq H)
State after:
no goals