apply_fun (λ e => e - 3) at hl
case intro.intro.intro
rel_sub : True
y : ℤ
hl : 3 + 3 * y = 4
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
⊢ False
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : 3 + 3 * y - 3 = 4 - 3
⊢ False