Theorem: ndiv_mul_left (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ a * b % p ≠ 0 → a % p ≠ 0
Tactic:
intro hab ha
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ False

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ False
Tactic:
apply hab
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ a * b % p = 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ a * b % p = 0
Tactic:
simp [Nat.mul_mod, ha]
State after:
no goals