internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro
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 }
w :
  (↑(unit ^ (3 * (b + 1)))).f = -23 - c1 * 69 + c3 * 108 + c2 * 90 ∧
    (↑(unit ^ (3 * (b + 1)))).g = -63 - c1 * 189 + c3 * 414 + c2 * 201 ∧
      (↑(unit ^ (3 * (b + 1)))).h = -15 - c1 * 45 + (c3 * 363 - c2 * 54)
this : 3 + b * 3 = 3 * (b + 1)
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
obtain ⟨f1,f2,f3⟩:=w
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro
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 = -23 - c1 * 69 + c3 * 108 + c2 * 90
f2 : (↑(unit ^ (3 * (b + 1)))).g = -63 - c1 * 189 + c3 * 414 + c2 * 201
f3 : (↑(unit ^ (3 * (b + 1)))).h = -15 - c1 * 45 + (c3 * 363 - c2 * 54)
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro
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 = -23 - c1 * 69 + c3 * 108 + c2 * 90
f2 : (↑(unit ^ (3 * (b + 1)))).g = -63 - c1 * 189 + c3 * 414 + c2 * 201
f3 : (↑(unit ^ (3 * (b + 1)))).h = -15 - c1 * 45 + (c3 * 363 - c2 * 54)
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
apply_fun (fun x => x%3) at f1 f2 f3
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro
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
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro.intro.intro.intro.intro
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
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
rw [f1,f2,f3]
Proof state after:
case left.succ.intro.intro.intro.intro.intro.intro.intro
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
⊢ (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3 = 1 ∧
    (-63 - c1 * 189 + c3 * 414 + c2 * 201) % 3 = 0 ∧ (-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
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
⊢ (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3 = 1 ∧
    (-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.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
⊢ (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3 = 1

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
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.zero
a b c : ℤθ
⊢ (↑(unit ^ (3 * ↑Nat.zero))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑Nat.zero))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑Nat.zero))).h % 3 = 0
Tactic:
exact unit_pow_zero
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
⊢ Nat.succ b = b + 1
Tactic:
rfl
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
⊢ ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
Tactic:
norm_cast
Proof state after:
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
⊢ unit ^ (3 * (b + 1)) = unit ^ (3 * b) * unit ^ 3
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
⊢ unit ^ (3 * (b + 1)) = unit ^ (3 * b) * unit ^ 3
Tactic:
rw [mul_add, mul_one, pow_add]
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
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
⊢ (↑(unit ^ (3 * b))).f % 3 = 1
Tactic:
norm_cast
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
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
⊢ (↑(unit ^ (3 * b))).g % 3 = 0
Tactic:
norm_cast
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
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
⊢ (↑(unit ^ (3 * b))).h % 3 = 0
Tactic:
norm_cast
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
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
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
⊢ ↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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
⊢ (↑(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
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 }
w :
  (↑(unit ^ (3 + b * 3))).f = -23 - c1 * 69 + c3 * 108 + c2 * 90 ∧
    (↑(unit ^ (3 + b * 3))).g = -63 - c1 * 189 + c3 * 414 + c2 * 201 ∧
      (↑(unit ^ (3 + b * 3))).h = -15 - c1 * 45 + (c3 * 363 - c2 * 54)
⊢ 3 + b * 3 = 3 * (b + 1)
Tactic:
ring
Proof state after:
no goals
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
⊢ (-23 - c1 * 69 + c3 * 108 + c2 * 90) % 3 = 1
Tactic:
rw [Int.add_emod,Int.add_emod _ (c3*108),Int.sub_emod, Int.mul_emod _ 69,Int.mul_emod _ 108,Int.mul_emod _ 90]
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
⊢ (((-23 % 3 - c1 % 3 * (69 % 3) % 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
⊢ (((-23 % 3 - c1 % 3 * (69 % 3) % 3) % 3 + c3 % 3 * (108 % 3) % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1
Tactic:
have : (69:ℤ) %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
⊢ (((-23 % 3 - c1 % 3 * (69 % 3) % 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
⊢ (((-23 % 3 - c1 % 3 * (69 % 3) % 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
⊢ (((-23 % 3 - c1 % 3 * 0 % 3) % 3 + c3 % 3 * (108 % 3) % 3) % 3 + c2 % 3 * (90 % 3) % 3) % 3 = 1