How do I unfold a complicated function

Stream: new members

[Lars Ericson]

Is there a way to unroll the nat.mk operation in a proof? I have this tactic state:

1 goal
ab: ℚ
nm: ℕ
ha: a.denom = 2 ^ n
hb: b.denom = 2 ^ m
a0: 0 < a.denom
b0: 0 < b.denom
a01: ↑(a.denom) ≠ 0
b01: ↑(b.denom) ≠ 0
h2: ↑(2 ^ n) * ↑(2 ^ m) = ↑(2 ^ (n + m))
h1: mk a.num ↑(2 ^ n) * mk b.num ↑(2 ^ m) = mk (a.num * b.num) ↑(2 ^ (n + m))
h3: (mk a.num (2 ^ n) * mk b.num (2 ^ m)).denom = (mk (a.num * b.num) (2 ^ (n + m))).denom
⊢ ∃ (k : ℕ), (a * b).denom = 2 ^ k

The h3 is almost in the form of the goal. However, the mk does tricky stuff to get to the final result for .denom. If I ask Lean to unfold mk at h3,, it says

mk does not have equational lemmas nor is a projection

The definition of mk is

/-- Form the quotient `n / d` where `n d : ℤ`. -/
def mk : ℤ → ℤ → ℚ
| n (d : ℕ) := mk_nat n d
| n -[1+ d] := mk_pnat (-n) d.succ_pnat

The thing I am trying to prove is (I am stuck at the sorry):

import data.rat.basic
import data.nat.gcd
import tactic
import tactic.slim_check
open tactic
open rat

lemma nonzero_nat_to_int {a: ℕ} (ha: 0 < a) : ((coe a):ℤ) ≠ 0 :=
begin
  have h1 := ne_of_gt ha,
  exact int.coe_nat_ne_zero.mpr h1,
end

lemma combine_powers (n m : ℕ): (coe (2 ^ n):ℤ) * ↑(2 ^ m) = ↑(2 ^ (n+m)) :=
begin
  simp,
  exact ring.pow_add_rev 2 n m,
end

lemma mul_injective
        {a b : ℚ}
        {n m : ℕ}
        (ha : a.denom = 2 ^ n)
        (hb : b.denom = 2 ^ m):
        ∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
  have a0 := a.pos,
  have b0 := b.pos,
  have a01 := nonzero_nat_to_int a0,
  have b01 := nonzero_nat_to_int b0,
  have h1 := @rat.mul_def a.num a.denom b.num b.denom a01 b01,
  rw ha at h1,
  rw hb at h1,
  have h2 := combine_powers n m,
  rw h2 at h1,
  have h3 := congr_arg (λ (c:ℚ), c.denom) h1,
  simp at h3,
  unfold mk at h3, -- ERROR
  sorry,
end