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

State before:
a b c : ℤθ
⊢ ∀ (k : ℤ), (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
intro k
State after:
a b c : ℤθ
k : ℤ
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
a b c : ℤθ
k : ℤ
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have w :
  ((unit ^ (3 * k + 2) : ℤθˣ) : ℤθ) = ((unit ^ (3 * k) : ℤθˣ) : ℤθ) * ((unit ^ 2 : ℤθˣ) : ℤθ) :=
  by
  rw [zpow_add]
  norm_cast
State after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have g := unit_zpow_zero_mod_three
State after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
specialize g k
State after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' g with g1 g23
State after:
case intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g23 : (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g23 : (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' g23 with g2 g3
State after:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g2 : (↑(unit ^ (3 * k))).g % 3 = 0
g3 : (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' t1 with j1 hj1
State after:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' t2 with j2 hj2
State after:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [add_zero] at hj2
State after:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2

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

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

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

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

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

State before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 2)) =
    { f := (3 * j1 + 1) * -5 + 6 * (3 * j3) * -4 - 2 * (3 * j2) * -4 - 2 * (3 * j3) * -14,
      g := (3 * j1 + 1) * -14 + 3 * j2 * -5 + 16 * (3 * j3) * -4 - 6 * (3 * j2) * -4 - 6 * (3 * j3) * -14,
      h := (3 * j1 + 1) * -4 + 3 * j3 * -5 + 3 * j2 * -14 + 3 * (3 * j3) * -4 - 3 * (3 * j2) * -4 - 3 * (3 * j3) * -14 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3)) =
    { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
      h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3)) =
    { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
      h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f =
      { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
          h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.f ∧
    (↑(unit ^ (2 + k * 3))).g =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.g ∧
      (↑(unit ^ (2 + k * 3))).h =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.h
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f =
      { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
          h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.f ∧
    (↑(unit ^ (2 + k * 3))).g =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.g ∧
      (↑(unit ^ (2 + k * 3))).h =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.h
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24 ∧
    (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
      (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24 ∧
    (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
      (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w23 :
  (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
    (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w23 :
  (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
    (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [add_comm 2,mul_comm k] at 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1 ∧
    (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1 ∧
    (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 3 = 2

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

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

State before:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1
Tactic:
rw [Int.add_emod,Int.add_emod _ (j3*12),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.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Tactic:
have : (15:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 15 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 15 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 15 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 15 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Tactic:
have : (12:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Tactic:
have : (24:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 15 % 3 = 0
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 15 % 3 = 0
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 15 % 3 = 0
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 15 % 3 = 0
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 15 % 3 = 0
⊢ 12 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ 24 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1
Tactic:
rw [Int.add_emod,Int.add_emod _ (j3*60),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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (((-14 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (((-14 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Tactic:
have : (42:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Tactic:
have : (60:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Tactic:
have : (57:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ 42 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 42 % 3 = 0
⊢ 60 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ 57 % 3 = 0
Tactic:
norm_num
State after:
no goals

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 3 = 2
Tactic:
rw [Int.add_emod, Int.sub_emod,Int.sub_emod (j3*75),Int.mul_emod j1,Int.mul_emod j2,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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ ((-4 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ ((-4 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Tactic:
have : (12:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Tactic:
have : (75:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Tactic:
have : (6:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * 0 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * 0 % 3) % 3) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ 12 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 12 % 3 = 0
⊢ 75 % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ 6 % 3 = 0
Tactic:
norm_num
State after:
no goals