Theorem: pair_fn_injective (meetings/ex4.lean)

State before:
⊢ Function.Injective pair_fn
Tactic:
intros p q eq
State after:
p q : ℤ × ℤ
eq : pair_fn p = pair_fn q
⊢ p = q

State before:
p q : ℤ × ℤ
eq : pair_fn p = pair_fn q
⊢ p = q
Tactic:
simp [pair_fn] at eq
State after:
p q : ℤ × ℤ
eq : p.1 + p.2 = q.1 + q.2 ∧ 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q

State before:
p q : ℤ × ℤ
eq : p.1 + p.2 = q.1 + q.2 ∧ 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
Tactic:
rcases eq with ⟨hl, hr⟩
State after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q

State before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
Tactic:
rw [Prod.eq_iff_fst_eq_snd_eq]
State after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
apply_fun (λ e => e - (p.1 + p.2)) at hr
State after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (p.1 + p.2)
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (p.1 + p.2)
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
nth_rewrite 2 [hl] at hr
State after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (q.1 + q.2)
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (q.1 + q.2)
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
ring_nf at hr
State after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
rw [hr] at hl
State after:
case intro
p q : ℤ × ℤ
hl : q.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hl : q.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
apply_fun (λ e => e - q.1) at hl
State after:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : q.1 + p.2 - q.1 = q.1 + q.2 - q.1
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : q.1 + p.2 - q.1 = q.1 + q.2 - q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
ring_nf at hl
State after:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : p.2 = q.2
⊢ p.1 = q.1 ∧ p.2 = q.2

State before:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : p.2 = q.2
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
exact ⟨hr, hl⟩
State after:
no goals