internlm/Lean-Github huggingface dataset:
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)
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
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 ^ (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 * 0 % 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)
this : 15 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Tactic:
have : (12:ℤ) %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
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 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)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (12 % 3) % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
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 ^ (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
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 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)
this✝ : 15 % 3 = 0
this : 12 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
Tactic:
have : (24:ℤ) %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
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 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)
this✝¹ : 15 % 3 = 0
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (24 % 3) % 3) % 3 = 1
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 ^ (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
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 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)
this✝¹ : 15 % 3 = 0
this✝ : 12 % 3 = 0
this : 24 % 3 = 0
⊢ (((-5 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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)
⊢ 15 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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
⊢ 12 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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
this : 12 % 3 = 0
⊢ 24 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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
Tactic:
rw [Int.add_emod,Int.add_emod _ (j3*60),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 ^ (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 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Tactic:
have : (42:ℤ) %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 ^ (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 : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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 : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * (42 % 3) % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
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 ^ (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 : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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 : 42 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Tactic:
have : (60:ℤ) %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 ^ (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✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * (60 % 3) % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
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 ^ (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✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Tactic:
have : (57:ℤ) %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 ^ (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✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
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 ^ (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✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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)
⊢ 42 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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 : 42 % 3 = 0
⊢ 60 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝ : 42 % 3 = 0
this : 60 % 3 = 0
⊢ 57 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_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 ^ (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
Tactic:
rw [Int.add_emod, Int.sub_emod,Int.sub_emod (j3*75),Int.mul_emod j1,Int.mul_emod j2,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 ^ (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 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (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 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Tactic:
have : (12:ℤ) %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 ^ (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 : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (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 : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * (12 % 3) % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (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 : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (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 : 12 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Tactic:
have : (75:ℤ) %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 ^ (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✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * (75 % 3) % 3 - j2 % 3 * (6 % 3) % 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 ^ (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✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Tactic:
have : (6:ℤ) %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 ^ (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✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 3) % 3) % 3 = 2
Theorem: ℤθ.unit_zpow_two_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 ^ (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✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * (6 % 3) % 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 ^ (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✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * 0 % 3) % 3) % 3 = 2