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

State before:
a b : ℤ
⊢ Even a → Even (a + b) → Even b
Tactic:
intro A
State after:
a b : ℤ
A : Even a
⊢ Even (a + b) → Even b

State before:
a b : ℤ
A : Even a
⊢ Even (a + b) → Even b
Tactic:
obtain ⟨k, H⟩ := A
State after:
case intro
a b k : ℤ
H : a = k + k
⊢ Even (a + b) → Even b

State before:
case intro
a b k : ℤ
H : a = k + k
⊢ Even (a + b) → Even b
Tactic:
intro A_B
State after:
case intro
a b k : ℤ
H : a = k + k
A_B : Even (a + b)
⊢ Even b

State before:
case intro
a b k : ℤ
H : a = k + k
A_B : Even (a + b)
⊢ Even b
Tactic:
obtain ⟨k2, H2⟩ := A_B
State after:
case intro.intro
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ Even b

State before:
case intro.intro
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ Even b
Tactic:
use (k2 - k)
State after:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ b = k2 - k + (k2 - k)

State before:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ b = k2 - k + (k2 - k)
Tactic:
rw [H] at H2
State after:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ b = k2 - k + (k2 - k)

State before:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ b = k2 - k + (k2 - k)
Tactic:
apply symm
State after:
case h.a
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = b

State before:
case h.a
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = b
Tactic:
calc k2 - k + (k2 - k) = k2 + k2 - k - k := by ring
  _ = k + k + b - k -k := by rw[H2]
  _ = b := by ring
State after:
no goals

State before:
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = k2 + k2 - k - k
Tactic:
ring
State after:
no goals

State before:
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 + k2 - k - k = k + k + b - k - k
Tactic:
rw[H2]
State after:
no goals

State before:
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k + k + b - k - k = b
Tactic:
ring
State after:
no goals