Theorem: HTPI.qr_one_one (HTPILib/Chap8Part2.lean)

State before:
n : ℕ
⊢ one_to_one (qr n)
Tactic:
define
State after:
n : ℕ
⊢ ∀ (x1 x2 : ℕ), qr n x1 = qr n x2 → x1 = x2

State before:
n : ℕ
⊢ ∀ (x1 x2 : ℕ), qr n x1 = qr n x2 → x1 = x2
Tactic:
fix a1 : Nat
State after:
n a1 : ℕ
⊢ ∀ (x2 : ℕ), qr n a1 = qr n x2 → a1 = x2

State before:
n a1 : ℕ
⊢ ∀ (x2 : ℕ), qr n a1 = qr n x2 → a1 = x2
Tactic:
fix a2 : Nat
State after:
n a1 a2 : ℕ
⊢ qr n a1 = qr n a2 → a1 = a2

State before:
n a1 a2 : ℕ
⊢ qr n a1 = qr n a2 → a1 = a2
Tactic:
assume h1 : qr n a1 = qr n a2
State after:
n a1 a2 : ℕ
h1 : qr n a1 = qr n a2
⊢ a1 = a2

State before:
n a1 a2 : ℕ
h1 : qr n a1 = qr n a2
⊢ a1 = a2
Tactic:
rewrite [qr_def, qr_def] at h1
State after:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
⊢ a1 = a2

State before:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
⊢ a1 = a2
Tactic:
have h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n := Prod.mk.inj h1
State after:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n
⊢ a1 = a2

State before:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n
⊢ a1 = a2
Tactic:
show a1 = a2 from
  calc a1
    _ = n * (a1 / n) + a1 % n := (Nat.div_add_mod a1 n).symm
    _ = n * (a2 / n) + a2 % n := by rw [h2.left, h2.right]
    _ = a2 := Nat.div_add_mod a2 n
State after:
no goals

State before:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n
⊢ n * (a1 / n) + a1 % n = n * (a2 / n) + a2 % n
Tactic:
rw [h2.left, h2.right]
State after:
no goals