internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  ↑(unit ^ (-3 - ↑b * 3)) =
    { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
      h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
rw [ℤθ.ext_iff] at w
Proof state after:
case right.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  (↑(unit ^ (-3 - ↑b * 3))).f =
      { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
          h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }.f ∧
    (↑(unit ^ (-3 - ↑b * 3))).g =
        { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
            h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }.g ∧
      (↑(unit ^ (-3 - ↑b * 3))).h =
        { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
            h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }.h
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  (↑(unit ^ (-3 - ↑b * 3))).f =
      { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
          h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }.f ∧
    (↑(unit ^ (-3 - ↑b * 3))).g =
        { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
            h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }.g ∧
      (↑(unit ^ (-3 - ↑b * 3))).h =
        { f := 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834), g := 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729),
            h := 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592) }.h
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
dsimp at w
Proof state after:
case right.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834) ∧
    (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) ∧
      (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834) ∧
    (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) ∧
      (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
cases' w with w1 w23
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w23 :
  (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) ∧
    (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w23 :
  (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) ∧
    (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
cases' w23 with w2 w3
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
have j2: -3 - (b : ℤ)*3 = 3*(-(b+1):ℤ):= by ring
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -(↑b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -(↑b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
have j1 : (b : ℤ) + 1 = ((b + 1 : ℕ) : ℤ) := by norm_cast
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -(↑b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -(↑b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
rw [j1] at j2
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
rw [j2] at w1
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
rw [j2] at w2
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (3 * -↑(b + 1)))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (3 * -↑(b + 1)))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
rw [j2] at w3
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (3 * -↑(b + 1)))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (3 * -↑(b + 1)))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (3 * -↑(b + 1)))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (3 * -↑(b + 1)))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
Tactic:
rw [w1, w2, w3]
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (3 * -↑(b + 1)))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (3 * -↑(b + 1)))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)) % 3 = 1 ∧
    (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0 ∧ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
c1 : ℤ
hc1 : (↑(unit ^ (3 * -↑b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * -↑b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * -↑b))).h = 3 * c3
s : ↑(unit ^ (3 * -↑b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w1 : (↑(unit ^ (3 * -↑(b + 1)))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w2 : (↑(unit ^ (3 * -↑(b + 1)))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)
w3 : (↑(unit ^ (3 * -↑(b + 1)))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
j2 : -3 - ↑b * 3 = 3 * -↑(b + 1)
j1 : ↑b + 1 = ↑(b + 1)
⊢ (10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)) % 3 = 1 ∧
    (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0 ∧ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Tactic:
clear h1 h2 h3 p hc1 hc2 hc3 w1 w2 w3 s j2 j1
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)) % 3 = 1 ∧
    (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0 ∧ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)) % 3 = 1 ∧
    (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0 ∧ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Tactic:
constructor
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)) % 3 = 1

case right.succ.intro.intro.intro.intro.intro.intro.intro.right
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0 ∧ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0 ∧ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Tactic:
constructor
Proof state after:
case right.succ.intro.intro.intro.intro.intro.intro.intro.right.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729)) % 3 = 0

case right.succ.intro.intro.intro.intro.intro.intro.intro.right.right
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ (2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)) % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.zero
a b c : ℤθ
⊢ (↑(unit ^ (3 * -↑Nat.zero))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑Nat.zero))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑Nat.zero))).h % 3 = 0
Tactic:
rw [Int.ofNat_zero, neg_zero, MulZeroClass.mul_zero]
Proof state after:
case right.zero
a b c : ℤθ
⊢ (↑(unit ^ 0)).f % 3 = 1 ∧ (↑(unit ^ 0)).g % 3 = 0 ∧ (↑(unit ^ 0)).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case right.zero
a b c : ℤθ
⊢ (↑(unit ^ 0)).f % 3 = 1 ∧ (↑(unit ^ 0)).g % 3 = 0 ∧ (↑(unit ^ 0)).h % 3 = 0
Tactic:
exact unit_pow_zero
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ Nat.succ b = b + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
Tactic:
rw [neg_add, mul_add, mul_neg_one, zpow_add]
Proof state after:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ ↑(unit ^ (3 * -↑b) * unit ^ (-3)) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ ↑(unit ^ (3 * -↑b) * unit ^ (-3)) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
Tactic:
norm_cast
Proof state after:
no goals