Theorem: ℤθ.unit_zpow_one_mod_three (Mordell4/CubicRing.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

State before:
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
Tactic:
dsimp at w
State after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 1)) =
    { f := (3 * j1 + 1) * -1 + 6 * (3 * j3) * -1 - 2 * (3 * j2) * -1 - 2 * (3 * j3) * -3,
      g := (3 * j1 + 1) * -3 + 3 * j2 * -1 + 16 * (3 * j3) * -1 - 6 * (3 * j2) * -1 - 6 * (3 * j3) * -3,
      h := (3 * j1 + 1) * -1 + 3 * j3 * -1 + 3 * j2 * -3 + 3 * (3 * j3) * -1 - 3 * (3 * j2) * -1 - 3 * (3 * j3) * -3 }
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

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 1)) =
    { f := (3 * j1 + 1) * -1 + 6 * (3 * j3) * -1 - 2 * (3 * j2) * -1 - 2 * (3 * j3) * -3,
      g := (3 * j1 + 1) * -3 + 3 * j2 * -1 + 16 * (3 * j3) * -1 - 6 * (3 * j2) * -1 - 6 * (3 * j3) * -3,
      h := (3 * j1 + 1) * -1 + 3 * j3 * -1 + 3 * j2 * -3 + 3 * (3 * j3) * -1 - 3 * (3 * j2) * -1 - 3 * (3 * j3) * -3 }
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:
ring_nf at w
State after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  ↑(unit ^ (1 + k * 3)) = { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  ↑(unit ^ (1 + k * 3)) = { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [ℤθ.ext_iff] at w
State after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f =
      { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.f ∧
    (↑(unit ^ (1 + k * 3))).g =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.g ∧
      (↑(unit ^ (1 + k * 3))).h =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.h
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f =
      { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.f ∧
    (↑(unit ^ (1 + k * 3))).g =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.g ∧
      (↑(unit ^ (1 + k * 3))).h =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.h
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
dsimp at w
State after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6 ∧
    (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6 ∧
    (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' w with w1 w23
State after:
case intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w23 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w23 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' w23 with w2 w3
State after:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [add_comm, mul_comm, w1, w2, w3]
State after:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2 ∧ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2 ∧ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2

case intro.intro.intro.intro.intro.intro.intro.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0

case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j3 * 15) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Tactic:
rw [Int.add_emod,Int.sub_emod,Int.mul_emod j1,Int.mul_emod j3]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
have : (3 : ℤ)%3 = 0:=by norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
have : (15 : ℤ)%3 = 0:=by norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 = 2
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
Tactic:
rw [zpow_add]
State after:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k) * unit ^ 1) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)

State before:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k) * unit ^ 1) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
Tactic:
norm_cast
State after:
no goals

State before:
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)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
Tactic:
ext <;> dsimp
State after:
case f
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))).f = 3 * j1 + 1

case g
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))).g = 3 * j2

case h
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))).h = 3 * j3

State before:
case f
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))).f = 3 * j1 + 1

case g
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))).g = 3 * j2

case h
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))).h = 3 * j3
Tactic:
exact hj1
State after:
case g
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))).g = 3 * j2

case h
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))).h = 3 * j3

State before:
case g
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))).g = 3 * j2

case h
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))).h = 3 * j3
Tactic:
exact hj2
State after:
case h
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))).h = 3 * j3

State before:
case h
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))).h = 3 * j3
Tactic:
exact hj3
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2
Tactic:
rw [Int.add_emod,Int.sub_emod, Int.mul_emod j1,Int.mul_emod j2]
State after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j2 % 3 * (6 % 3) % 3) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j2 % 3 * (6 % 3) % 3) % 3 = 2
Tactic:
norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2
Tactic:
have : (6 : ℤ)%3 = 0:=by norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * 0) % 3 = 2

State before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * 0) % 3 = 2
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ 6 % 3 = 0
Tactic:
norm_num
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0
Tactic:
rw [Int.add_emod,Int.add_emod _ (j3*6),Int.sub_emod,Int.mul_emod j1,Int.mul_emod j2,Int.mul_emod j3]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
have : (6 : ℤ)%3 = 0:=by norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
have : (9 : ℤ)%3 = 0:=by norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
have : (15 : ℤ)%3 = 0:=by norm_num
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 0

State before:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 0
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ 9 % 3 = 0
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ 15 % 3 = 0
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ 3 % 3 = 0
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ 15 % 3 = 0
Tactic:
norm_num
State after:
no goals