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

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

State before:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a - c ≡ b - d [ZMOD n]
Tactic:
obtain ⟨y, hy⟩ := h2
State after:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a - c ≡ b - d [ZMOD n]

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

State before:
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a - c - (b - d) = n * (x - y)
Tactic:
linear_combination hx - hy
State after:
no goals