-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_num_den (z : d ≠ 0) (h : n /. d = ⟨n', d', z', c⟩) :
    ∃ m, m ≠ 0 ∧ n = n' * m ∧ d = d' * m

Proof state:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m

Tactic:
rw [← Int.neg_inj, Int.neg_neg] at h₂

Result:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : n = -(n' * ↑m) ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m

Proof state:
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m

Tactic:
exists m

Result:
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬↑m = 0 ∧ n = n' * ↑m ∧ ↑w✝ = ↑d' * ↑m

Proof state:
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬↑m = 0 ∧ n = n' * ↑m ∧ ↑w✝ = ↑d' * ↑m

Tactic:
simp [Int.ofNat_eq_zero, Int.ofNat_mul, h₁, h₂]

Result:
no goals

Proof state:
d n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
z : d ≠ 0
h : n /. d = { num := n', den := d', den_nz := z', reduced := c }
⊢ ∃ m, m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m

Tactic:
rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;>
  simp_all [divInt_neg', Int.ofNat_eq_zero, Int.neg_eq_zero]

Result:
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m

case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m

Proof state:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m

Tactic:
exists -m

Result:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m

Proof state:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m

Tactic:
have ⟨m, h₁, h₂⟩ := mkRat_num_den z h

Result:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m

Proof state:
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : n = -(n' * ↑m) ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m

Tactic:
simp [Int.ofNat_eq_zero, Int.ofNat_mul, h₁, h₂, Int.mul_neg, Int.neg_eq_zero]

Result:
no goals

Proof state:
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m

Tactic:
have ⟨m, h₁, h₂⟩ := mkRat_num_den z h

Result:
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m