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

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

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

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

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