internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.left
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝¹ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝ : 189 % 3 = 0
this : 414 % 3 = 0
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (201 % 3) % 3) % 3 = 0
Tactic:
have : (201:ℤ) %3 = 0:=by norm_num
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.left
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 189 % 3 = 0
this✝ : 414 % 3 = 0
this : 201 % 3 = 0
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (201 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.left
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 189 % 3 = 0
this✝ : 414 % 3 = 0
this : 201 % 3 = 0
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (201 % 3) % 3) % 3 = 0
Tactic:
rw [this]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.left
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 189 % 3 = 0
this✝ : 414 % 3 = 0
this : 201 % 3 = 0
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * 0 % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.left
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 189 % 3 = 0
this✝ : 414 % 3 = 0
this : 201 % 3 = 0
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * 0 % 3) % 3 = 0
Tactic:
norm_num
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
⊢ 189 % 3 = 0
Tactic:
norm_num
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this : 189 % 3 = 0
⊢ 414 % 3 = 0
Tactic:
norm_num
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝¹ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝ : 189 % 3 = 0
this : 414 % 3 = 0
⊢ 201 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
⊢ (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3 = 0
Tactic:
rw [Int.add_emod,Int.sub_emod,Int.sub_emod (c3*363), Int.mul_emod _ 363,Int.mul_emod _ 54,Int.mul_emod _ 45]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
⊢ ((-15 % 3 - c1 % 3 * (45 % 3) % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
⊢ ((-15 % 3 - c1 % 3 * (45 % 3) % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Tactic:
have : (45:ℤ) %3 = 0:=by norm_num
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this : 45 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * (45 % 3) % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this : 45 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * (45 % 3) % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Tactic:
rw [this]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this : 45 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this : 45 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Tactic:
have : (363:ℤ) %3 = 0:=by norm_num
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝¹ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝ : 45 % 3 = 0
this : 363 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝¹ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝ : 45 % 3 = 0
this : 363 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * (363 % 3) % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Tactic:
rw [this]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝¹ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝ : 45 % 3 = 0
this : 363 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝¹ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝ : 45 % 3 = 0
this : 363 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Tactic:
have : (54:ℤ) %3 = 0:=by norm_num
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 45 % 3 = 0
this✝ : 363 % 3 = 0
this : 54 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 45 % 3 = 0
this✝ : 363 % 3 = 0
this : 54 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (54 % 3) % 3) % 3) % 3 = 0
Tactic:
rw [this]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 45 % 3 = 0
this✝ : 363 % 3 = 0
this : 54 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * 0 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.right.right
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝² : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this✝¹ : 45 % 3 = 0
this✝ : 363 % 3 = 0
this : 54 % 3 = 0
⊢ ((-15 % 3 - c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * 0 % 3) % 3) % 3 = 0
Tactic:
norm_num
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
⊢ 45 % 3 = 0
Tactic:
norm_num
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
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
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 }
this✝ : 3 + b * 3 = 3 * (b + 1)
f1 : (↑(unit ^ (3 * (b + 1)))).f % 3 = (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3
f2 : (↑(unit ^ (3 * (b + 1)))).g % 3 = (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3
f3 : (↑(unit ^ (3 * (b + 1)))).h % 3 = (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3
this : 45 % 3 = 0
⊢ 363 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals