Theorem: ℤθ.unit_zpow_zero_mod_three (Mordell4/CubicRing.lean)

State before:
a b c : ℤθ
⊢ ∀ (k : ℤ), (↑(unit ^ (3 * k))).f % 3 = 1 ∧ (↑(unit ^ (3 * k))).g % 3 = 0 ∧ (↑(unit ^ (3 * k))).h % 3 = 0
Tactic:
intro q
State after:
a b c : ℤθ
q : ℤ
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
a b c : ℤθ
q : ℤ
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
have h := lt_or_le 0 q
State after:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
have p := unit_pow_zero_mod_three
State after:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
cases' h with h1 h2
State after:
case inl
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h1 : 0 < q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

case inr
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h2 : q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h2 : q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
specialize p (Int.toNat (-q))
State after:
case inr
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p :
  ((↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p :
  ((↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
cases' p with p1 p2
State after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
have r := neg_le_neg h2
State after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : -0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : -0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [neg_zero] at r
State after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [Int.toNat_of_nonneg r] at p2
State after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * - -q))).f % 3 = 1 ∧ (↑(unit ^ (3 * - -q))).g % 3 = 0 ∧ (↑(unit ^ (3 * - -q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * - -q))).f % 3 = 1 ∧ (↑(unit ^ (3 * - -q))).g % 3 = 0 ∧ (↑(unit ^ (3 * - -q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [neg_neg] at p2
State after:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
r : 0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
exact p2
State after:
no goals

State before:
case inl
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h1 : 0 < q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
specialize p (Int.toNat q)
State after:
case inl
a b c : ℤθ
q : ℤ
h1 : 0 < q
p :
  ((↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inl
a b c : ℤθ
q : ℤ
h1 : 0 < q
p :
  ((↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
cases' p with p1 p2
State after:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
rw [Int.toNat_of_nonneg (le_of_lt h1)] at p1
State after:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0

State before:
case inl.intro
a b c : ℤθ
q : ℤ
h1 : 0 < q
p1 : (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
Tactic:
exact p1
State after:
no goals