internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
Tactic:
ext <;> dsimp
Proof state after:
case f
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1

case g
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).g = 3 * c2

case h
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).h = 3 * c3
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case f
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1

case g
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).g = 3 * c2

case h
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).h = 3 * c3
Tactic:
exact hc1
Proof state after:
case g
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).g = 3 * c2

case h
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).h = 3 * c3
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case g
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).g = 3 * c2

case h
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).h = 3 * c3
Tactic:
exact hc2
Proof state after:
case h
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).h = 3 * c3
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case h
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
⊢ (↑(unit ^ (3 * -↑b))).h = 3 * c3
Tactic:
exact hc3
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ -3 - ↑b * 3 = 3 * -(↑b + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -(↑b + 1)
⊢ ↑b + 1 = ↑(b + 1)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)) % 3 = 1
Tactic:
rw [Int.add_emod ,Int.add_emod 10591, Int.sub_emod]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 * 31773 % 3) % 3 + (c3 * 5184 % 3 - c2 * 12834 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 * 31773 % 3) % 3 + (c3 * 5184 % 3 - c2 * 12834 % 3) % 3) % 3 = 1
Tactic:
rw [Int.mul_emod c1]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 * 5184 % 3 - c2 * 12834 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 * 5184 % 3 - c2 * 12834 % 3) % 3) % 3 = 1
Tactic:
rw [Int.mul_emod c3,Int.mul_emod c2]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
have : (10591:ℤ) %3 = 1 :=by norm_num
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this : 10591 % 3 = 1
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this : 10591 % 3 = 1
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
rw [this]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this : 10591 % 3 = 1
⊢ ((1 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this : 10591 % 3 = 1
⊢ ((1 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
have : (31773:ℤ) %3 =0 :=by norm_num
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝ : 10591 % 3 = 1
this : 31773 % 3 = 0
⊢ ((1 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝ : 10591 % 3 = 1
this : 31773 % 3 = 0
⊢ ((1 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
rw [this]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝ : 10591 % 3 = 1
this : 31773 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝ : 10591 % 3 = 1
this : 31773 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
have : (5184:ℤ) %3 =0 :=by norm_num
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝¹ : 10591 % 3 = 1
this✝ : 31773 % 3 = 0
this : 5184 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝¹ : 10591 % 3 = 1
this✝ : 31773 % 3 = 0
this : 5184 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
rw [this]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝¹ : 10591 % 3 = 1
this✝ : 31773 % 3 = 0
this : 5184 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝¹ : 10591 % 3 = 1
this✝ : 31773 % 3 = 0
this : 5184 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
have : (12834:ℤ) %3 =0 :=by norm_num
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝² : 10591 % 3 = 1
this✝¹ : 31773 % 3 = 0
this✝ : 5184 % 3 = 0
this : 12834 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝² : 10591 % 3 = 1
this✝¹ : 31773 % 3 = 0
this✝ : 5184 % 3 = 0
this : 12834 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
Tactic:
rw [this]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝² : 10591 % 3 = 1
this✝¹ : 31773 % 3 = 0
this✝ : 5184 % 3 = 0
this : 12834 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * 0 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝² : 10591 % 3 = 1
this✝¹ : 31773 % 3 = 0
this✝ : 5184 % 3 = 0
this : 12834 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * 0 % 3) % 3) % 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 10591 % 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this : 10591 % 3 = 1
⊢ 31773 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝ : 10591 % 3 = 1
this : 31773 % 3 = 0
⊢ 5184 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝¹ : 10591 % 3 = 1
this✝ : 31773 % 3 = 0
this : 5184 % 3 = 0
⊢ 12834 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0
Tactic:
norm_num
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 3 ∣ 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 3 ∣ 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
Tactic:
use 5553 * c1 + (906 * c3 + (-(2243 * c2) + 1851))
Proof state after:
case h
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) = 3 * (5553 * c1 + (906 * c3 + (-(2243 * c2) + 1851)))
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case h
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) = 3 * (5553 * c1 + (906 * c3 + (-(2243 * c2) + 1851)))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.right
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Tactic:
norm_num
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.right
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 3 ∣ 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.right
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 3 ∣ 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
Tactic:
use 2139 * c1 + (349 * c3 + (-(864 * c2) + 713))
Proof state after:
case h
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) = 3 * (2139 * c1 + (349 * c3 + (-(864 * c2) + 713)))
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case h
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) = 3 * (2139 * c1 + (349 * c3 + (-(864 * c2) + 713)))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
a b c : ℤθ
⊢ ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
Tactic:
intro q
Proof state after:
a b c : ℤθ
q : ℤ
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
a b c : ℤθ
q : ℤ
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
have h := lt_or_le 0 q
Proof state after:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
have p := unit_pow_zero_mod_three
Proof state after:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
cases' h with h1 h2
Proof state after:
case inl
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h1 : 0 < q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

case inr
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h2 : q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h2 : q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
specialize p (Int.toNat (-q))
Proof state after:
case inr
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p :
  ((↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p :
  ((↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
cases' p with p1 p2
Proof state after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
have r := neg_le_neg h2
Proof state after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : -0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : -0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [neg_zero] at r
Proof state after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [Int.toNat_of_nonneg r] at p2
Proof state after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * - -q))).f % 3 = 1 ∧ (↑(unit ^ (3 * - -q))).g % 3 = 0 ∧ (↑(unit ^ (3 * - -q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0