internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 1)) =
    {
      f :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -1, g := -3, h := -1 }.f +
              6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.h -
            2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.h -
          2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.g,
      g :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -1, g := -3, h := -1 }.g +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.f +
              16 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.h -
            6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.h -
          6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.g,
      h :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -1, g := -3, h := -1 }.h +
                  { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.f +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.g +
              3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.h -
            3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -1, g := -3, h := -1 }.h -
          3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -1, g := -3, h := -1 }.g }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
dsimp at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 1)) =
    { f := (3 * j1 + 1) * -1 + 6 * (3 * j3) * -1 - 2 * (3 * j2) * -1 - 2 * (3 * j3) * -3,
      g := (3 * j1 + 1) * -3 + 3 * j2 * -1 + 16 * (3 * j3) * -1 - 6 * (3 * j2) * -1 - 6 * (3 * j3) * -3,
      h := (3 * j1 + 1) * -1 + 3 * j3 * -1 + 3 * j2 * -3 + 3 * (3 * j3) * -1 - 3 * (3 * j2) * -1 - 3 * (3 * j3) * -3 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 1)) =
    { f := (3 * j1 + 1) * -1 + 6 * (3 * j3) * -1 - 2 * (3 * j2) * -1 - 2 * (3 * j3) * -3,
      g := (3 * j1 + 1) * -3 + 3 * j2 * -1 + 16 * (3 * j3) * -1 - 6 * (3 * j2) * -1 - 6 * (3 * j3) * -3,
      h := (3 * j1 + 1) * -1 + 3 * j3 * -1 + 3 * j2 * -3 + 3 * (3 * j3) * -1 - 3 * (3 * j2) * -1 - 3 * (3 * j3) * -3 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
ring_nf at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  ↑(unit ^ (1 + k * 3)) = { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  ↑(unit ^ (1 + k * 3)) = { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [ℤθ.ext_iff] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f =
      { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.f ∧
    (↑(unit ^ (1 + k * 3))).g =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.g ∧
      (↑(unit ^ (1 + k * 3))).h =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.h
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f =
      { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.f ∧
    (↑(unit ^ (1 + k * 3))).g =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.g ∧
      (↑(unit ^ (1 + k * 3))).h =
        { f := -1 - j1 * 3 + j2 * 6, g := -3 - j1 * 9 + j3 * 6 + j2 * 15, h := -1 - j1 * 3 + j3 * 15 }.h
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
dsimp at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6 ∧
    (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6 ∧
    (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' w with w1 w23
Proof state after:
case intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w23 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w23 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15 ∧ (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
cases' w23 with w2 w3
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
Tactic:
rw [add_comm, mul_comm, w1, w2, w3]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2 ∧ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2 ∧ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2

case intro.intro.intro.intro.intro.intro.intro.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0 ∧ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-3 - j1 * 9 + j3 * 6 + j2 * 15) % 3 = 0

case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j3 * 15) % 3 = 2
Tactic:
rw [Int.add_emod,Int.sub_emod,Int.mul_emod j1,Int.mul_emod j3]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
have : (3 : ℤ)%3 = 0:=by norm_num
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
rw [this]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
have : (15 : ℤ)%3 = 0:=by norm_num
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
Tactic:
rw [this]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this✝ : 3 % 3 = 0
this : 15 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
Tactic:
rw [zpow_add]
Proof state after:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k) * unit ^ 1) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k) * unit ^ 1) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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 }
Tactic:
ext <;> dsimp
Proof state after:
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
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
Tactic:
exact hj1
Proof state after:
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
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
Tactic:
exact hj2
Proof state after:
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
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
Tactic:
exact hj3
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 - j1 * 3 + j2 * 6) % 3 = 2
Tactic:
rw [Int.add_emod,Int.sub_emod, Int.mul_emod j1,Int.mul_emod j2]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j2 % 3 * (6 % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j2 % 3 * (6 % 3) % 3) % 3 = 2
Tactic:
norm_num
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2
Tactic:
have : (6 : ℤ)%3 = 0:=by norm_num
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2