cases' t2 with j2 hj2
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
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