Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.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
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
w :
  ↑(unit ^ (3 * -(↑b + 1))) =
    {
      f :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := 10591, g := 5553, h := 2139 }.f +
              6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.h -
            2 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.h -
          2 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.g,
      g :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := 10591, g := 5553, h := 2139 }.g +
                { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.f +
              16 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.h -
            6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.h -
          6 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.g,
      h :=
        { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.f * { f := 10591, g := 5553, h := 2139 }.h +
                  { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.f +
                { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.g +
              3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.h -
            3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.g * { f := 10591, g := 5553, h := 2139 }.h -
          3 * { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }.h * { f := 10591, g := 5553, h := 2139 }.g }
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
dsimp at w
Proof state after:
case right.succ.intro.intro.intro.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
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
w :
  ↑(unit ^ (3 * -(↑b + 1))) =
    { f := (3 * c1 + 1) * 10591 + 6 * (3 * c3) * 2139 - 2 * (3 * c2) * 2139 - 2 * (3 * c3) * 5553,
      g := (3 * c1 + 1) * 5553 + 3 * c2 * 10591 + 16 * (3 * c3) * 2139 - 6 * (3 * c2) * 2139 - 6 * (3 * c3) * 5553,
      h :=
        (3 * c1 + 1) * 2139 + 3 * c3 * 10591 + 3 * c2 * 5553 + 3 * (3 * c3) * 2139 - 3 * (3 * c2) * 2139 -
          3 * (3 * c3) * 5553 }
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0