-- Mathlib/Data/Rat/Lemmas.lean
theorem num_den_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = n /. d) :
    ∃ c : ℤ, n = c * q.num ∧ d = c * q.den

Proof state:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ c, 0 = c * q.num ∧ d = c * ↑q.den

case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Proof state:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ q.num ∣ n

Tactic:
rw [qdf]

Result:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ (n /. d).num ∣ n

Proof state:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0

Tactic:
exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)

Result:
no goals

Proof state:
case inl
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ c, 0 = c * q.num ∧ d = c * ↑q.den

Tactic:
simp [qdf]

Result:
no goals

Proof state:
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
have hqdn : q.num ∣ n := by
  rw [qdf]
  exact Rat.num_dvd _ hd

Result:
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Proof state:
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
refine ⟨n / q.num, ?_, ?_⟩

Result:
case inr.refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num

case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den

Proof state:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ q.num ≠ 0

Tactic:
rw [qdf]

Result:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0

Proof state:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * ↑q.den

Tactic:
refine (divInt_eq_iff ?_ hd).mp ?_

Result:
case refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0

case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d

Proof state:
case inr.refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num

Tactic:
rw [Int.ediv_mul_cancel hqdn]

Result:
no goals

Proof state:
case refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0

Tactic:
exact Int.natCast_ne_zero.mpr (Rat.den_nz _)

Result:
no goals

Proof state:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ (n /. d).num ∣ n

Tactic:
exact Rat.num_dvd _ hd

Result:
no goals

Proof state:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den

Tactic:
refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this

Result:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ q.num ≠ 0

Proof state:
case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d

Tactic:
rwa [num_divInt_den]

Result:
no goals