internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.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
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
r2 : ∃ k, (↑(unit ^ (3 * b))).g = 3 * k + 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
cases' r2 with c2 hc2
Proof state after:
case left.succ.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
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 + 0
⊢ (↑(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
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 + 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
rw [add_zero] at hc2
Proof state after:
case left.succ.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
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
⊢ (↑(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
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
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have r3 := y_mod_three (unit ^ (3 * b) : ℤθ).h 0 t3
Proof state after:
case left.succ.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
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
r3 : ∃ k, (↑(unit ^ (3 * b))).h = 3 * k + 0
⊢ (↑(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
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
r3 : ∃ k, (↑(unit ^ (3 * b))).h = 3 * k + 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
cases' r3 with c3 hc3
Proof state after:
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
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 + 0
⊢ (↑(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
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 + 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
rw [add_zero] at hc3
Proof state after:
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
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 + 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
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 + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have s : (unit ^ (3 * b) : ℤθ) = ⟨3 * c1 + 1, 3 * c2, 3 * c3⟩ :=
  by
  ext <;> dsimp
  exact hc1; exact hc2; exact hc3
Proof state after:
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
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
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(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
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
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
rw [s] at w
Proof state after:
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 : ℤ
w : ↑(unit ^ (3 * (b + 1))) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 } * ↑unit ^ 3
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(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
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 : ℤ
w : ↑(unit ^ (3 * (b + 1))) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 } * ↑unit ^ 3
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
rw [unit_cubed] at w
Proof state after:
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 : ℤ
w : ↑(unit ^ (3 * (b + 1))) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 } * { f := -23, g := -63, h := -15 }
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(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
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 : ℤ
w : ↑(unit ^ (3 * (b + 1))) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 } * { f := -23, g := -63, h := -15 }
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
rw [hMul_mule_3] at w
Proof state after:
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 : ℤ
w :
  ↑(unit ^ (3 * (b + 1))) =
    {
      f :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := -23, g := -63, h := -15 }.g }
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(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
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 : ℤ
w :
  ↑(unit ^ (3 * (b + 1))) =
    { f := (3 * c1 + 1) * -23 + 6 * (3 * c3) * -15 - 2 * (3 * c2) * -15 - 2 * (3 * c3) * -63,
      g := (3 * c1 + 1) * -63 + 3 * c2 * -23 + 16 * (3 * c3) * -15 - 6 * (3 * c2) * -15 - 6 * (3 * c3) * -63,
      h :=
        (3 * c1 + 1) * -15 + 3 * c3 * -23 + 3 * c2 * -63 + 3 * (3 * c3) * -15 - 3 * (3 * c2) * -15 -
          3 * (3 * c3) * -63 }
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
ring_nf at w
Proof state after:
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 * 3)) =
    { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
      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
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, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
      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:
rw [ℤθ.ext_iff] at w
Proof state after:
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 * 3))).f =
      { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
          h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.f ∧
    (↑(unit ^ (3 + b * 3))).g =
        { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
            h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.g ∧
      (↑(unit ^ (3 + b * 3))).h =
        { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
            h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.h
⊢ (↑(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
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 =
      { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
          h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.f ∧
    (↑(unit ^ (3 + b * 3))).g =
        { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
            h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.g ∧
      (↑(unit ^ (3 + b * 3))).h =
        { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
            h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.h
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
dsimp at w
Proof state after:
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 * 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)
⊢ (↑(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
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)
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have : 3 + b*3 = 3*(b+1):= by ring
Proof state after:
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 * 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)
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
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 * 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)
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:
rw [this] at w
Proof state after:
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