rw [t3] at hj
case intro.intro.inr.intro.intro.inr.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t3 : j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
case intro.intro.inr.intro.intro.inr.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))