internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * - -q))).f % 3 = 1 ∧ (↑(unit ^ (3 * - -q))).g % 3 = 0 ∧ (↑(unit ^ (3 * - -q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [neg_neg] at p2
Proof state after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
exact p2
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inl
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h1 : 0 < q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
specialize p (Int.toNat q)
Proof state after:
case inl
a b c : ℤθ
q : ℤ
h1 : 0 < q
p :
  ((↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inl
a b c : ℤθ
q : ℤ
h1 : 0 < q
p :
  ((↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
cases' p with p1 p2
Proof state after:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [Int.toNat_of_nonneg (le_of_lt h1)] at p1
Proof state after:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Theorem: ℤθ.unit_zpow_zero_mod_three
Proof state before:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
exact p1
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
⊢ ∀ (k : ℤ), (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
intro k
Proof state after:
a b c : ℤθ
k : ℤ
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
have w :
  ((unit ^ (3 * k + 1) : ℤθˣ) : ℤθ) = ((unit ^ (3 * k) : ℤθˣ) : ℤθ) * ((unit ^ 1 : ℤθˣ) : ℤθ) :=
  by
  rw [zpow_add]
  norm_cast
Proof state after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
have g := unit_zpow_zero_mod_three
Proof state after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g : ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g : ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
specialize g k
Proof state after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g : (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g : (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' g with g1 g23
Proof state after:
case intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g23 : (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g23 : (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' g23 with g2 g3
Proof state after:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
have t1 := y_mod_three ((unit ^ (3 * k) : ℤθˣ) : ℤθ).f 1 g1
Proof state after:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
t1 : ∃ k_1, (↑(unit ^ (3 * k))).f = 3 * k_1 + 1
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
t1 : ∃ k_1, (↑(unit ^ (3 * k))).f = 3 * k_1 + 1
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' t1 with j1 hj1
Proof state after:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
have t2 := y_mod_three ((unit ^ (3 * k) : ℤθˣ) : ℤθ).g 0 g2
Proof state after:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
t2 : ∃ k_1, (↑(unit ^ (3 * k))).g = 3 * k_1 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
t2 : ∃ k_1, (↑(unit ^ (3 * k))).g = 3 * k_1 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' t2 with j2 hj2
Proof state after:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [add_zero] at hj2
Proof state after:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
have t3 := y_mod_three ((unit ^ (3 * k) : ℤθˣ) : ℤθ).h 0 g3
Proof state after:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
t3 : ∃ k_1, (↑(unit ^ (3 * k))).h = 3 * k_1 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
t3 : ∃ k_1, (↑(unit ^ (3 * k))).h = 3 * k_1 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' t3 with j3 hj3
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3 + 0
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [add_zero] at hj3
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
have s : ((unit ^ (3 * k) : ℤθˣ) : ℤθ) = ⟨3 * j1 + 1, 3 * j2, 3 * j3⟩ :=
  by
  ext <;> dsimp
  exact hj1; exact hj2; exact hj3
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
j1 : ℤ
hj1 : (↑(unit ^ (3 * k))).f = 3 * j1 + 1
j2 : ℤ
hj2 : (↑(unit ^ (3 * k))).g = 3 * j2
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
clear g1 g2 g3 hj1 hj2 hj3
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [s] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 1)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑(unit ^ 1)
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 1)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑(unit ^ 1)
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [pow_one] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 1)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑unit
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 1)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑unit
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [unit_l] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 1)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * { f := -1, g := -3, h := -1 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 1)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * { f := -1, g := -3, h := -1 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [hMul_mule_3] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 1)) =
    {
      f :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -1, g := -3, h := -1 }.f +
              6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.h -
            2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.h -
          2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.g,
      g :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -1, g := -3, h := -1 }.g +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.f +
              16 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.h -
            6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.h -
          6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.g,
      h :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -1, g := -3, h := -1 }.h +
                  { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.f +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.g +
              3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.h -
            3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.h -
          3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.g }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2