have r1 := y_mod_three (unit ^ (3 * b) : ℤθ).f 1 t1
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
r1 : ∃ k, (↑(unit ^ (3 * b))).f = 3 * k + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0