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

State before:
a b c : ℤθ
n : ℕ
⊢ ∃ a, n = 3 * a ∨ n = 3 * a + 1 ∨ n = 3 * a + 2
Tactic:
induction' n with k hk
State after:
case zero
a b c : ℤθ
⊢ ∃ a, Nat.zero = 3 * a ∨ Nat.zero = 3 * a + 1 ∨ Nat.zero = 3 * a + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case zero
a b c : ℤθ
⊢ ∃ a, Nat.zero = 3 * a ∨ Nat.zero = 3 * a + 1 ∨ Nat.zero = 3 * a + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use 0
State after:
case h
a b c : ℤθ
⊢ Nat.zero = 3 * 0 ∨ Nat.zero = 3 * 0 + 1 ∨ Nat.zero = 3 * 0 + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h
a b c : ℤθ
⊢ Nat.zero = 3 * 0 ∨ Nat.zero = 3 * 0 + 1 ∨ Nat.zero = 3 * 0 + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
left
State after:
case h.h
a b c : ℤθ
⊢ Nat.zero = 3 * 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h
a b c : ℤθ
⊢ Nat.zero = 3 * 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [MulZeroClass.mul_zero]
State after:
case h.h
a b c : ℤθ
⊢ Nat.zero = 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h
a b c : ℤθ
⊢ Nat.zero = 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rfl
State after:
case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
cases' hk with j hj
State after:
case succ.intro
a b c : ℤθ
k j : ℕ
hj : k = 3 * j ∨ k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case succ.intro
a b c : ℤθ
k j : ℕ
hj : k = 3 * j ∨ k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
cases' hj with h1 h23
State after:
case succ.intro.inl
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case succ.intro.inl
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use j
State after:
case h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
right
State after:
case h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
left
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
change k + 1 = 3 * j + 1
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k + 1 = 3 * j + 1

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k + 1 = 3 * j + 1

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [add_left_inj 1]
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k = 3 * j

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k = 3 * j

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
exact h1
State after:
case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
cases' h23 with h2 h3
State after:
case succ.intro.inr.inl
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case succ.intro.inr.inl
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use j
State after:
case h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
right
State after:
case h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
right
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
change k + 1 = 3 * j + 2
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [← one_add_one_eq_two]
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + (1 + 1)

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + (1 + 1)

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [← add_assoc]
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 1 + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 1 + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [add_left_inj 1]
State after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k = 3 * j + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k = 3 * j + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
exact h2
State after:
case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

State before:
case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use j + 1
State after:
case h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1) ∨ Nat.succ k = 3 * (j + 1) + 1 ∨ Nat.succ k = 3 * (j + 1) + 2

State before:
case h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1) ∨ Nat.succ k = 3 * (j + 1) + 1 ∨ Nat.succ k = 3 * (j + 1) + 2
Tactic:
left
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1)

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1)
Tactic:
change k + 1 = 3 * (j + 1)
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * (j + 1)

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * (j + 1)
Tactic:
rw [mul_add]
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3 * 1

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3 * 1
Tactic:
rw [mul_one]
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3
Tactic:
have babymath : 3 = 2 + 1 := by norm_num
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 3

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 3
Tactic:
nth_rw 2 [babymath]
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + (2 + 1)

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + (2 + 1)
Tactic:
rw [← add_assoc]
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 2 + 1

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 2 + 1
Tactic:
rw [add_left_inj 1]
State after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k = 3 * j + 2

State before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k = 3 * j + 2
Tactic:
exact h3
State after:
no goals

State before:
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ 3 = 2 + 1
Tactic:
norm_num
State after:
no goals