internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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 : 69 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (108 % 3) % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Tactic:
have : (108:ℤ) %3 = 0:=by norm_num
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝ : 69 % 3 = 0
this : 108 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (108 % 3) % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝ : 69 % 3 = 0
this : 108 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (108 % 3) % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Tactic:
rw [this]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝ : 69 % 3 = 0
this : 108 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝ : 69 % 3 = 0
this : 108 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Tactic:
have : (90:ℤ) %3 = 0:=by norm_num
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝¹ : 69 % 3 = 0
this✝ : 108 % 3 = 0
this : 90 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝¹ : 69 % 3 = 0
this✝ : 108 % 3 = 0
this : 90 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Tactic:
rw [this]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝¹ : 69 % 3 = 0
this✝ : 108 % 3 = 0
this : 90 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * 0 % 3) % 3 = 1
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro.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✝¹ : 69 % 3 = 0
this✝ : 108 % 3 = 0
this : 90 % 3 = 0
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * 0 % 3) % 3 = 1
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
⊢ 69 % 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 : 69 % 3 = 0
⊢ 108 % 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✝ : 69 % 3 = 0
this : 108 % 3 = 0
⊢ 90 % 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
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
⊢ (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3 = 0 ∧ (-15 - c1 * 45 + (c3 * 363 - c2 * 54)) % 3 = 0
Tactic:
constructor
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
⊢ (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3 = 0

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
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
⊢ (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3 = 0
Tactic:
rw [Int.add_emod,Int.add_emod _ (c3*414),Int.sub_emod, Int.mul_emod _ 189,Int.mul_emod _ 414,Int.mul_emod _ 201]
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
⊢ (((-63 % 3 - c1 % 3 * (189 % 3) % 3) % 3 + c3 % 3 * (414 % 3) % 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
⊢ (((-63 % 3 - c1 % 3 * (189 % 3) % 3) % 3 + c3 % 3 * (414 % 3) % 3) % 3 + c2 % 3 * (201 % 3) % 3) % 3 = 0
Tactic:
have : (189:ℤ) %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
⊢ (((-63 % 3 - c1 % 3 * (189 % 3) % 3) % 3 + c3 % 3 * (414 % 3) % 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
⊢ (((-63 % 3 - c1 % 3 * (189 % 3) % 3) % 3 + c3 % 3 * (414 % 3) % 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
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (414 % 3) % 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
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (414 % 3) % 3) % 3 + c2 % 3 * (201 % 3) % 3) % 3 = 0
Tactic:
have : (414:ℤ) %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
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (414 % 3) % 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
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (414 % 3) % 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
⊢ (((-63 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * 0 % 3) % 3 + c2 % 3 * (201 % 3) % 3) % 3 = 0