internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case h.right
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
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
right
Proof state after:
case h.right.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 + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case h.right.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 + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
exact_mod_cast hj
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof state before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
⊢ 3 ∣ 3 * n
Tactic:
use n
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof state before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ 3 ∣ 3 * n ∧ ¬3 ∣ 3 * n
Tactic:
constructor
Proof state after:
case left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ 3 ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ 3 ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n
Tactic:
exact p
Proof state after:
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n
Tactic:
exact h2
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case intro.intro.inr.intro.intro.inl
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
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
exfalso
Proof state after:
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
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
Tactic:
rw [t1] at hj
Proof state after:
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
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
Tactic:
rw [← mul_assoc] at hj
Proof state after:
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
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
Tactic:
nth_rw 3 [← pow_one 3] at hj
Proof state after:
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
hj : 3 * n = 3 ^ k * 3 ^ 1 * r
t1 : j = 3 * r
⊢ False
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
hj : 3 * n = 3 ^ k * 3 ^ 1 * r
t1 : j = 3 * r
⊢ False
Tactic:
rw [← pow_add] at hj
Proof state after:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
⊢ False
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
⊢ False
Tactic:
have g : 3 ^ (k + 1) ∣ 3 * n := by use r;
Proof state after:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ False
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ False
Tactic:
have combine : 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n := by constructor; exact g; exact h2
Proof state after:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
combine : 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ False
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
combine : 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ False
Tactic:
simp at combine
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
⊢ 3 ^ (k + 1) ∣ 3 * n
Tactic:
use r
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof state before:
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
Tactic:
constructor
Proof state after:
case left
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ (k + 1) ∣ 3 * n

case right
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case left
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ (k + 1) ∣ 3 * n

case right
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
Tactic:
exact g
Proof state after:
case right
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case right
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
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
Tactic:
exact h2
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case intro.intro.inr.intro.intro.inr.inl
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 : ℕ
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
rw [t2] at hj
Proof state after:
case intro.intro.inr.intro.intro.inr.inl
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 + 1)
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case intro.intro.inr.intro.intro.inr.inl
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 + 1)
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
use k
Proof state after:
case 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 + 1)
t2 : j = 3 * r + 1
⊢ ∃ b, 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * b + 1) ∨ 3 * ↑n = 3 ^ k * (3 * b + 2))
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case 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 + 1)
t2 : j = 3 * r + 1
⊢ ∃ b, 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * b + 1) ∨ 3 * ↑n = 3 ^ k * (3 * b + 2))
Tactic:
use r
Proof state after:
case 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 + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case 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 + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))
Tactic:
constructor
Proof state after:
case h.left
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 + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k

case h.right
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 + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case h.left
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 + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k

case h.right
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 + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
exact s2
Proof state after:
case h.right
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 + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case h.right
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 + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
left
Proof state after:
case h.right.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 + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1)
Theorem: ℤθ.hMul_three_expansion
Proof state before:
case h.right.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 + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1)
Tactic:
exact_mod_cast hj
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof state before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
have p : n ≥ 0 ∨ n < 0 := by
  have w := lt_or_le 0 n
  cases' w with w1 w2
  left; rw [ge_iff_le]; rw [le_iff_lt_or_eq]; left; exact w1
  rw [le_iff_lt_or_eq] at w2
  cases' w2 with w3 w4
  right; exact w3
  left; rw [ge_iff_le]; rw [le_iff_lt_or_eq]; right; exact Eq.symm w4
Proof state after:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p : n ≥ 0 ∨ n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p : n ≥ 0 ∨ n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
cases' p with p1 p2
Proof state after:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p1 : n ≥ 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p1 : n ≥ 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
rw [ge_iff_le] at p1
Proof state after:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p1 : 0 ≤ n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p1 : 0 ≤ n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
rw [le_iff_eq_or_lt] at p1
Proof state after:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p1 : 0 = n ∨ 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p1 : 0 = n ∨ 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
cases' p1 with p3 p4
Proof state after:
case inl.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
have t : n = 0 ∧ n ≠ 0 := by constructor; exact Eq.symm p3; exact h
Proof state after:
case inl.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
t : n = 0 ∧ n ≠ 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
t : n = 0 ∧ n ≠ 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
exfalso
Proof state after:
case inl.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
t : n = 0 ∧ n ≠ 0
⊢ False

case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
t : n = 0 ∧ n ≠ 0
⊢ False

case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
simp at t
Proof state after:
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
have p5 : 1 ≤ Int.toNat n :=
  by
  have s := Nat.eq_zero_or_pos (Int.toNat n)
  cases' s with s1 s2
  exfalso
  simp at s1
  push_neg at s1
  apply lt_irrefl 0 (lt_of_lt_of_le p4 s1)
exact s2
Proof state after:
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
have r1 := hMul_three_expansion (Int.toNat n) p5
Proof state after:
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
r1 : ∃ 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
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
r1 : ∃ 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
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
cases' r1 with j hj
Proof state after:
case inl.inr.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inr.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
cases' hj with g hg
Proof state after:
case inl.inr.intro.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg : 1 ≤ j ∧ (3 * ↑(Int.toNat n) = 3 ^ j * (3 * g + 1) ∨ 3 * ↑(Int.toNat n) = 3 ^ j * (3 * g + 2))
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inr.intro.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg : 1 ≤ j ∧ (3 * ↑(Int.toNat n) = 3 ^ j * (3 * g + 1) ∨ 3 * ↑(Int.toNat n) = 3 ^ j * (3 * g + 2))
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
cases' hg with hg0 hg12
Proof state after:
case inl.inr.intro.intro.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inl.inr.intro.intro.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
use j
Proof state after:
case h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ ∃ b, 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * b + 1) ∨ 3 * n = 3 ^ j * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ ∃ b, 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * b + 1) ∨ 3 * n = 3 ^ j * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
use g
Proof state after:
case h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * g + 1) ∨ 3 * n = 3 ^ j * (3 * g + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * g + 1) ∨ 3 * n = 3 ^ j * (3 * g + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
constructor
Proof state after:
case h.left
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 1 ≤ j

case h.right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 3 * n = 3 ^ j * (3 * g + 1) ∨ 3 * n = 3 ^ j * (3 * g + 2)

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))