internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [s] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 2)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑(unit ^ 2)
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 2)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑(unit ^ 2)
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [unit_sq] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 2)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * { f := -5, g := -14, h := -4 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 2)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * { f := -5, g := -14, h := -4 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [hMul_mule_3] at w
Proof state after:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 2)) =
    {
      f :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.f +
              6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g,
      g :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.g +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.f +
              16 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g,
      h :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.h +
                  { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.f +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.g +
              3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 2)) =
    {
      f :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.f +
              6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g,
      g :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.g +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.f +
              16 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g,
      h :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.h +
                  { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.f +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.g +
              3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 + 2)) =
    { f := (3 * j1 + 1) * -5 + 6 * (3 * j3) * -4 - 2 * (3 * j2) * -4 - 2 * (3 * j3) * -14,
      g := (3 * j1 + 1) * -14 + 3 * j2 * -5 + 16 * (3 * j3) * -4 - 6 * (3 * j2) * -4 - 6 * (3 * j3) * -14,
      h := (3 * j1 + 1) * -4 + 3 * j3 * -5 + 3 * j2 * -14 + 3 * (3 * j3) * -4 - 3 * (3 * j2) * -4 - 3 * (3 * j3) * -14 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 2)) =
    { f := (3 * j1 + 1) * -5 + 6 * (3 * j3) * -4 - 2 * (3 * j2) * -4 - 2 * (3 * j3) * -14,
      g := (3 * j1 + 1) * -14 + 3 * j2 * -5 + 16 * (3 * j3) * -4 - 6 * (3 * j2) * -4 - 6 * (3 * j3) * -14,
      h := (3 * j1 + 1) * -4 + 3 * j3 * -5 + 3 * j2 * -14 + 3 * (3 * j3) * -4 - 3 * (3 * j2) * -4 - 3 * (3 * j3) * -14 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3)) =
    { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
      h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (2 + k * 3)) =
    { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
      h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f =
      { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
          h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.f ∧
    (↑(unit ^ (2 + k * 3))).g =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.g ∧
      (↑(unit ^ (2 + k * 3))).h =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.h
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (2 + k * 3))).f =
      { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
          h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.f ∧
    (↑(unit ^ (2 + k * 3))).g =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.g ∧
      (↑(unit ^ (2 + k * 3))).h =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.h
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24 ∧
    (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
      (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24 ∧
    (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
      (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w23 :
  (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
    (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w23 :
  (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
    (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [add_comm 2,mul_comm k] at 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1 ∧
    (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1 ∧
    (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1 ∧ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-14 - j1 * 42 + j3 * 60 + j2 * 57) % 3 = 1

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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-4 - j1 * 12 + (j3 * 75 - j2 * 6)) % 3 = 2
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
Tactic:
rw [zpow_add]
Proof state after:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k) * unit ^ 2) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
a b c : ℤθ
k : ℤ
⊢ ↑(unit ^ (3 * k) * unit ^ 2) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
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
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 + 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
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 + 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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).g = 3 * j2

case h
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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).h = 3 * j3
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case f
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
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 + 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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).g = 3 * j2

case h
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
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 + 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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).g = 3 * j2

case h
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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).h = 3 * j3
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case g
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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).g = 3 * j2

case h
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
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 + 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
j3 : ℤ
hj3 : (↑(unit ^ (3 * k))).h = 3 * j3
⊢ (↑(unit ^ (3 * k))).h = 3 * j3
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case h
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
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_two_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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (-5 - j1 * 15 + j3 * 12 + j2 * 24) % 3 = 1
Tactic:
rw [Int.add_emod,Int.add_emod _ (j3*12),Int.sub_emod,Int.mul_emod j1,Int.mul_emod j2,Int.mul_emod j3]
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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Tactic:
have : (15:ℤ) %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 ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 15 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * (15 % 3) % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1