Theorem: Usa2005P2.lemma1 (Compfiles/Usa2005P2.lean)

State before:
x : ZMod 13
⊢ x ^ 3 = 0 ∨ x ^ 3 = 1 ∨ x ^ 3 = -1 ∨ x ^ 3 = 5 ∨ x ^ 3 = -5
Tactic:
reduce_mod_char
State after:
x : ZMod 13
⊢ x ^ 3 = 0 ∨ x ^ 3 = 1 ∨ x ^ 3 = 12 ∨ x ^ 3 = 5 ∨ x ^ 3 = 8

State before:
x : ZMod 13
⊢ x ^ 3 = 0 ∨ x ^ 3 = 1 ∨ x ^ 3 = 12 ∨ x ^ 3 = 5 ∨ x ^ 3 = 8
Tactic:
fin_cases x <;> decide
State after:
no goals