internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
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
⊢ 54 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right
a b c : ℤθ
k : ℕ
⊢ (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
Tactic:
induction' k with b hb
Proof state after:
case right.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

case right.succ
a b✝ c : ℤθ
b : ℕ
hb : (↑(unit ^ (3 * -↑b))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ
a b✝ c : ℤθ
b : ℕ
hb : (↑(unit ^ (3 * -↑b))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Tactic:
cases' hb with h1 h23
Proof state after:
case right.succ.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h23 : (↑(unit ^ (3 * -↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h23 : (↑(unit ^ (3 * -↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Tactic:
cases' h23 with h2 h3
Proof state after:
case right.succ.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
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.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
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Tactic:
have p : b.succ = b + 1 := by rfl
Proof state after:
case right.succ.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
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.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
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
Tactic:
rw [p]
Proof state after:
case right.succ.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
⊢ (↑(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 right.succ.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
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
have w :
  ((unit ^ ((3 : ℤ) * -(b + 1 : ℤ)) : ℤθˣ) : ℤθ) =
    ((unit ^ (3 * -(b : ℤ)) : ℤθˣ) : ℤθ) * ((unit ^ (-3 : ℤ) : ℤθˣ) : ℤθ) :=
  by
  rw [neg_add, mul_add, mul_neg_one, zpow_add]
  norm_cast
Proof state after:
case right.succ.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))
⊢ (↑(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 right.succ.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))
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
have r1 := y_mod_three ((unit ^ ((3 : ℤ) * -(b : ℤ)) : ℤθˣ) : ℤθ).f 1 h1
Proof state after:
case right.succ.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))
r1 : ∃ k, (↑(unit ^ (3 * -↑b))).f = 3 * k + 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 right.succ.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))
r1 : ∃ k, (↑(unit ^ (3 * -↑b))).f = 3 * k + 1
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
cases' r1 with c1 hc1
Proof state after:
case right.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))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 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 right.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))
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
have r2 := y_mod_three ((unit ^ ((3 : ℤ) * -(b : ℤ)) : ℤθˣ) : ℤθ).g 0 h2
Proof state after:
case right.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))
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
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.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))
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 right.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))
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 right.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))
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 right.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))
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 right.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))
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 h3
Proof state after:
case right.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))
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 right.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))
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 right.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))
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 right.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))
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 right.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))
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 right.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))
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 right.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))
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 right.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))
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 right.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
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 right.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
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_inv_cubed] at w
Proof state after:
case right.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
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 := 10591, g := 5553, h := 2139 }
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 right.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
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 := 10591, g := 5553, h := 2139 }
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 right.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
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 := 10591, g := 5553, h := 2139 }.f +
              6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.h -
            2 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.h -
          2 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.g,
      g :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := 10591, g := 5553, h := 2139 }.g +
                { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.f +
              16 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.h -
            6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.h -
          6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.g,
      h :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := 10591, g := 5553, h := 2139 }.h +
                  { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.f +
                { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.g +
              3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.h -
            3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.h -
          3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.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 right.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
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) * 10591 + 6 * (3 * c3) * 2139 - 2 * (3 * c2) * 2139 - 2 * (3 * c3) * 5553,
      g := (3 * c1 + 1) * 5553 + 3 * c2 * 10591 + 16 * (3 * c3) * 2139 - 6 * (3 * c2) * 2139 - 6 * (3 * c3) * 5553,
      h :=
        (3 * c1 + 1) * 2139 + 3 * c3 * 10591 + 3 * c2 * 5553 + 3 * (3 * c3) * 2139 - 3 * (3 * c2) * 2139 -
          3 * (3 * c3) * 5553 }
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 right.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
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 := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
      h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0