Theorem: BrownCs22.Int.ModEq.mul (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 * c + b * y, by linear_combination c * hx + b * 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 * c + b * y)
Tactic:
linear_combination c * hx + b * hy
State after:
no goals