rw [t1] at hj
case intro.intro.inr.intro.intro.inl.h
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 : ℕ
t1 : j = 3 * r
⊢ False
case intro.intro.inr.intro.intro.inl.h
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)
t1 : j = 3 * r
⊢ False