Theorem: BrownCs22.Int.ModEq.add (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