rw [h2] at this'
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h2 : u + 3 * v = 0
⊢ False
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h2 : u + 3 * v = 0
⊢ False