internlm/Lean-Github huggingface dataset:
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_zero] at p2
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 [lt_neg] at p2
Proof 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
Theorem: ℤθ.zmul_three_expansion
Proof 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)
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof 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)
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
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))
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
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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
no goals
Theorem: ℤθ.zmul_three_expansion
Proof 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)
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
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))
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
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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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]
Proof 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)
Theorem: ℤθ.zmul_three_expansion
Proof 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
Proof state after:
no goals
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
⊢ ↑unit ^ 6 = { f := -1901, g := -4842, h := -336 }
Tactic:
have elem : 6 = 3 + 3 := by norm_num;
Proof state after:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ ↑unit ^ 6 = { f := -1901, g := -4842, h := -336 }
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ ↑unit ^ 6 = { f := -1901, g := -4842, h := -336 }
Tactic:
rw [elem]
Proof state after:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ ↑unit ^ (3 + 3) = { f := -1901, g := -4842, h := -336 }
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ ↑unit ^ (3 + 3) = { f := -1901, g := -4842, h := -336 }
Tactic:
rw [pow_add]
Proof state after:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ ↑unit ^ 3 * ↑unit ^ 3 = { f := -1901, g := -4842, h := -336 }
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ ↑unit ^ 3 * ↑unit ^ 3 = { f := -1901, g := -4842, h := -336 }
Tactic:
rw [unit_cubed]
Proof state after:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ { f := -23, g := -63, h := -15 } * { f := -23, g := -63, h := -15 } = { f := -1901, g := -4842, h := -336 }
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ { f := -23, g := -63, h := -15 } * { f := -23, g := -63, h := -15 } = { f := -1901, g := -4842, h := -336 }
Tactic:
rw [hMul_mule_3]
Proof state after:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ {
      f :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -1901, g := -4842, h := -336 }
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ {
      f :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -1901, g := -4842, h := -336 }
Tactic:
dsimp
Proof state after:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ { f := -23 * -23 + 6 * -15 * -15 - 2 * -63 * -15 - 2 * -15 * -63,
      g := -23 * -63 + -63 * -23 + 16 * -15 * -15 - 6 * -63 * -15 - 6 * -15 * -63,
      h := -23 * -15 + -15 * -23 + -63 * -63 + 3 * -15 * -15 - 3 * -63 * -15 - 3 * -15 * -63 } =
    { f := -1901, g := -4842, h := -336 }
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
elem : 6 = 3 + 3
⊢ { f := -23 * -23 + 6 * -15 * -15 - 2 * -63 * -15 - 2 * -15 * -63,
      g := -23 * -63 + -63 * -23 + 16 * -15 * -15 - 6 * -63 * -15 - 6 * -15 * -63,
      h := -23 * -15 + -15 * -23 + -63 * -63 + 3 * -15 * -15 - 3 * -63 * -15 - 3 * -15 * -63 } =
    { f := -1901, g := -4842, h := -336 }
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤθ.unit_pow_six
Proof state before:
a b c : ℤθ
⊢ 6 = 3 + 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
⊢ ↑unit ^ 9 = { f := -113633, g := -251019, h := 75015 }
Tactic:
have elem : 9 = 3 + 3 + 3 := by norm_num;
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ 9 = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ 9 = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [elem]
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3 + 3) = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3 + 3) = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [pow_add]
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Tactic:
have elem1 : 3 + 3 = 6 := by norm_num;
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [elem1]
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [unit_cubed]
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [unit_pow_six]
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901, g := -4842, h := -336 } * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901, g := -4842, h := -336 } * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [hMul_mule_3]
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ {
      f :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -113633, g := -251019, h := 75015 }