rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at hl
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y * 3 = 1
⊢ False
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y = 1 ∧ 3 = 1 ∨ y = -1 ∧ 3 = -1
⊢ False