Theorem: BrownCs22.Int.ModEq.symm (BrownCs22/Library/ModEq/Lemmas.lean)

State before:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ b ≡ a [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h
State after:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ b ≡ a [ZMOD n]

State before:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ b ≡ a [ZMOD n]
Tactic:
exact ⟨-x, by linear_combination - hx⟩
State after:
no goals

State before:
n a b x : ℤ
hx : a - b = n * x
⊢ b - a = n * -x
Tactic:
linear_combination - hx
State after:
no goals