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

State before:
a b c : ℤθ
y s : ℤ
h : y % 3 = s
⊢ ∃ k, y = 3 * k + s
Tactic:
have q := Int.dvd_sub_of_emod_eq h
State after:
a b c : ℤθ
y s : ℤ
h : y % 3 = s
q : 3 ∣ y - s
⊢ ∃ k, y = 3 * k + s

State before:
a b c : ℤθ
y s : ℤ
h : y % 3 = s
q : 3 ∣ y - s
⊢ ∃ k, y = 3 * k + s
Tactic:
cases' q with l lh
State after:
case intro
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ ∃ k, y = 3 * k + s

State before:
case intro
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ ∃ k, y = 3 * k + s
Tactic:
use l
State after:
case h
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ y = 3 * l + s

State before:
case h
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ y = 3 * l + s
Tactic:
exact eq_add_of_sub_eq lh
State after:
no goals