ext <;> dsimp
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 }
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