internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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)
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.zmul_three_expansion
Proof state before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
have w := lt_or_le 0 n
Proof state after:
a b c : ℤθ
n : ℤ
h : n ≠ 0
w : 0 < n ∨ n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Theorem: ℤθ.zmul_three_expansion
Proof state before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
w : 0 < n ∨ n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
cases' w with w1 w2
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n < 0 ∨ n = 0
⊢ n ≥ 0 ∨ n < 0
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inr.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0 ∨ n < 0
Tactic:
left
Proof state after:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ n ≥ 0
Tactic:
rw [ge_iff_le]
Proof state after:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 ≤ n
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof state after:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 < n ∨ 0 = n
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inr.inr.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 < n ∨ 0 = n
Tactic:
right
Proof state after:
case inr.inr.h.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 = n
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case inr.inr.h.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w4 : n = 0
⊢ 0 = n
Tactic:
exact Eq.symm w4
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof state before:
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n = 0 ∧ n ≠ 0
Tactic:
constructor
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
case right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n ≠ 0
Theorem: ℤθ.zmul_three_expansion
Proof state before:
case right
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
⊢ n ≠ 0
Tactic:
exact h
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof 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)
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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)
Proof state after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
s2 : Int.toNat n > 0
⊢ 1 ≤ Int.toNat n
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof 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))
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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)
Proof state after:
case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof 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