cases' hg12 with hg1 hg2
case h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
j : ℕ
g : ℤ
hg0 : 1 ≤ j
hg12 : 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 1) ∨ 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 2)
coe_coe : -↑(Int.toNat (-n)) = n
⊢ ∃ b, 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * b + 1) ∨ 3 * n = 3 ^ j * (3 * b + 2))
case h.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : -↑(Int.toNat (-n)) = n
hg1 : 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 1)
⊢ ∃ b, 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * b + 1) ∨ 3 * n = 3 ^ j * (3 * b + 2))

case h.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : -↑(Int.toNat (-n)) = n
hg2 : 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 2)
⊢ ∃ b, 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * b + 1) ∨ 3 * n = 3 ^ j * (3 * b + 2))