cases' r2 with j hj
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
r2 : ∃ a b, 1 ≤ a ∧ (3 * ↑(Int.toNat (-n)) = 3 ^ a * (3 * b + 1) ∨ 3 * ↑(Int.toNat (-n)) = 3 ^ a * (3 * b + 2))
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
case inr.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
j : ℕ
hj : ∃ b, 1 ≤ j ∧ (3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * b + 1) ∨ 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * b + 2))
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))