Theorem: Poland2016S1P8.div_4_mul_of_both_even (Compfiles/Poland2016S1P8.lean)

State before:
a b : ℤ
H : Even a ∧ Even b
⊢ 4 ∣ a * b
Tactic:
obtain ⟨k, Hk⟩ := H.left
State after:
case intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
⊢ 4 ∣ a * b

State before:
case intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
⊢ 4 ∣ a * b
Tactic:
obtain ⟨l, Hl⟩ := H.right
State after:
case intro.intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ 4 ∣ a * b

State before:
case intro.intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ 4 ∣ a * b
Tactic:
use k * l
State after:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ a * b = 4 * (k * l)

State before:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ a * b = 4 * (k * l)
Tactic:
rw[Hk]
State after:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * b = 4 * (k * l)

State before:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * b = 4 * (k * l)
Tactic:
rw[Hl]
State after:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * (l + l) = 4 * (k * l)

State before:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * (l + l) = 4 * (k * l)
Tactic:
ring
State after:
no goals