Theorem: pair_fn_surjective (meetings/ex4.lean)

State before:
⊢ Function.Surjective pair_fn
Tactic:
intro p
State after:
p : ℤ × ℤ
⊢ ∃ a, pair_fn a = p

State before:
p : ℤ × ℤ
⊢ ∃ a, pair_fn a = p
Tactic:
simp [pair_fn]
State after:
p : ℤ × ℤ
⊢ ∃ a b, (a + b, 2 * a + b) = p

State before:
p : ℤ × ℤ
⊢ ∃ a b, (a + b, 2 * a + b) = p
Tactic:
use (-p.1 + p.2)
State after:
case h
p : ℤ × ℤ
⊢ ∃ b, (-p.1 + p.2 + b, 2 * (-p.1 + p.2) + b) = p

State before:
case h
p : ℤ × ℤ
⊢ ∃ b, (-p.1 + p.2 + b, 2 * (-p.1 + p.2) + b) = p
Tactic:
use (2 * p.1 - p.2)
State after:
case h
p : ℤ × ℤ
⊢ (-p.1 + p.2 + (2 * p.1 - p.2), 2 * (-p.1 + p.2) + (2 * p.1 - p.2)) = p

State before:
case h
p : ℤ × ℤ
⊢ (-p.1 + p.2 + (2 * p.1 - p.2), 2 * (-p.1 + p.2) + (2 * p.1 - p.2)) = p
Tactic:
ring_nf
State after:
no goals