rw [this]
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝² : 10591 % 3 = 1
this✝¹ : 31773 % 3 = 0
this✝ : 5184 % 3 = 0
this : 12834 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this✝² : 10591 % 3 = 1
this✝¹ : 31773 % 3 = 0
this✝ : 5184 % 3 = 0
this : 12834 % 3 = 0
⊢ ((1 + c1 % 3 * 0 % 3) % 3 + (c3 % 3 * 0 % 3 - c2 % 3 * 0 % 3) % 3) % 3 = 1