Theorem: Int.mul_eq_zero_left (Smt/Reconstruct/Int/Lemmas.lean)

State before:
x y : Int
hx : x ≠ 0
hxy : x * y = 0
⊢ y = 0
Tactic:
rewrite [Int.mul_eq_zero] at hxy
State after:
x y : Int
hx : x ≠ 0
hxy : x = 0 ∨ y = 0
⊢ y = 0

State before:
x y : Int
hx : x ≠ 0
hxy : x = 0 ∨ y = 0
⊢ y = 0
Tactic:
exact hxy.resolve_left hx
State after:
no goals