internlm/Lean-Github huggingface dataset:
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
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * (6 % 3)) % 3 = 2
Tactic:
rw [this]
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 * 0) % 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
this : 6 % 3 = 0
⊢ (-1 + j2 % 3 * 0) % 3 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
⊢ 6 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
Tactic:
rw [Int.add_emod,Int.add_emod _ (j3*6),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.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 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
have : (6 : ℤ)%3 = 0:=by norm_num
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
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * (6 % 3) % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
rw [this]
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
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this : 6 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
have : (9 : ℤ)%3 = 0:=by norm_num
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
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * (9 % 3) % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
rw [this]
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
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this✝ : 6 % 3 = 0
this : 9 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
have : (15 : ℤ)%3 = 0:=by norm_num
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
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (15 % 3) % 3) % 3 = 0
Tactic:
rw [this]
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
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 0
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this✝¹ : 6 % 3 = 0
this✝ : 9 % 3 = 0
this : 15 % 3 = 0
⊢ (((-3 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
⊢ 9 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
this : 9 % 3 = 0
⊢ 15 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_one_mod_three
Proof state before:
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
⊢ 15 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
a b c : ℤθ
⊢ ∀ (k : ℤ), (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
intro k
Proof state after:
a b c : ℤθ
k : ℤ
⊢ (↑(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:
a b c : ℤθ
k : ℤ
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have w :
  ((unit ^ (3 * k + 2) : ℤθˣ) : ℤθ) = ((unit ^ (3 * k) : ℤθˣ) : ℤθ) * ((unit ^ 2 : ℤθˣ) : ℤθ) :=
  by
  rw [zpow_add]
  norm_cast
Proof state after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
⊢ (↑(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:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have g := unit_zpow_zero_mod_three
Proof state after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(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:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
specialize g k
Proof state after:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(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:
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g : (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' g with g1 g23
Proof state after:
case intro
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g23 : (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(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
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 2)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 2)
g1 : (↑(unit ^ (3 * k))).f % 3 = 1
g23 : (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' g23 with g2 g3
Proof state after:
case intro.intro
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
⊢ (↑(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
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
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have t1 := y_mod_three ((unit ^ (3 * k) : ℤθˣ) : ℤθ).f 1 g1
Proof state after:
case intro.intro
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
t1 : ∃ k_1, (↑(unit ^ (3 * k))).f = 3 * k_1 + 1
⊢ (↑(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
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
t1 : ∃ k_1, (↑(unit ^ (3 * k))).f = 3 * k_1 + 1
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' t1 with j1 hj1
Proof state after:
case intro.intro.intro
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
⊢ (↑(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
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
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have t2 := y_mod_three ((unit ^ (3 * k) : ℤθˣ) : ℤθ).g 0 g2
Proof state after:
case intro.intro.intro
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
t2 : ∃ k_1, (↑(unit ^ (3 * k))).g = 3 * k_1 + 0
⊢ (↑(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
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
t2 : ∃ k_1, (↑(unit ^ (3 * k))).g = 3 * k_1 + 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' t2 with j2 hj2
Proof state after:
case intro.intro.intro.intro
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 + 0
⊢ (↑(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
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 + 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [add_zero] at hj2
Proof state after:
case intro.intro.intro.intro
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
⊢ (↑(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
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
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have t3 := y_mod_three ((unit ^ (3 * k) : ℤθˣ) : ℤθ).h 0 g3
Proof state after:
case intro.intro.intro.intro
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
t3 : ∃ k_1, (↑(unit ^ (3 * k))).h = 3 * k_1 + 0
⊢ (↑(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
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
t3 : ∃ k_1, (↑(unit ^ (3 * k))).h = 3 * k_1 + 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
cases' t3 with j3 hj3
Proof state after:
case intro.intro.intro.intro.intro
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 + 0
⊢ (↑(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 : ℤ
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 + 0
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
rw [add_zero] at hj3
Proof state after:
case intro.intro.intro.intro.intro
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 + 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 : ℤ
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 + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
Tactic:
have s : ((unit ^ (3 * k) : ℤθˣ) : ℤθ) = ⟨3 * j1 + 1, 3 * j2, 3 * j3⟩ :=
  by
  ext <;> dsimp
  exact hj1; exact hj2; exact hj3
Proof state after:
case intro.intro.intro.intro.intro
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
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 : ℤ
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
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:
clear g1 g2 g3 hj1 hj2 hj3
Proof state after:
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