Theorem: ℤθ.zmul_three_expansion (Mordell4/CubicRing.lean)

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

State before:
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))
Tactic:
exact hg0
State after:
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))

State before:
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))
Tactic:
have coe_coe : (Int.toNat n : ℤ) = n :=
  haveI finale := le_of_lt p4
  Int.toNat_of_nonneg finale
State after:
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)
coe_coe : ↑(Int.toNat n) = n
⊢ 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))

State before:
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)
coe_coe : ↑(Int.toNat n) = n
⊢ 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:
cases' hg12 with hg1 hg2
State after:
case h.right.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 3 * n = 3 ^ j * (3 * g + 1) ∨ 3 * n = 3 ^ j * (3 * g + 2)

case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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))

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

case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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:
rw [coe_coe] at hg1
State after:
case h.right.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg1 : 3 * n = 3 ^ j * (3 * g + 1)
⊢ 3 * n = 3 ^ j * (3 * g + 1) ∨ 3 * n = 3 ^ j * (3 * g + 2)

case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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))

State before:
case h.right.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg1 : 3 * n = 3 ^ j * (3 * g + 1)
⊢ 3 * n = 3 ^ j * (3 * g + 1) ∨ 3 * n = 3 ^ j * (3 * g + 2)

case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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:
left
State after:
case h.right.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg1 : 3 * n = 3 ^ j * (3 * g + 1)
⊢ 3 * n = 3 ^ j * (3 * g + 1)

case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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))

State before:
case h.right.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg1 : 3 * n = 3 ^ j * (3 * g + 1)
⊢ 3 * n = 3 ^ j * (3 * g + 1)

case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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:
exact hg1
State after:
case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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))

State before:
case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 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)
⊢ 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:
rw [coe_coe] at hg2
State after:
case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg2 : 3 * 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))

State before:
case h.right.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg2 : 3 * 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))
Tactic:
right
State after:
case h.right.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg2 : 3 * n = 3 ^ j * (3 * g + 2)
⊢ 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))

State before:
case h.right.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
j : ℕ
g : ℤ
hg0 : 1 ≤ j
coe_coe : ↑(Int.toNat n) = n
hg2 : 3 * n = 3 ^ j * (3 * g + 2)
⊢ 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:
exact hg2
State after:
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))

State before:
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 p6 : 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_le_of_lt  s1 p2)
  exact s2
State after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

State before:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
have r2 := hMul_three_expansion (Int.toNat (-n)) p6
State after:
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))

State before:
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))
Tactic:
cases' r2 with j hj
State after:
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))

State before:
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))
Tactic:
cases' hj with g hg
State after:
case inr.intro.intro
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 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))

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

State before:
case inr.intro.intro.intro
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)
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
have coe_coe : -(Int.toNat (-n) : ℤ) = n :=
  by
  rw [← neg_inj]; rw [neg_neg]
  rw [← neg_zero] at p2 ; rw [lt_neg] at p2
  exact Int.toNat_of_nonneg (le_of_lt p2)
State after:
case inr.intro.intro.intro
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
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

State before:
case inr.intro.intro.intro
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
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
Tactic:
use j
State after:
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))

State before:
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))
Tactic:
cases' hg12 with hg1 hg2
State after:
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))

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
have w := lt_or_le 0 n
State after:
a b c : ℤθ
n : ℤ
h : n ≠ 0
w : 0 < n ∨ n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
w : 0 < n ∨ n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
cases' w with w1 w2
State after:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ n ≥ 0 ∨ n < 0

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ n ≥ 0 ∨ n < 0

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
left
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ n ≥ 0

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ n ≥ 0

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
rw [ge_iff_le]
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 ≤ n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 ≤ n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
rw [le_iff_lt_or_eq]
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 < n ∨ 0 = n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 < n ∨ 0 = n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
left
State after:
case inl.h.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 < n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inl.h.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 < n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
exact w1
State after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
rw [le_iff_lt_or_eq] at w2
State after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n < 0 ∨ n = 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n < 0 ∨ n = 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
cases' w2 with w3 w4
State after:
case inr.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
w3 : n < 0
⊢ n ≥ 0 ∨ n < 0

case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inr.inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
w3 : n < 0
⊢ n ≥ 0 ∨ n < 0

case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
right
State after:
case inr.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w3 : n < 0
⊢ n < 0

case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inr.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w3 : n < 0
⊢ n < 0

case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
exact w3
State after:
case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0

State before:
case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
left
State after:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0

State before:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0
Tactic:
rw [ge_iff_le]
State after:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 ≤ n

State before:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 ≤ n
Tactic:
rw [le_iff_lt_or_eq]
State after:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 < n ∨ 0 = n

State before:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 < n ∨ 0 = n
Tactic:
right
State after:
case inr.inr.h.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 = n

State before:
case inr.inr.h.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 = n
Tactic:
exact Eq.symm w4
State after:
no goals

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n = 0 ∧ n ≠ 0
Tactic:
constructor
State after:
case left
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n = 0

case right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n ≠ 0

State before:
case left
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n = 0

case right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n ≠ 0
Tactic:
exact Eq.symm p3
State after:
case right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n ≠ 0

State before:
case right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n ≠ 0
Tactic:
exact h
State after:
no goals

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ 1 ≤ Int.toNat n
Tactic:
have s := Nat.eq_zero_or_pos (Int.toNat n)
State after:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s : Int.toNat n = 0 ∨ Int.toNat n > 0
⊢ 1 ≤ Int.toNat n

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s : Int.toNat n = 0 ∨ Int.toNat n > 0
⊢ 1 ≤ Int.toNat n
Tactic:
cases' s with s1 s2
State after:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s1 : Int.toNat n = 0
⊢ 1 ≤ Int.toNat n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n

State before:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s1 : Int.toNat n = 0
⊢ 1 ≤ Int.toNat n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n
Tactic:
exfalso
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s1 : Int.toNat n = 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s1 : Int.toNat n = 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n
Tactic:
simp at s1
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s1 : n ≤ 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s1 : n ≤ 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n
Tactic:
apply lt_irrefl 0 (lt_of_lt_of_le p4 s1)
State after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n

State before:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n
Tactic:
exact s2
State after:
no goals

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ 1 ≤ Int.toNat (-n)
Tactic:
have s := Nat.eq_zero_or_pos (Int.toNat (-n))
State after:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s : Int.toNat (-n) = 0 ∨ Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s : Int.toNat (-n) = 0 ∨ Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
Tactic:
cases' s with s1 s2
State after:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : Int.toNat (-n) = 0
⊢ 1 ≤ Int.toNat (-n)

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)

State before:
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : Int.toNat (-n) = 0
⊢ 1 ≤ Int.toNat (-n)

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
Tactic:
exfalso
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : Int.toNat (-n) = 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : Int.toNat (-n) = 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
Tactic:
simp at s1
State after:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : 0 ≤ n
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)

State before:
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : 0 ≤ n
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
Tactic:
apply lt_irrefl 0 (lt_of_le_of_lt  s1 p2)
State after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)

State before:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
Tactic:
exact s2
State after:
no goals

State before:
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)
⊢ -↑(Int.toNat (-n)) = n
Tactic:
rw [← neg_inj]
State after:
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)
⊢ - -↑(Int.toNat (-n)) = -n

State before:
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)
⊢ - -↑(Int.toNat (-n)) = -n
Tactic:
rw [neg_neg]
State after:
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)
⊢ ↑(Int.toNat (-n)) = -n

State before:
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)
⊢ ↑(Int.toNat (-n)) = -n
Tactic:
rw [← neg_zero] at p2
State after:
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)
⊢ ↑(Int.toNat (-n)) = -n

State before:
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)
⊢ ↑(Int.toNat (-n)) = -n
Tactic:
rw [lt_neg] at p2
State after:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : 0 < -n
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)
⊢ ↑(Int.toNat (-n)) = -n

State before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : 0 < -n
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)
⊢ ↑(Int.toNat (-n)) = -n
Tactic:
exact Int.toNat_of_nonneg (le_of_lt p2)
State after:
no goals

State before:
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))
Tactic:
use-(g + 1)
State after:
case h
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)
⊢ 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2))

State before:
case h
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)
⊢ 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2))
Tactic:
constructor
State after:
case h.left
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)
⊢ 1 ≤ j

case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.left
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)
⊢ 1 ≤ j

case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
exact hg0
State after:
case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
right
State after:
case h.right.h
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
rw [← neg_inj] at hg1
State after:
case h.right.h
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)
hg1 : -(3 * ↑(Int.toNat (-n))) = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
hg1 : -(3 * ↑(Int.toNat (-n))) = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
rw [mul_comm] at hg1
State after:
case h.right.h
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)
hg1 : -(↑(Int.toNat (-n)) * 3) = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
hg1 : -(↑(Int.toNat (-n)) * 3) = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
rw [← neg_mul] at hg1
State after:
case h.right.h
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)
hg1 : -↑(Int.toNat (-n)) * 3 = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
hg1 : -↑(Int.toNat (-n)) * 3 = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
rw [coe_coe] at hg1
State after:
case h.right.h
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)
hg1 : n * 3 = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
hg1 : n * 3 = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
rw [mul_comm] at hg1
State after:
case h.right.h
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)
hg1 : 3 * n = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
hg1 : 3 * n = -(3 ^ j * (3 * g + 1))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
rw [hg1]
State after:
case h.right.h
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)
hg1 : 3 * n = -(3 ^ j * (3 * g + 1))
⊢ -(3 ^ j * (3 * g + 1)) = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right.h
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)
hg1 : 3 * n = -(3 ^ j * (3 * g + 1))
⊢ -(3 ^ j * (3 * g + 1)) = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
ring
State after:
no goals

State before:
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))
Tactic:
use-(g + 1)
State after:
case h
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)
⊢ 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2))

State before:
case h
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)
⊢ 1 ≤ j ∧ (3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2))
Tactic:
constructor
State after:
case h.left
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)
⊢ 1 ≤ j

case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.left
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)
⊢ 1 ≤ j

case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
exact hg0
State after:
case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)

State before:
case h.right
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1) ∨ 3 * n = 3 ^ j * (3 * -(g + 1) + 2)
Tactic:
left
State after:
case h.right.h
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
rw [← neg_inj] at hg2
State after:
case h.right.h
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)
hg2 : -(3 * ↑(Int.toNat (-n))) = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
hg2 : -(3 * ↑(Int.toNat (-n))) = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
rw [mul_comm] at hg2
State after:
case h.right.h
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)
hg2 : -(↑(Int.toNat (-n)) * 3) = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
hg2 : -(↑(Int.toNat (-n)) * 3) = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
rw [← neg_mul] at hg2
State after:
case h.right.h
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)
hg2 : -↑(Int.toNat (-n)) * 3 = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
hg2 : -↑(Int.toNat (-n)) * 3 = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
rw [coe_coe] at hg2
State after:
case h.right.h
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)
hg2 : n * 3 = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
hg2 : n * 3 = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
rw [mul_comm] at hg2
State after:
case h.right.h
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)
hg2 : 3 * n = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
hg2 : 3 * n = -(3 ^ j * (3 * g + 2))
⊢ 3 * n = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
rw [hg2]
State after:
case h.right.h
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)
hg2 : 3 * n = -(3 ^ j * (3 * g + 2))
⊢ -(3 ^ j * (3 * g + 2)) = 3 ^ j * (3 * -(g + 1) + 1)

State before:
case h.right.h
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)
hg2 : 3 * n = -(3 ^ j * (3 * g + 2))
⊢ -(3 ^ j * (3 * g + 2)) = 3 ^ j * (3 * -(g + 1) + 1)
Tactic:
ring
State after:
no goals